During long editing sessions in JEdit the ML memory usage (as reported in the JEDIT Status bar) tends to go up until it fills up my whole RAM and terminates (gracefully). Even an explicit GC doesn't bring it down. However, if I restart JEdit and let it prove everything, the resulting memory usage is far lower. I guess I can't fix the leak itself, but I would like to try a workaround: Is there a way for me to tell Isabelle (or JEdit or whatever is responsible for that) to forget intermediate proof steps after a lemma is proved? This would free up a significant chunk of memory, I guess. I'm only interested in the intermediate steps within the lemma I'm currently working on. Or, as an alternative workaround: Can I tell Isabelle/JEdit to assume all statements in other theories are true, and only prove the current theory?

It is hard to know if anything can help besides investing money in a new computer... The most important: create a sessions, i.e., create a ROOT file for your theories. Combined with `isabelle jedit -R <my_session>`

all base sessions are compiled. But you cannot edit them anymore.

Also Isar proofs help. Avoid `apply X apply Y`

. Prefer `by X Y`

. Also better for parallelization.

Ok, thank you. I'll definitely try using a session. This might already be sufficient to solve my problem. As for the proofs: I'm using "subgoal" and "by" quite furiously. But I'll take another look at Isar proofs in the hope of simplifying some long running proofs. Again, thanks!

Last updated: Sep 25 2021 at 09:17 UTC