Stream: Beginner Questions

Topic: ML memory usage goes up

view this post on Zulip Alex (Mar 05 2021 at 10:13):

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?

view this post on Zulip Mathias Fleury (Mar 05 2021 at 16:25):

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.

view this post on Zulip Mathias Fleury (Mar 06 2021 at 06:03):

Also Isar proofs help. Avoid apply X apply Y. Prefer by X Y. Also better for parallelization.

view this post on Zulip Alex (Mar 06 2021 at 11:12):

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