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 \ / w2 and the current
ACL2 world is
w0 once again. That is,
:oops ``undoes'' the
w0. Similarly, a second
:oops will move the
w1, undoing the undo that produced
w1. A third
w2 the current world. Note however that a fourth
restores us to the configuration above.
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