Alex (Mar 05 2021 at 10:13): 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?
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.
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.
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: Apr 16 2024 at 16:19 UTC