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

[Makarius]

On Sun, 15 Dec 2013, Christian Urban wrote:

> My guess is that I notice this message already for at least a year. It 
> is in fact so frequent that I assumed this is normal behaviour of 
> Isabelle.

So just one more thing on the long list of open problems that nobody dared 
to report or cared about.

The big problem of Isabelle2013-1 was a lack of serious testing towards a 
truly stable release, but I misinterpreted the lack of problem reports as 
absence of problems.  Isabelle2013-2 is a bit better, but not really there 
-- right *after* the release I've got again further observations about 
certain oddities that were already there at the start of the RC phase 8 
weeks ago.

These are not complaints, just some observations that the Isabelle release 
process no longer works realiably.  I am also lacking first-hand 
power-users, whom I can watch over the shoulder.


> I just tried it out with tree different theories, with
> Isabelle-2013-1 and also Isabelle-2013-2; in all
> instances I got a message like
>
> > isabelle build -c -v -d . Slides1
>
> ...
> >>> SCHEDULER: disposed 4 dead worker threads

My impression over the years: in *rare* situations the basic heap image is 
built in a bad way such that the crash of the worker threads happens after 
loading it again.  In that case one needs to build the image again.

If this incident now happens routinely, I need to look very closely at the 
gloabl thread management.  It is not a real problem though, just an 
oddity: the future scheduler notices a dirty situation and clears out the 
state.


 	Makarius