Re: [isabelle] Code_Target.evaluator raises various exception during serialisation
Thank you for the quick response.
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.
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.
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.
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and