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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev