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

[Lars Hupel]

> 1. Gratchk is a similar use-case, where I need to export code, link it
> with some external ML code using MLton b/c it's faster, and test the
> result for timing regressions. Because gratchk is also bundled with
> gratgen, which is implemented in C++, I have not yet put it into the
> AFP, b/c that would mean to separate gratchk from gratgen, or to push
> C++ code to the AFP, for which I cannot expect an build infrastructure
> there.
> 
> 2. In the AFP, there is the CAVA model checker. It also comes with some
> external ML code. I just checked, and this external ML code is already
> severely bit-rotten, as it has not been maintained for years now ... at
> latest the recent string-literal reform should have reliably killed it.
>  
> Also, timing regression tests are important when doing such reforms as
> the above-mentioned string-literal reform, which has the potential to
> severely slowdown the generated code.

This is not a new problem. It is merely slightly exacerbated by making
it more difficult to run such tests manually. There have been various
discussions about this in the past, but they are all orthogonal to the
issue of code generation.

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.

Cheers
Lars