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



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
theory Scratch
  imports
    Pure
begin

le mma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

lemma "x \<equiv> x"
  by (rule ?)+

end

Attachment: Screenshot 2.PNG
Description: PNG image

Attachment: Screenshot 1.PNG
Description: PNG image

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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