> 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 Makefiles: – 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" call it? _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
