Major Section: TRACE
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
(Break-on-error) generates approximately the following, but modified to
print appropriate extra information:
(trace! (error1 :entry nil :exit (break))
(throw-raw-ev-fncall :entry (break)))
This trace should cause entry to the Lisp debugger whenever ACL2 calls
its error routines, except for certain errors when inside the theorem prover
(and even then if option :all is supplied).NOTE: For technical reasons, if you see the break message
ACL2 Error [Breaking on error (entry to ev-fncall-msg)]:which is followed by an explanation of the error, then if you continue from the break, you will see that explanation again.
Finally, note that you are 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, for possible inclusion into ACL2.
Break-on-error is implmented using ACL2 trace$. See trace! if you
want an explanation of the ``TTAG NOTE'' that is printed.
The argument, if supplied, is evaluated and must evaluate to t, nil,
or :all.
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
GCL; see set-debugger-enable).