[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