Re: [isabelle] Isabelle2019-RC2 non-terminating commands and memory consumption



Hi Fabian,


I don't think that this is a new behaviour. So far, I even thought that this was part of the Isabelle experience. 


I see things like that on a daily base (both on macOS and linux) — at least when I use Isabelle/jEdit. I am forced to restart Isabelle at least once a day due to issues like that. In my experience, it is independent of the base session and waiting does not help (it is faster to restart Isabelle/jEdit, whatever the size of the development).



Best regards,
Mathias



> On 14. May 2019, at 11:53, Fabian Immler <immler at in.tum.de> wrote:
> 
> This is very vague feedback, but it seems like it is relatively easy to drive Isabelle2019-RC2 into a state where Isabelle/jEdit becomes extremely slow and unresponsive.
> 
> I encountered this while fixing some theories based on AFP/Affine_Arithmetic. I think problems were caused by non-terminating commands (somewhere below my current edits).
> 
> I tried to reproduce this with the attached Scratch.thy, and the behavior seems similar.
> 
> Below is a trace of my edits, where I stands for an edit that invalidates most of the buffer ("lemma" -> "le mma") and V stands for reversing that edit. I took a screenshot of the Heap-Monitor panel after 750s, then Reset the panel and continued with edits for another 650 seconds.
> Especially after 750s, performance degrades a lot. Also the graph looks very different (e.g., the blue size_allocation does not decrease anymore).
> 
> The performance degradation is probably just general memory pressure on the system, but what I find disturbing is that the end of this experiment, I am left with a "theory Scratch imports Pure begin end" that does not seem like it will reduce the size_heap of 14GB anymore and is almost impossible to work with.
> 
> I am using Windows 10 on a laptop with a 6-core i7 processor and 32GB of RAM.
> 
> Best regards,
> Fabian
> 
> 12: V
> 75: I
> 133: V
> 230: I
> 240: V
> 330: I
> 340: V
> 410: I
> 412: V
> 690: I
> 715: V
> 750: I
> Screenshot 1
> Reset
> 15: V
> 115-230: I, no response
> 265: V
> 280: I
> no response until 295
> 320: V
> 340: I, no response for 3 s
> 360: V
> 365: I
> 380: V
> 400: I, no response for 40 s
> 485: V
> 490: I
> 505: V
> 510: I
> 560: V
> 600-650: I, no response
> 750: Screenshot 2
> <Scratch.thy><Screenshot 2.PNG><Screenshot 1.PNG>





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