Break-on-error
Break when encountering a hard or soft error caused by ACL2
General forms:
(break-on-error t) ; installs a trace causing a continuable error (break)
; when an error is invoked by ACL2.
(break-on-error) ; same as above
(break-on-error :all) ; same as above, but even when inside the prover
(break-on-error nil) ; uninstall any above trace
Evaluation of (break-on-error :all) generates a suitable trace
of error functions, so that the Lisp debugger is entered whenever ACL2 calls
them. You can then continue the interrupted computation by suitable exit from
the debugger (with a command that depends on the host Lisp). Evaluation of
(Break-on-error t), or equivalently, (break-on-error), is similar
except that certain errors are ignored when inside the theorem prover; this is
probably preferable, in general, to (break-on-error :all). Finally,
evaluation of (break-on-error nil) removes those traces.
Remarks.
- The argument, if supplied, is evaluated and must evaluate to t,
nil, or :all.
- For technical reasons, you may see breaks or error messages more than
once.
- It is an error to call break-on-error while in raw-mode.
- Break-on-error is implemented using ACL2 trace!, which is a
version of trace$ that uses a ttag and hence generates a
``TTAG NOTE'' message. You can use :trans1 to see the
trace! call generated by a given call of break-on-error. Evaluate
(trace$) if you want to see the current trace specs.
You are of course welcome to define your own version of break-on-error
by modifying a copy of the source definition (search for ``(defmacro
break-on-error)'' in ACL2 source file other-events.lisp). Please feel
free to send your version of break-on-error to the ACL2 implementors, to
consider for inclusion into ACL2.
Also see set-debugger-enable for how to get raw-Lisp backtrace
information when an error occurs as a result of break-on-error, or even
of a raw Lisp error, by calling set-debugger-enable with argument
:bt, :bt-break, or :break-bt. Note that for ACL2 errors (as
opposed to raw Lisp errors), i.e. errors affected by break-on-error, all
three of those keyword values are treated equivalently (and, all are ignored
for non-ANSI GCL; see set-debugger-enable).
