Abort-soft
Control how interrupts are handled in proofs
ACL2 arranges by default that when a proof is interrupted (with
Control-C), a ``soft'' abort occurs in the following sense: the message
below is printed and then the proof attempt continues temporarily before
ultimately failing (usually very soon thereafter).
***********************************************
Note: interrupt signal
Will attempt to exit the proof in progress;
otherwise, the next interrupt will abort the proof.
For an immediate abort see :DOC abort-soft.
***********************************************
This default behavior supports proper operation of the utility, redo-flat, when a proof is interrupted. It also supports more complete
summaries than would be obtained with an immediate abort. If you nevertheless
want proofs to abort immediately, you may evaluate the form (assign
abort-soft nil). To restore the default behavior, evaluate (assign
abort-soft t).
Remarks for system hackers.
- An important effect of having evaluated (assign abort-soft nil) is
that an interrupt will send you immediately back to the ACL2 read-eval-print
loop, in contrast to the default behavior where the prover returns an error-triple whose error component is non-nil.
- It may be preferable to bind state global abort-soft rather
than to assign it globally. See the implementation of prove$ (specifically, the definition of prove$-fn in community-book books/tools/prove-dollar.lisp) for an example.
