[isabelle-dev] NEWS: commands for generated files

[Christian Sternagel]

Dear Makarius,

I had a look at

  Diophantine_Eqns_Lin_Hom.Solver_Code

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!

cheers

chris

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.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>