Redo-flat
Redo on failure of a progn, encapsulate, or certify-book
When one submits an encapsulate, progn, or certify-book command and there is a failure, ACL2 restores its logical world as though the command had not been run. But sometimes one would like
to debug the failure by re-executing all sub-events that succeeded up to the
point of failure, and then re-executing the failed sub-event. Said
differently, imagine that the events under an encapsulate,
progn, or certify-book form were flattened into a list of events
that were then submitted to ACL2 up to the point of failure. This would put
us in the state in which the original failed event had failed, so we could now
replay that failed event and try modifying it, or first proving additional
events, in order to get it admitted.
Redo-flat is provided for this purpose. Consider the following
(rather nonsensical) example, in which the defun of f3 fails (the
body is y but the formal parameter list is (x)).
(encapsulate
()
(defun f1 (x) x)
(encapsulate ()
(local (defthm hack (equal (car (cons x y)) x))))
(encapsulate ()
(local (defthm hack (equal (+ x y) (+ y x)))))
(encapsulate ()
(make-event '(defun f2 (x) x))
(progn (defthm foo (equal x x) :rule-classes nil)
(defun f3 (x) y)))
(defun f4 (x) x)
(defun f5 (x) y))
After this attempt fails, you can evaluate the following form.
(redo-flat)
This will first lay down a deflabel event, (deflabel r), so
that you can eventually remove your debugging work with (:ubt! r). Then
the successful sub-events that preceded the failure will be executed with
proofs skipped (so that this execution is fast). Then, the failed event will
be executed. Finally, a :pbt command is executed so that you can
see a summary of the events that executed successfully.
You can eliminate some of the steps above by supplying keyword values, as
follows, where those arguments are not evaluated.
(redo-flat
:succ succ ; Skip the successful sub-events if val is nil.
:fail fail ; Skip the failed sub-event if val is nil.
:label lab ; Skip deflabel if lab or succ is nil, else use (deflabel lab).
:pbt val ; Skip the final :pbt if val, lab, or succ is nil.
)
Also, you can avoid skipping proofs for the successful sub-events by
supplying keyword :succ-ld-skip-proofsp with a valid value for
ld-skip-proofsp; see ld-skip-proofsp. For example, you might want
to execute (redo-flat :succ-ld-skip-proofsp nil) if you use the
must-fail utility from community book make-event/eval.lisp, since
for example (must-fail (thm (equal x y))) normally succeeds but would
cause an error if proofs are skipped. For another example: you may wish to do
proofs when re-running certain make-event forms, for example, when the
expansion is (:OR expr1 expr2) and the proof initially succeeds for
expr2 rather than expr1 (see make-event).
If you prefer only to see the successful and failed sub-events, without any
events being re-executed, you may evaluate the following form instead.
(redo-flat :show t)
For the example above, this command produces the following output.
List of events preceding the failure:
((DEFUN F1 (X) X)
(ENCAPSULATE NIL
(LOCAL (DEFTHM HACK (EQUAL (CAR (CONS X Y)) X))))
(ENCAPSULATE NIL
(LOCAL (DEFTHM HACK (EQUAL (+ X Y) (+ Y X)))))
(MAKE-EVENT '(DEFUN F2 (X) X))
(DEFTHM FOO (EQUAL X X)
:RULE-CLASSES NIL))
Failed event:
(DEFUN F3 (X) Y)
ACL2 !>
Redo-flat uses a scheme that should not cause spurious name conflicts
for local events. Above, it is mentioned that events are
``flattened''; now we clarify this notion. Each sub-event that succeeds and
is an encapsulate or progn is left intact. Only such events
that fail are replaced by their component events. Thus, in the example above,
there is no conflict between the two local sub-events named
``hack,'' because these are contained in successful encapsulate
sub-events, which are therefore not flattened. The progn and two
encapsulate events surrounding the definition of f3 are, however,
flattened, because that definition failed to be admitted.
Normally, redo-flat will have the desired effect even if you
interrupted a proof (with control-c). However, redo-flat will not
produce the desired result after an interrupt if you have enabled the debugger
using (set-debugger-enable t) or if you have disabled the default
``soft'' interrupt behavior (see abort-soft).
