On Mon, 16 Dec 2013, René Neumann wrote:

That is, have Isabelle-yyyy-x and Isabelle/Tools-yyyy-x.z with the
invariant that for every z Isabelle-yyyy-x and Isabelle/Tools-yyyy-x.z
work well together.

Again: This is just a quick idea, and I have no insight into how feasible the differentiation is, especially on the very low levels.

This would basically mean a second line of development, where problems of published versions are sorted out incrementally later on. In principle Isabelle2013-2 over Isabelle2013-1 was that already. The Coq guys also do that routinely, with 8.4, 8.4pl1, 8.4pl2, and 8.4pl3 coming out this week (they have 5 times more people working on that).

We did not do this in the past, because it is an extra effort. I am already feeling mostly alone on just the main line of Isabelle release, with more and more people just following "the" repository version and not really taking notice of the main thing: the published stable releases.

Going from Isabelle2013 to Isabelle2013-1/Isabelle2013-2 I've spent about 3 months doing some actual work, and then 3 months trying to get everything released. With a second line, this ratio would become even worse.


        Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to