Stream: Beginner Questions

Topic: Continuous "ML Cleanup"


view this post on Zulip Alex (Mar 22 2021 at 07:34):

I have many "by auto"-proofs that use up a lot of memory. As soon as ML reaches about 8GB (I have 16GB RAM), a "ML cleanup" is performed after every single line in my theory, which in total takes up far more time than the actual proofs. Is there a way to adjust the memory limits or GC frequency?

view this post on Zulip Mathias Fleury (Mar 22 2021 at 07:42):

In theory, you can adjust the min-heap of PolyML. Add to $ISABELLE_HOME/etc/settings

ML_OPTIONS="--minheap 10G"

restart Isabelle, and try. That could backfire however (GCs become slower)

view this post on Zulip Mathias Fleury (Mar 22 2021 at 07:42):

Not sure if that helps though

view this post on Zulip Mathias Fleury (Mar 22 2021 at 07:44):

Other alternatives are splitting the file or changing the proofs…

view this post on Zulip Mathias Fleury (Mar 22 2021 at 07:52):

More generally, I always found that the garbage collector behave strangely in SML (both PolyML and MLton): Not eager enough to allocate memory past 50% of memory (including cases where GC will take up most of the runtime…), but also not eager enough to deallocate memory for low memory usage (in percentage again: Isabelle/polyml can use 50GB if the server has 1TB RAM… completely useless)

view this post on Zulip Alex (Mar 22 2021 at 08:07):

Thank you! Adjusting the limit this way worked. And, just as you said, raising it too much backfires immediately. I will experiment with different values to find what works best in my case.


Last updated: Mar 28 2024 at 08:18 UTC