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:

  http://isabelle.in.tum.de/website-Isabelle2014-RC4
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 seen here:

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2014-RC4/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML#l455

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 the queue.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.