On 31/01/2019 20:37, Mathias Fleury wrote: > >> On 31. Jan 2019, at 20:10, Makarius <makar...@sketis.net >> >> Can you point to these special applications? >> >> If export_code uses Generated_Files.add_files (in addition to >> Export.export) we get both a check for unique names and an easy way to >> retrieve the exports in Isabelle/ML, e.g. to write to a temporary >> directory and do some tests. > > Can you give some more details on how to achieve this? > > Concrete application: I have a verified SAT solver (lets call that > function isasat), an unverified parser, and several large CNF files > (each one is several MB large). I would like to compile the SAT solver > with MLton*, test it on those CNF files. With some timings information > to identify regression if possible. > >> So far I have never seen an application that could not be made stateless >> and thus fit properly into the PIDE model.
The general principle is to keep generated material inside the theory context (Generated_Files) and take them from there to produce other artifacts in Isabelle/ML, e.g. as a "sink" to produce error information, timing etc. It is also possible to formally export sources or artifacts to the session build database using Export.export: Isabelle/Scala can take results from there and do something else with it, but inside the build process, only after it. * Here is a simple example with 'generated_file': https://isabelle.in.tum.de/repos/isabelle/file/7e4966eaf781/src/Tools/Haskell/Haskell.thy * Here is a test build inside Isabelle/ML -- this is stateless thanks to a temp dir: https://isabelle.in.tum.de/repos/isabelle/file/7e4966eaf781/src/Tools/Haskell/Test.thy * Here is the use of the same sources in session database exports, written to a global file-space that is not the Isabelle (or AFP) repository: https://github.com/Naproche/Naproche-SAD/commit/698527fc6a47839bd48c521beb3d71129e3924a4 Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev