Raw-lisp-error
Raw lisp errors
You may see a message about ``ABORTING from raw Lisp'' as in the
following example.
ACL2 !>(defun foo (x) (declare (xargs :mode :program)) (car x))
Summary
Form: ( DEFUN FOO ...)
Rules: NIL
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FOO
ACL2 !>(foo 3)
***********************************************
************ ABORTING from raw Lisp ***********
********** (see :DOC raw-lisp-error) **********
Error: Fault during read of memory address #x1D
***********************************************
The message above might explain the error. If not, and
if you didn't cause an explicit interrupt (Control-C),
then it may help to see :DOC raw-lisp-error.
To enable breaks into the debugger (also see :DOC acl2-customization):
(SET-DEBUGGER-ENABLE T)
ACL2 !>
The ``Error:'' message, ``Fault during read of memory address #x1D'', is
printed by the host Common Lisp implementation. In the example above, the
function foo has an implicit guard of t, which causes
evaluation to invoke the Common Lisp function car on argument 3,
resulting in the error. This sort of error may occur when calling a
:program mode function, because the guard hasn't been verified.
See defun-mode-caveat for a discussion of the possibility that ACL2 is
rendered unsound by a raw Lisp error. For further relevant background, see
evaluation.
Calls of :program mode functions are not the only sources of raw Lisp
errors. Here is a non-exhaustive list of some such sources.
- Calls of :program mode functions
- Calls of :logic mode functions whose guards were verified
using skip-proofs
- Resource errors, e.g., when attempting to evaluate (expt 2 (expt 2
1000000)). (We have seen raw Lisp errors when evaluating that expression in
ACL2 built on host Lisps CCL, SBCL, and Allegro CL.)
- Illegal calls of certain functions and macros with special ``under the
hood'' raw Lisp code, such as read-file-into-string and return-last
- Defattach using argument :skip-checks t
- Reader errors (for examples see reader and see set-iprint)
