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. There is the "checking"-option, which will test the generated code in isolation. But any external code that is supposed to interface with the generated code is left to bit-rotting. -- Peter _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev