Hyper-Card for ACL2 Programming


ACL2 is an applicative (``side-effect free'') subset of Common Lisp The Language, Second Edition.

Getting Started

If you have never used ACL2 take The Tours.

Determine from local experts whether acl2 is installed on your system. If not, you can install it from ACL2. Try invoking ACL2 with acl2.

ACL2 provides a ``read-eval-print'' command loop

ACL2 !>:program                          ; enter program mode
ACL2 p>:redef                            ; allow redefinitions
ACL2 p!>(your input form here)<Return>   ; this is a comment
(value printed here)
ACL2 p!>                                 ; waiting for your next input

To exit ACL2 to ``raw Common Lisp'' type  :q.

To enter ACL2 from raw Common Lisp, type (LP).

Use a text editor! Most ACL2 users choose Emacs. Prepare Lisp definitions in an edit buffer and save them to .lisp ``script'' files. Definitions must be presented in a ``bottom-up'' style: primitive subroutines first; top-level functions last. Submit commands one at a time in   :program mode to check syntax. Type test expressions directly to ACL2 or put them in your script, possibly as #|comments|#.

To load a script use (ld "script.lisp") or use include-book if your script is a book.


Useful ACL2 Commands

Useful EMACS Commands

Note: for an updated list and comprehensive explanation about the disabling of some emacs defaults, please see emacs-acl2.el in the acl2-sources/emacs/ directory. The list below is for ACL2 Version 2.9.4; earlier releases are missing some functionality described below.