|
|
|---|
|
|
|
|---|
Obtaining Common Lisp
A requirement for installing ACL2 is to install a suitable Common Lisp implementation. ACL2 can be hosted by several Common Lisp implementations, as listed alphabetically below. The most commonly-used of these are SBCL and CCL, which can be obtained without charge.
Regardless of which Common Lisp you choose, it is highly recommended that you install a 64-bit implementation. While 32-bit Lisps are supported by the core ACL2 system, using a 32-bit Lisp may result in reduced performance as well as certification failures for certain community-books. If you are unsure whether your installed Common Lisp is 64-bit or not, try running the following:
;; If you are in an ACL2 REPL, first do :q to exit to Common Lisp. ;; Evaluates to t if in a 64-bit Lisp. (>= most-positive-fixnum (1- (expt 2 60)))
Allegro Common Lisp is a commercial implementation. It has been maintained for many years, but it generally runs ACL2 more slowly than most other implementations.
CCL is available without charge. See ccl-installation for instructions on how to fetch and install CCL.
Quoting the CCL website:
Clozure CL (often called CCL for short) is a free Common Lisp implementation with a long history. Some distinguishing features of the implementation include fast compilation speed, native threads, a precise, generational, compacting garbage collector, and a convenient foreign-function interface.
As of this writing (July 2025), CCL does not run natively on Arm-based Macs. There is an effort in progress to remedy that.
CMUCL is available without charge.
Follow the Download link on the CMUCL website to obtain CMUCL. It has been maintained for many years, but it generally runs ACL2 more slowly than most other implementations. At the time of writing (July, 2025), CMUCL does not offer a 64-bit version.
GCL is available without charge.
You can download a binary Debian package for ACL2. Thanks to Camm Maguire for maintaining this package. Note however that it may take some time after each ACL2 release for this package to be updated for that release.
Otherwise, it should be easy to obtain and build GCL yourself. Note that
ACL2 requires ANSI GCL version 2.6.12 or later. See
git clone git://git.sv.gnu.org/gcl.git cd gcl/gcl git checkout Version_2_6_13pre ./configure --enable-ansi && make
LispWorks is a commercial implementation. You may ask the vendor for an evaluation license for the full product if you are considering purchasing a license.
SBCL is available without charge. See
sbcl-installation-brief for instructions on how to fetch and install
SBCL. Important: For maximum performance, build from source using the
options indicated in sbcl-installation when building with