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



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?


	Makarius




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