Hi Makarius,

> On 31. Jan 2019, at 20:10, Makarius <makar...@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.


* 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-...@in.tum.de <mailto:isabelle-...@in.tum.de>
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
> <https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev>
isabelle-dev mailing list

Reply via email to