• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Version
        • Acknowledgments
        • Pre-built-binary-distributions
        • Common-lisp
          • Defun-mode-caveat
          • Generalized-booleans
          • Raw-lisp-error
          • Escape-to-common-lisp
        • Git-quick-start
        • Copyright
        • Building-ACL2
        • ACL2-help
        • Bibliography
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Common-lisp

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 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 !>

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)