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

Makarius makarius at sketis.net
Fri Jan 11 11:51:18 CET 2019

On 10/01/2019 16:38, Makarius wrote:
> On 10/01/2019 16:28, Florian Haftmann wrote:
>> Code generation: command 'export_code' without file keyword exports
>> code as regular theory export, which can be materialized using tool
>> 'isabelle export'; to get generated code dumped into output, use
>> 'file ""'.  Minor INCOMPATIBILITY.
>> This refers to e02bdf853a4c and opens opportunities to get rid of ad-hoc
>> generated code in AFP-entries.
> Great, I will try this out soon.

I have started looking and thinking about it again.

First note that Export.export_raw is only required for very big exports
that have their own compression somehow built in. You can always use
Export.export in regular applications: the compression status is stored
in the database, and the exported result is uncompressed.

> I've had some discussions with users of Haskell code generation, e.g.
> My conclusions so far:
>   * primary (default) output should be via the new Generated_Files
> module in Isabelle/ML; thus applications can refer to file content via a
> theory context, e.g. to write it to the file-system via
> Generated_Files.write_files.
>   * secondary output works via the Export interface to Isabelle/Scala;
> e.g. I could easily add Generated_Files.export_files for that and
> export_code would merely use Generated_Files.add_files (no export yet).

I have added Generated_Files.export_files in Isabelle/a2fbfdc5e62d: the
generated sources from Isabelle/Haskell serve as an example.

How to proceed from here is still unclear. I will look more closely at
the applications of 'export_code' in AFP. The question is if we can get
rid of all options for experimentation ('file') and have the Prover IDE
and system environment take care of it.


More information about the isabelle-dev mailing list