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 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 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.

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 evaluting (reset-kill-ring 0 state); see reset-kill-ring.