[isabelle-dev] NEWS: generated code as proper theory export
makarius at sketis.net
Tue Feb 5 20:05:06 CET 2019
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.)
More information about the isabelle-dev