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