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.
> AFP/HLDE.
>
> 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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
