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

>> 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.

Then your life is easy: just invoke your external process and return
your result.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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