Undo a :u or :ubt
The keyword command :oops will undo the most recent
:ubt (or :u, which we here consider just another
:ubt). A second :oops will undo the next most recent
:ubt, a third will undo the :ubt before that one,
and a fourth :oops will return the logical world to its
configuration before the first :oops.
Consider the logical world (see world) that represents the current
extension of the logic and ACL2's rules for dealing with it. The :ubt and :u commands ``roll back'' to some previous world
(see ubt). Sometimes these commands are used to inadvertently
undo useful work and user's wish they could ``undo the last undo.'' That is
the function provided by :oops.
:Oops is best described in terms of an implementation. Imagine a ring
of four worlds and a marker (*) indicating the current ACL2 world:
This is called the ``kill ring'' and it is maintained as follows. When you
execute an event the current world is extended and the kill ring is not
otherwise affected. When you execute :ubt or :u, the
current world marker is moved one step counterclockwise and that world in the ring is replaced by the result, say w0', of the
:ubt or :u.
If you were to execute events at this point, w0' would be
extended and no other changes would occur in the kill ring.
When you execute :oops, the marker is moved one step clockwise. Thus
the kill ring becomes
and the current ACL2 world is w0 once again. That is,
:oops ``undoes'' the :ubt that produced w0' from
w0. Similarly, a second :oops will move the marker to w1,
undoing the undo that produced w0 from w1. A third :oops makes
w2 the current world. Note however that a fourth :oops
restores us to the configuration previously displayed above in which w0'
has the marker.
In general, the kill ring contains the current world and the three
most recent worlds in which a :ubt or :u were
While :ubt may appear to discard the information in the events undone, we can see that the world in which the :ubt occurred is still available. No information has been lost about that
world. But :ubt does discard information! :Ubt discards the information necessary to recover from the third most recent
ubt! An :oops, on the other hand, discards no information, it
just selects the next available world on the kill ring and doing enough
:oopses will return you to your starting point.
We can put this another way. You can freely type :oops and inspect
the world that you thus obtain with :pe, :pc,
and other history commands. You can repeat this as often as you
wish without risking the permanent loss of any information. But you must be
more careful typing :ubt or :u. While :oops makes
:ubt seem ``safe'' because the most recent :ubt can
always be undone, information is lost when you execute :ubt.
We note that :ubt and :u may remove compiled definitions (but
note that in some Lisps, including CCL (OpenMCL) and SBCL, functions are
always compiled). When the original world is restored using :oops,
restored functions will not generally be compiled (except for Lisps as above),
though the user can remedy this situation; see comp.
Finally, we note that our implementation of oops can use a significant
amount of memory, because of the saving of old logical worlds. Most
users are unlikely to experience a memory problem, but if you do, then you may
want to disable oops by evaluating (reset-kill-ring 0 state); see