Major Section: HISTORY
The keyword command
:oops will undo the most recent
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
Consider the logical world (see world) that represents the
current extension of the logic and ACL2's rules for dealing with it.
: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 is best described in terms of an implementation. Imagine a
ring of four worlds and a marker (
*) indicating the current ACL2
* w0 / \ w3 w1 \ / w2This 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
: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
w0 / \ *w0' w1 \ / w2If 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
* w0 / \ w0' w1 \ / w2and the current ACL2 world is
w0once again. That is,
w0. Similarly, a second
:oopswill move the marker to
w1, undoing the undo that produced
w1. A third
w2the current world. Note however that a fourth
:oopsrestores 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
:u were done.
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.
ubt does discard information!
Ubt discards the information
necessary to recover from the third most recent
the other hand, discards no information, it just selects the next
available world on the kill ring and doing enough
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
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
ubt seem ``safe'' because the
ubt can always be undone, information is lost when you
We note that
: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
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 evaluting
(reset-kill-ring 0 state);