On 01/02/2019 15:30, Lars Hupel wrote: > >> * 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?
The present reform is mainly about generated output files, not input theory files. The standard approach for the latter is to have the other tool directly import its source format into the theory context within Isabelle/ML, without the intermediate theory source. Doing this carefully, would even produce nice PIDE markup for the original sources. PIDE is an IDE for arbitrary user-defined languages. It might be worth doing this for tools like Lem eventually, but I have not looked at it closely so far. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev