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 ring General form: (reset-kill-ring n state)where
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
nils.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.
