Email Gateway (Aug 22 2022 at 19:41): Email Gateway (Aug 22 2022 at 19:41):From: Mathias Fleury <mathias.fleury12@gmail.com>
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
Email Gateway (Aug 22 2022 at 19:50):From: Fabian Immler <immler@in.tum.de>
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
smime.p7s
Last updated: Apr 18 2024 at 01:05 UTC