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 pool.
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

    sledgehammer_params [mepo]

at the top of your theory should take care of (1).
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).

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 clues.

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.


	Makarius




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