[isabelle-dev] >>> SCHEDULER: disposed 4 dead worker threads
Makarius
makarius at sketis.net
Mon Dec 16 17:21:07 CET 2013
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
More information about the isabelle-dev
mailing list