>> 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to