[isabelle-dev] Max threads & Sledgehammer

[Stefan Berghofer]

On 01/04/2013 01:37 PM, Jasmin Blanchette wrote:
> Hi Makarius,
>
> Change cb5cdbb645cd ("clarified bootstrapping of Pure") altered the semantics of
>
>      Multithreading.max_threads_value ()
>
> with Poly/ML. Namely, all of a sudden the function returns 1 instead of 4 on a 4-CPU machine, which seems strage as a default for a function called "max_threads_value". As a result, Sledgehammer launches only one local thread -- see "avoid_too_many_threads" and its use in "src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML". SPASS is then no longer run at all.
>
> This has been like this for some time now. I failed to notice the issue because I had overwritten the number of threads via a Proof General setting.
>
> This really needs to be fixed before the release -- either in "multithreading_polyml.ML" or in "sledgehammer_isar.ML".

Hi Markus,

I am not sure if this is related to the above bug, but 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. To avoid this problem, I
tried to limit the number of threads by adding

   ISABELLE_BUILD_OPTIONS="threads=n"

to my .isabelle/etc/settings file (for a suitable value of n), but that didn't
seem to have any effect.

Any ideas?

Greetings,
Stefan