[isabelle-dev] Max threads & Sledgehammer

[Makarius]

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