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