control whether Lisp errors and breaks invoke the Lisp debugger
Major Section:  OTHER

Introduction. Suppose we define foo in ::program mode to take the 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 be a little different in 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] [1] 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 foo in :program mode, with an implicit guard of t. The ACL2 evaluator therefore called the Lisp evaluator, which expected nil or a consp argument to car.

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 ER with flag 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 (break$). 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 (break$).
(set-debugger-enable :never)

The discussion above also applies to interrupts (from Control-C) in some, but not all, host Common Lisps.