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

[Christian Urban]

Sorry about being a harbinger of bad news. But
this message about dead worker threads shows up 
pretty frequently with me. Though it has not caused
any problems I am aware of. 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. 

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

 Started at Sun 15 Dec 2013 11:25:22 EST (polyml-5.5.1_x86-darwin on Christians-MacBook-Air-2.local)
 ISABELLE_BUILD_OPTIONS=""
 ML_PLATFORM="x86-darwin"
 ML_HOME="/Users/cu/Desktop/Isabelle2013-2.app/Contents/Resources/Isabelle2013-2/contrib/polyml-5.5.1-1/x86-darwin"
 ML_SYSTEM="polyml-5.5.1"
 ML_OPTIONS="-H 500"

 ...
 >>> SCHEDULER: disposed 4 dead worker threads
 Timing RC (4 threads, 372.740s elapsed time, 1161.691s cpu time, 111.615s GC time, factor 3.12)
 Finished RC (0:06:41 elapsed time, 0:20:03 cpu time, factor 3.00)
 Running Slides1 ...
 Slides1: theory Slides1
 Timing Slides1 (4 threads, 1.143s elapsed time, 1.706s cpu time, 0.016s GC time, factor 1.49)
 Document at /Users/cu/Repos/rc/slides1.pdf
 Finished Slides1 (0:00:14 elapsed time, 0:00:15 cpu time, factor 1.07)
 Finished at Sun 15 Dec 2013 11:32:23 EST
 0:07:01 elapsed time, 0:20:34 cpu time, factor 2.93

This seems to me all reproducible, although with a
fourth theory I tried I do not get this message.

If I can provide any further debugging information,
please let me know.

Best wishes,
Christian 


On Friday, December 13, 2013 at 14:44:28 (+0100), Makarius wrote:
 > On Wed, 11 Dec 2013, Tobias Nipkow wrote:
 > 
 > > I just saw the above message for the first time, when building HOL-IMP. 
 > > Should this worry me?
 > 
 > Incidently I had seen the same on the same day, and asked myself the same 
 > question.  It did not come back later, though.
 > 
 > These sporadic incidents might be a problem in the session shutdown phase, 
 > i.e. a misunderstanding of Isabelle/ML vs. Poly/ML.  If it happens more 
 > frequently, I will have to look again.
 > 
 > 
 >  	Makarius
 > _______________________________________________
 > isabelle-dev mailing list
 > isabelle-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

--