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 > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev > _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
