Re: [isabelle] Code_Target.evaluator raises various exception during serialisation



Hi Florian,

Thank you for the quick response.

When building similar thing, it is best to follow structure
Code_Runtime.  The Quickcheck Narrowing engine is an experimental
(though apparently operative) ad-hoc approach toward code generation and
definitely nothing I recommend to glimpse from in that respect.
In Code_Runtime, we have not found anything related to actually writing out the files, compiling and executing them and reading back the input. This is essentially what we take from Quickcheck_Narrowing. We am aware that the whole setup with narrowing_engine.hs is ad hoc and we avoid that.

There is also something in both Code_Runtime and Quickcheck_Narrowing that we have not yet understood. What is the purpose of the cookies that appear everywhere? So far, our solution seems to work without them, but maybe our testcases are too simple.

Both problems cannot be reproduced on the ongoing development branch.
Since we are converging towards a release, you might consider basing
your work on a particular source code revision until the next release.

The whole evaluation stack has seen considerable reworking and
clarification during the last months and subtle misbehaviours are likely
to have been eliminated.

I'm not giving this advice light-minded but I trust your experience.  In
case, we should continue the discussion on isabelle-dev.
The problem is that it is not just me, but also a student working on this. We'll think about this and let you know if we switch.

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.