Re: [isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress
On Wed, 20 Aug 2014, Lars Noschinski wrote:
On 18.08.2014 16:48, Makarius wrote:
Dear Isabelle users,
this is presumably the last release candidate before the Isabelle2014
release next week. See:
Something I noticed just now: On my machine (a quad-core i7), starting
sledgehammer (with 3 provers, from the panel) keeps the rest of the
prover from making progress. Processing the document only resumes when
sledgehammer finishes (I guess it completely exhausts the worker pool?).
As far as I understand sledgehammer it should use normal future forks
(via Par_List.map) and thus participate in the global worker thread pool.
The size of that is determined by the system option "threads", which is 0
by default, and thus determined from the hardware. You can use check this
in Isabelle/ML via Multithreading.max_threads_value. You should get 4
here, although there are i7 versions with only 2 cores.
The PIDE sledgehammer panel invokes it as "query operation", as can be
This formally documents the particular modes and parameters given to
sledgehammer. Only Jasmin understands all details of that.
With 3 provers there should be at most 3 tasks per sledgehammer invocation
-- of course there could be more than one active sledgehammer panel. The
task priority is 0, and thus higher than the -1 for forked proofs. In
addition, there could be slow "print_state" tasks at priority 1 saturating
This archive was generated by a fusion of
Pipermail (Mailman edition) and