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

Hi Florian,

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.

the actual compiler invocation is in these lines in Code_Runtime:

fun exec verbose code =
   (if ! trace then tracing code else ();
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
This is a compiler invocation, but within Isabelle's PolyML process. That is not what I meant in the above. We need to write out the files and compile and run them using external programs such as GHC.

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 cookies are a device to connect to ML more or less raw compiler to
the runtime system.
Thanks for the explanation. That confirms my feeling that we probably do not need these cookies, because our application do not invoke the ML compiler inside Isabelle's ML process any more.


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