Major Section: SWITCHES-PARAMETERS-AND-MODES
Forms (see below for explanations and GCL exceptions): (set-debugger-enable t) ; enable breaks into the raw Lisp debugger (set-debugger-enable :break) ; same as above :set-debugger-enable t ; same as above (set-debugger-enable :break-bt) ; as above, but print a backtrace first (set-debugger-enable :bt-break) ; as above, but print a backtrace first (set-debugger-enable :bt) ; print a backtrace but do not enter debugger (set-debugger-enable :never) ; disable all breaks into the debugger (set-debugger-enable nil) ; disable debugger except when calling break$
Introduction. Suppose we define
program mode to
car of its argument. This can cause a raw Lisp error. ACL2
will then return control to its top-level loop unless you enable the Lisp
debugger, as shown below (except: the error message can take quite a
different form in non-ANSI GCL).
ACL2 !>(defun foo (x) (declare (xargs :mode :program)) (car x)) Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>(foo 3) *********************************************** ************ ABORTING from raw Lisp *********** Error: Attempt to take the car of 3 which is not listp. *********************************************** If you didn't cause an explicit interrupt (Control-C), then the root cause may be call of a :program mode function that has the wrong guard specified, or even no guard specified (i.e., an implicit guard of t). See :DOC guards. To enable breaks into the debugger (also see :DOC acl2-customization): (SET-DEBUGGER-ENABLE T) ACL2 !>(SET-DEBUGGER-ENABLE T) <state> ACL2 !>(foo 3) Error: Attempt to take the car of 3 which is not listp. [condition type: TYPE-ERROR] Restart actions (select using :continue): 0: Abort entirely from this (lisp) process. [Current process: Initial Lisp Listener]  ACL2(1): [RAW LISP]
Details. ACL2 usage is intended to take place inside the ACL2 read-eval-print loop (see lp). Indeed, in most Lisp implementations ACL2 comes up inside that loop, as evidenced by the prompt:
ACL2 !>However, one can occasionally hit a raw Lisp error. Here is the above example again, this time for a GCL implementation, which unfortunately gives a slightly less aesthetic report.
ACL2 !>(foo 3) Error: 3 is not of type LIST. Fast links are on: do (si::use-fast-links nil) for debugging Error signalled by CAR. Backtrace: funcall > system:top-level > lisp:lambda-closure > lp > acl2_*1*_acl2::foo > foo > car > system:universal-error-handler > system::break-level-for-acl2 > let* > UNLESS ACL2 !>
Here, the user has defined
program mode, with an
implicit guard of
t. The ACL2 evaluator therefore called the Lisp
evaluator, which expected
nil or a
consp argument to
By default, ACL2 will return to its top-level loop (at the same level of
LD) when there is a raw Lisp error, as though a call of
HARD has been evaluated. If instead you want to enter the raw Lisp
debugger in such cases, evaluate the following form.
(set-debugger-enable t)You can subsequently return to the default behavior with:
(set-debugger-enable nil)Either way, you can enter the Lisp debugger from within the ACL2 loop by evaluating
). If you want
break$disabled, then evaluate the following, which disables entry to the Lisp debugger not only for Lisp errors but also when executing
The discussion above also applies to interrupts (from
Control-C) in some,
but not all, host Common Lisps.
It remains to discuss options
:break is synonymous with option
:bt prints a backtrace. Options
are equivalent, and each has the combined effect of
backtrace is printed and then the debugger is entered.
set-debugger-enable applies not only to raw Lisp errors, but
also to ACL2 errors: those affected by
break-on-error. However, for
ACL2 errors, entering the debugger is controlled only by
set-debugger-enable. For ACL2 errors encountered after evaluating
(break-on-error t), the
set-debugger-enable values of
:bt-break will result in the same effect: in many host
LIsps, this effect will be to cause a backtrace to be printed.
Remark for Common Lisp hackers (except for the case that the host Lisp is
non-ANSI GCL). You can customize the form of the backtrace printed by
entering raw Lisp (with
:q) and then redefining function
print-call-history, whose definition immediately precedes that of
break-on-error in ACL2 source file
ld.lisp. Of course, all bets are
off when defining any function in raw Lisp, but as a practical matter you are
probably fine as long as your books are ultimately certified with an
unmodified copy of ACL2. If you come up with improvements to
print-call-history, please pass them along to the ACL2 implementors.