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

[Makarius]

On 01/02/2019 12:43, Lars Hupel wrote:
> 
> It would like to reiterate that the technical part of this issue is the
> easy bit. The difficult bit is deciding policy: Should Isabelle
> committers be responsible for breakage in downstream artifacts? In other
> words, should the AFP stability guarantees be extended? Right now we
> have that odd situation where extra sources are present (e.g. Makefiles)
> but nobody bothers to look at them.

In 2012 we eliminated all Makefiles from AFP: I did not know that some
came back, or chose to ignore it.

The formal status of sessions is defined via "isabelle build" -- that is
a powerful tool that can do many things. I.e. we can easily define that
anything outside of it as outside of AFP.

As usual, the empirical proof of this claims works by going through the
applications seen in practice, and to reform them to make them fit to
the model. (This sometimes requires minor adjustments of the model.)


	Makarius