OOPS

undo a :u or :ubt 
Major Section:  HISTORY

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: 

             *
           w0 
         /    \
       w3      w1
         \    /
           w2
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. 
           w0 
         /    \
      *w0'     w1
         \    /
           w2
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 * w0 / \ w0' w1 \ / w2 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 above.

In general, the kill ring contains the current world and the three most recent worlds in which a :ubt or :u were done.

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.