[isabelle-dev] Max threads & Sledgehammer

Jasmin Blanchette jasmin.blanchette at gmail.com
Fri Jan 4 13:37:05 CET 2013

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



More information about the isabelle-dev mailing list