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

[Makarius]

On 01/02/2019 14:29, Lars Hupel wrote:
>> In 2012 we eliminated all Makefiles from AFP: I did not know that some
>> came back, or chose to ignore it.
> 
> ~/work/afp (default)$ find thys/ -name Makefile
> thys/Buchi_Complementation/code/Makefile
> thys/Formal_SSA/Makefile
> thys/LightweightJava/ott-src/Makefile
> thys/Sturm_Sequences/guide/Makefile

What are the remaining uses of these? How much of this can be integrated
into the formal Isabelle session? How much of it is actually obsolete?


We have plenty of mechanisms in "isabelle build" (and "isabelle
process") that are waiting to be put into proper use.

>From a maintenance point of view the goals are:

  * no generated files in the repository (these are not sources but
results from sources)

  * no violations of the stateless PIDE model, e.g. commands that leave
a trace of garbage in the natural environment while editing (such as
"export_code ... file ..." with varying file names).


In principle, everything should work on a read-only file-system.


	Makarius