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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
