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

Salomon Sickert sickert at in.tum.de
Tue Feb 5 13:18:55 CET 2019

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


More information about the isabelle-dev mailing list