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

[Mathias Fleury]

Hi Makarius,

> On 31. Jan 2019, at 20:10, Makarius <makarius at sketis.net> wrote:
> 
> 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.

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.


Mathias


* Last time I tried, MLton was an order of magnitude faster than Poly/ML. But I can rewrite the parser for Poly/ML.

> 
> 
> 	Makarius
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de <mailto:isabelle-dev at in.tum.de>
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev <https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190131/900cb953/attachment-0002.html>