[isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress



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?).




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