> On 1. Feb 2019, at 15:30, Lars Hupel <hu...@in.tum.de> wrote: > >> 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.
To add a couple more to the list: — LTL has includes a parser that is used in an example and built using LTL/examples/build_poly.sh — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh and LTL_to_DRA/Code/build_mlton.sh Best, Salomon >> * 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
