[isabelle-dev] NEWS: generated code as proper theory export

[Salomon Sickert]

>> To add a couple more to the list:
>> 
>> — LTL has includes a parser that is used in an example and built using LTL/examples/build_poly.sh
>> 
>> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh and LTL_to_DRA/Code/build_mlton.sh
> 
> It should be easy to make this part of the formal session, with some
> options [condition = ISABELLE_MLTON].
> 
> The 'export_code' command will have to emit generated files
> (Generated_Files.add_files) to make the assembly work in Isabelle/ML.
> 
> I have already added support for executable exports in
> Isabelle/c175499a7537 -- a few more such fine-tunings might be required.

That is a great development. 

Could someone point me to an example on how to do compilation with either mlton or polyml within a formal session?
The build scripts in these two entries are copying the style of the CAVA entry at that time and I’m not sure about the current best practices here.

Best,
Salomon