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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
