terru (Oct 07 2025 at 08:45): terru (Oct 07 2025 at 08:45):Recently it has happened to me several times that the prover appears to "hang" in large projects, i.e. it initially gets stuck somewhere (perhaps in a long-running or non-terminating auto) and then doesn't seem to recover — even after removing the faulty invocation & waiting for quite a while, jedit seems to no longer get "updates" on the document state from the prover, so while editing still works, new proofs won't be checked (nor terms type-checked, etc.).
Is this a known problem, and is there a better way of dealing with this than restarting all of jedit (& potentially having to re-check a large number of theories?). I've built heap images for parts of the project to at least reduce the cost of restarting, but that's only a stopgap solution ..
Lukas Stevens (Oct 07 2025 at 13:10):This has been discussed before, see for example #Mirror: Isabelle Users Mailing List > [isabelle] Heavy memory use with sledgehammer.
Unfortunately, this is a known issue that is probably related to memory leakage. You can improve the situation somewhat using a fine-grained session structure, preferring Isar proofs over apply scripts, or, ultimately, buying more powerful hardware.
Lukas Stevens (Oct 07 2025 at 13:12):Also see #Beginner Questions > ML memory usage goes up
Mathias Fleury (Oct 07 2025 at 15:10):polyml's garbage collection is also prone to this
Mathias Fleury (Oct 07 2025 at 15:11):or at least was
Mathias Fleury (Oct 07 2025 at 15:11):(I rarely do whole-day Isabelle anymore)
Mathias Fleury (Oct 07 2025 at 15:11):but look at the system panel in Isabelle/jEdit, how much heap is left
Mathias Fleury (Oct 07 2025 at 15:12):But the solution is the same: restarting
terru (Oct 07 2025 at 15:14):well that's annoying, then; dealing with this is currently slowing down my work quite a bit (but thanks for the information to both of you!)
Last updated: Oct 08 2025 at 20:22 UTC