[isabelle-dev] >>> SCHEDULER: disposed 4 dead worker threads

Tobias Nipkow nipkow at in.tum.de
Mon Dec 16 17:49:39 CET 2013


Am 16/12/2013 17:21, schrieb Makarius:
> 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.

I suspect the mailing list gives a skewed picture because the most vocal people
on it are the power users who tend to follow the development closely. But having
a stable release is absolutely essential and your work on it is highly
appreciated. I hope/assume you are aware of this. (I know that this is not
exactly what you were talking about.)

Tobias

> 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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 



More information about the isabelle-dev mailing list