On 01/02/2019 12:43, Lars Hupel wrote: > > 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.
In 2012 we eliminated all Makefiles from AFP: I did not know that some came back, or chose to ignore it. The formal status of sessions is defined via "isabelle build" -- that is a powerful tool that can do many things. I.e. we can easily define that anything outside of it as outside of AFP. As usual, the empirical proof of this claims works by going through the applications seen in practice, and to reform them to make them fit to the model. (This sometimes requires minor adjustments of the model.) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev