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

Makarius makarius at sketis.net
Thu Jan 10 16:38:40 CET 2019

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.

On Mon..Wed this week I visited the Innsbruck Isabelle site (the city of
Innsbruck is very professional in managing a lot of snow without
hindering public life :-)

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

  * 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).


More information about the isabelle-dev mailing list