[isabelle-dev] NEWS: generated code as proper theory export

Makarius makarius at sketis.net
Thu Jan 31 20:59:45 CET 2019

On 31/01/2019 20:37, Mathias Fleury wrote:
>> On 31. Jan 2019, at 20:10, Makarius <makarius at 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':


* Here is a test build inside Isabelle/ML -- this is stateless thanks to
a temp dir:


* 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:



More information about the isabelle-dev mailing list