|
|
|---|
|
|
|
|---|
Obtaining Common Lisp
ACL2 has been built and tested on x86-64 Linux and on Mac OS X (Darwin), which we call “Unix-like systems”, as well as (from time to time) some Windows operating systems. It has been successfully run on other platforms as well, including FreeBSD and ARM architectures.
The only other 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.
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.
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