[isabelle-dev] Max threads & Sledgehammer
makarius at sketis.net
Mon Jan 7 10:36:44 CET 2013
On Fri, 4 Jan 2013, 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
date: Mon Jan 07 10:17:11 2013 +0100
slightly odd duplication of Pure options for Proof General (amending
The above change cb5cdbb645cd from 22-Aug-2012 is a typical Proof General
casualty, a consequence of myself starting the thing extremely rarely now.
So the remaining Proof Generaly guys have to look more closely themselves.
The deeper technical issue behind it is a divergence of "options":
Isabelle/Scala provides an official concept for that since last summer,
but not all sub-systems use it uniformly at the moment (not just Proof
More information about the isabelle-dev