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)
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:
Then, you can return to the default strategy, re-enabling EGC and no longer causing delays in garbage collection, as follows.
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
(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
When a second argument is supplied in a call of