[isabelle-dev] >>> SCHEDULER: disposed 4 dead worker threads
christian.urban at kcl.ac.uk
Sun Dec 15 01:42:47 CET 2013
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
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)
>>> 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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev