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:
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and