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

[Makarius]

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


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