[isabelle-dev] Max threads & Sledgehammer

[Makarius]

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 
> setting.

See now

changeset:   50757:37091451ba1a
tag:         tip
user:        wenzelm
date:        Mon Jan 07 10:17:11 2013 +0100
files:       src/Pure/ROOT.ML
description:
slightly odd duplication of Pure options for Proof General (amending 
cb5cdbb645cd);

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 
General).


 	Makarius