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
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.)
isabelle-dev mailing list