Re: [isabelle] Isabelle2014-RC4: sledgehammer blocks all other progress
On 22.08.2014 16:10, Makarius wrote:
>>> 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.
Multithreading.max_threads_value () is 4. I made a video of what I am
experiencing. Notice that the pink background goes away immediately when
I cancel sledgehammer:
(Don't be alarmed by the mouse cursor offset problem -- it only occurs
in the video).
This archive was generated by a fusion of
Pipermail (Mailman edition) and