		Search-engine friendly clone of the ACL2 documentation.

Hons

Maybe-wash-memory

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 n bytes of memory are currently free. If more than n bytes are free, it does nothing.

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 maybe-wash-memory in between computations to trigger garbage collections in an opportunistic way: if there's ample memory still available, no GC will be triggered, but if memory is getting scarce, then it's time to trigger an expensive collection, wiping out the memo tables and cleaning up honses in the process.

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 clear argument is t, honses will be cleared using hons-clear instead of hons-wash. (This is generally ill advised.)

This can be a good way to clean up memory in between def-gl-param-thm cases, and in other situations.