[isabelle-dev] NEWS: generated code as proper theory export
hupel at in.tum.de
Fri Feb 1 15:30:31 CET 2019
> 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?
Hard to tell from a distance, but here's what I gather from reading the
– Formal_SSA appears to download some file, unpack it, and compile
generated code together with it.
– Lightweight_Java generates an Isabelle theory file with Ott.
– Buchi_Complementation compiles generated code with MLton.
– Sturm_Sequences produces some extra LaTeX documentation. The generated
PDF is even committed to the AFP.
> * no generated files in the repository (these are not sources but
> results from sources)
What about generated theory files? This also affects the CakeML entry. I
could easily package Lem as a component, but how would "isabelle build"
More information about the isabelle-dev