Conditionally trigger a hons-wash and also clear-memoize-tables to reclaim memory. (CCL only; requires a trust tag)
(maybe-wash-memory n &optional clear) will clear out unused honses and throw
away all currently memoized results, but only if fewer than
The general idea here is that garbage collection is slow, so you only want to do it if you are starting to run out of memory. At the same time, garbage collection is cheaper if you can do it "in between" computations that are creating a lot of garbage, where there are fewer live objects. Moreover, if you still have a lot of memory still available, then you may prefer to keep currently memoized results so that you aren't repeating work.
You can use
Here's a basic example:
(include-book "centaur/misc/memory-mgmt" :dir :system) ;; adds ttag (value-triple (set-max-mem (* 8 (expt 2 30)))) ;; 8 GB ... some memory intensive stuff ... (value-triple (maybe-wash-memory (* 3 (expt 2 30)))) ... more memory intensive stuff ... (value-triple (maybe-wash-memory (* 3 (expt 2 30)))) ... etc ...
If the optional
This can be a good way to clean up memory in between def-gl-param-thm cases, and in other situations.