oops
Major Section: HISTORY
By default, ACL2 holds on to old logical worlds when you undo
commands (see ubt), as documented elswhere; see oops. You can free up
memory by deleting those old worlds using reset-kill-ring
.
Examples: (reset-kill-ring t state) ; replace each element of the kill ring by nil (reset-kill-ring 2 state) ; create a new kill ring of '(nil nil) (reset-kill-ring 0 state) ; create a new kill ring that is empty (reset-kill-ring nil state) ; just return the length of the kill ringwhereGeneral form: (reset-kill-ring n state)
n
evaluates either to t
, to nil
, or to a nonnegative
integer (a natp
). If n
evaluates to t
, it is treated as the
length of the current kill ring. If n
is nil
, then the length k
of the current kill ring is returned as a value triple (mv nil k state)
.
If n
is a natp
, then the kill ring is replaced with a list of n
nil
s.
In particular, use (reset-kill-ring 0 state)
to avoid saving any old
logical worlds, at the cost of disabling the effect of the oops
command.