		Search-engine friendly clone of the ACL2 documentation.

Set-gc-strategy

Set the garbage collection strategy (CCL only)

Note: This macro has no effect unless the host Lisp is CCL.

General Forms:

(set-gc-strategy :egc)     ; the default: EGC is on, full GC is not delayed
(set-gc-strategy :delay)   ; EGC is off, full GC is delayed
(set-gc-strategy :current) ; same as replacing :current by the latest
                           ; strategy set (:egc or :delay)

(set-gc-strategy strategy threshold)
                           ; Same as (set-gc-strategy strategy), but sets
                           ; threshold to the indicated number of bytes
                           ; (see below)

Logically, (set-gc-strategy op) returns op. But in some host Lisps (currently CCL only), it changes how garbage collection is invoked. Exactly how that is done is best understood by reading the ACL2 source code, starting with set-gc-strategy. Here we document what most users might want to know about this utility, assuming they are using CCL. We defer discussion of the optional second argument, threshold, to the end.

Normally the default garbage collection strategy will probably be fine. That default has the ephemeral garbage collector (EGC) enabled. But in jobs that stress hons, or perhaps memoization (see memoize) or fast-alists, it might be useful to switch to a strategy that disables EGC but also significantly delays garbage collection. To switch to that delaying strategy:

(set-gc-strategy :delay)

Then, you can return to the default strategy, re-enabling EGC and no longer causing delays in garbage collection, as follows.

(set-gc-strategy :egc)

It is also legal to invoke (set-gc-strategy :current), which is equivalent to replacing :current by the current strategy; see gc-strategy.

If you want to change the gc-strategy during certification of a book, but not when including that book, you can place your call of set-gc-strategy inside value-triple, for example as follows.

(value-triple (set-gc-strategy :delay))

The following variant causes the gc-strategy to be modified when including the book as well.

(value-triple (set-gc-strategy :delay) :on-skip-proofs t)

This capability might be extended to other host Lisps in the future, especially if ACL2 users provide suggestions for how to do so.

Note that the default behavior can be changed to :delay at ACL2 build time, by setting Make variable ACL2_EGC_ON=nil when building an ACL2 executable.

The threshold argument

When a second argument is supplied in a call of set-gc-strategy, it must be either nil, which is equivalent to supplying no second argument, or else a positive integer. This positive integer will be the ``GC threshold'' number of bytes CCL will try to ensure are available before the next full garbage collection. The default (i.e., the value used when the second argument is nil or is omitted) is the minimum of the following two values: 1/2 GB, and 1/32 of physical memory (or 1/32 of 4 GB, if the physical memory cannot be determined). (Technical note: The GC threshold is stored in raw Lisp variable *gc-min-threshold*.)