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.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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