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