*To*: Fabian Immler <immler at in.tum.de>*Subject*: Re: [isabelle] Isabelle2019-RC2 non-terminating commands and memory consumption*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Wed, 22 May 2019 10:57:58 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <47c3c121-9ffc-1a2c-8644-86b2d6a21f90@in.tum.de>*References*: <47c3c121-9ffc-1a2c-8644-86b2d6a21f90@in.tum.de>

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>

**References**:**[isabelle] Isabelle2019-RC2 non-terminating commands and memory consumption***From:*Fabian Immler

- Previous by Date: [isabelle] Schematic and universally quantified variables in forward proofs
- Next by Date: Re: [isabelle] Isabelle2019-RC2 NullPointerException on Cygwin-Terminal (Windows 10)
- Previous by Thread: [isabelle] Isabelle2019-RC2 non-terminating commands and memory consumption
- Next by Thread: [isabelle] R: Isabelle2019-RC2 sporadic smt failures
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list