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



On 26.08.2014 12:08, Makarius wrote:
> On Sat, 23 Aug 2014, Lars Noschinski wrote:
>
>>> 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
>
> Thanks for the video.  After watching it 2 times, I could see the
> pattern when this sitation occurs, and managed to reproduce it without
> anything particular from sledgehammer, just using some
> OS.Process.sleep dummies.
>
> I am presently investigating the reasons for this behaviour of PIDE
> document scheduling, which could well be just a normal consequence of
> certain heuristics in task priorities that have accumulated over time.
>
> For now: How would you rate the practical relevance and priority of
> this issue?  Is it just a minor oddity or outright a hindrance in
> practical work?
Somewhere in between. It is annoying since it essentially sequentializes
the behavior of the IDE, but it is no showstopper.

  -- Lars




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