[isabelle-dev] NEWS: generated code as proper theory export
mathias.fleury12 at gmail.com
Thu Jan 31 20:37:48 CET 2019
> 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
>>> editor (or via the command-line!?), or doing that on the output
>>> The isabelle-export: file-system covers that already, i.e. we should
>>> 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.
> 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...
More information about the isabelle-dev