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

[Peter Lammich]

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