On Fri, 4 Jan 2013, Stefan Berghofer wrote:
I am currently getting an exception Thread "Thread creation failed"
after some time when compiling HOL with PolyML 5.5.0 on a machine with
quite a few CPUs (I am using Isabelle repository version 30bcdd5c8e78).
I have the impression that Isabelle just tries to create as many threads
as there are CPUs, which exceeds the maximum number of threads allowed
by the operating system for a single process.
Can you say more about the hardware and operating system here? How many
CPUs do you have?
I've seen problems creating threads on the JVM (e.g. see f7ba30a816b9),
but not for Poly/ML 5.5.0. Also note that the default (threads=0) is
bounded by 8 at the moment.
What could happen here nonetheless is that Poly/ML tries to fork too many
GC threads. So how many cores do you have? I reckon it should work
until 32 at the least. You could try ML_OPTIONS="--gcthreads 8" in one of
your settings.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
