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:

    http://www21.in.tum.de/~noschinl/ml/sledgehammer-blocks.mp4

(Don't be alarmed by the mouse cursor offset problem -- it only occurs
in the video).

  -- Lars




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