[isabelle-dev] NEWS: commands for generated files
c.sternagel at gmail.com
Fri Apr 5 10:37:24 CEST 2019
I had a look at
and the new stateless setup looks great.
I am also delighted by the possibility to browse the resulting generated
code from inside Isabelle/jEdit. Very convenient!
PS: At first I was a bit confused about where the documentation for
"compile_generated_files" had gone, before I remembered that, of course,
I had to run "isabelle build_doc isar-ref" first.
On 4/4/19 10:56 PM, Makarius wrote:
> *** General ***
> * Commands 'generate_file', 'export_generated_files', and
> 'compile_generated_files' support a stateless (PIDE-conformant) model
> for generated sources and compiled binaries of other languages. The
> compilation processed is managed in Isabelle/ML, and results exported to
> the session database for further use (e.g. with "isabelle export" or
> "isabelle build -e").
> This refers to Isabelle/0403b5127da1, which also contains the
> documentation in the isar-ref manual as usual.
> Examples are in AFP/390cb3cbebad: theories
> Diophantine_Eqns_Lin_Hom.Solver_Code and
> Buchi_Complementation.Complementation_Build as before, but now using the
> Isar command 'compile_generated_files'. This provides a better overview
> of incoming and outgoing files in concrete syntax, including hyperlinks
> to various physical and logical locations.
> From my side that finishes the functionalities for stateless generated /
> exported files for the Isabelle2019. If anything is still missing or not
> properly working, we have still a few weeks to sort it out.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev