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

[Makarius]

On 31/01/2019 18:27, Peter Lammich wrote:
> On Do, 2019-01-31 at 16:03 +0100, Makarius wrote:
>> I have looked around at typical uses of 'export_code' in AFP. Most of
>> the time it is just informative: writing a file and looking at it in
>> the
>> editor (or via the command-line!?), or doing that on the output
>> channel.
>> The isabelle-export: file-system covers that already, i.e. we should
>> be
>> able to eliminate almost all generated files from the AFP repository.
>>
>> So "export_code .. file" should just disappear -- it is semantically
>> illtyped in PIDE: editing the "file" argument will leave a trace of
>> machine oil spilled to the physical file-system.
> 
> The problem here is actually deeper: 
> Many AFP-entries are designed to export code which then works together
> with some external code. However, there seems to be no way to test
> whether this external code works with the generated code. 

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.

So far I have never seen an application that could not be made stateless
and thus fit properly into the PIDE model.


	Makarius