On 05.02.19 13:18, Salomon Sickert wrote:
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.
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.
A partial example with generated files is src/Tools/Haskell/Test.thy
(e.g. in Isabelle/2c3e5e58d93f): the generated Haskell sources are used
for a test build, but its result is thrown away instead of exporting it.
I have some ideas in the pipeline to make the 'export_files'
specifications in session ROOT entries more robust (no export by
default) and more useful (collective export on something like "isabelle
build -e").
We also need to wait for Florian Haftmann to provide the
Generated_Files.add_files facility to 'export_code' -- in parallel to
its existing Export.export. The main difference that this will be an
update on the theory.
(Note that I am presently busy elsewhere and only sporadically connected.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
