Re: [isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress
On Fri, 22 Aug 2014, Lars Noschinski wrote:
On 22.08.2014 12:32, Jasmin Christian Blanchette wrote:
As far as I understand sledgehammer it should use normal future forks
(via Par_List.map) and thus participate in the global worker thread
With the Sledgehammer panel, all threads should participate in the
global worker thread pool, with the potential exception of a single
MaSh learning thread (occasionally -- e.g. the first time you launch
Sledgehammer and MaSh has no accumulated state) -- the MaSh threads are
managed using the old "asynchronous manager" mechanism, that is also
used when invoking the "sledgehammer" command from the proof text.
In the worst case that extra thread would suck up more CPU cycles than
specified in the nominal "threads" option, but it should not stop regular
future tasks from running, like the ones for forked proofs.
It would be useful to know if the problem also occurs when (1) MaSh is
not run and (2) no proofs are found (and hence no proof minimization
etc. and hence no "Par_List" operations, IIRC). Adding
When I add "sledgehammer_params [mepo]" before the place where I call
sledgehammer, the problem persists. Also, all provers timed out, so the
problem occurs also with (2).
at the top of your theory should take care of (1).
It is still unclear to me what the problem is. What does
Multithreading.max_threads_value () say? How is the task farm pupulated?
The improved Monitor dockable in Isabelle2014-RC4 might provide some
We have only a few days left to figure out if there is a remaining problem
or not. The month of August ends next week, and the final roll-out of
Isabelle2014 will happen before that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and