ACL2 Version 7.4
Copyright (C) 2017, Regents of the University of Texas
ACL2 is licensed under the terms of the LICENSE file distributed with ACL2. See also the documentation topic, COPYRIGHT.
Obtaining Allegro Common Lisp
The website for Allegro Common Lisp, a commercial implementation, is
You may be able to obtain a trial version there.
Obtaining CCL (OpenMCL)
Clozure Common Lisp (Clozure CL, or CCL) was formerly known as OpenMCL. Quoting from the Clozure Common Lisp web page (July, 2014): ``Some distinguishing features of the implementation include fast compilation speed, native threads, a precise, generational, compacting garbage collector, and a convenient foreign-function interface.''
features are optimized for 64-bit CCL. Some large developments
may even fail with 32-bit CCL; so for CCL, the 64-bit version is
preferred. To check if your CCL is a 64-bit CCL, evaluate the
following expression in your CCL; the result should
#+x86_64 'yes #-x86_64 'noHere are instructions for fetching and installing CCL.
CLISP is a non-commercial Common Lisp implementation, available from
We do not recommend CLISP as a platform for ACL2, for the following
Obtaining CMU Common Lisp
CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from
You might be able to 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 binary Debian 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. Perhaps simplest
is to fetch it via git and then build the
gcl/gcl/bin/gcl as follows.
git clone git://git.sv.gnu.org/gcl.git cd gcl/gcl git checkout Version_2_6_13pre ./configure --enable-ansi && makeIt may also be possible to fetch it from the main GNU website for GCL or perhaps from
backports.debian.org, in which case ANSI GCL can be built as shown above:
cd gcl && ./configure --enable-ansi && make
LispWorks is a commercial Common Lisp implementation. You can download
a free, restricted, version
You may ask the vendor for an evaluation license for the full product
if you are considering purchasing a license.
SBCL (Steel Bank Common Lisp) is a non-commercial Common Lisp
implementation, available from
Building ACL2 may initially fail with SBCL because of insufficient heap
memory. Harsh Raju Chamarthi points out that a fix is to run SBCL
with an increased heap size limit. As of 2014 we find that the
--dynamic-space-size 2000 following works well
on 64-bit linux, for example using a script like the following for
#!/bin/sh <sbcl-dir-path>/src/runtime/sbcl --core <sbcl-dir-path>/output/sbcl.core --dynamic-space-size 2000 "$@"
If you try to run large jobs using ACL2 build on SBCL, such as building the ACL2+books combined manual, you may fail with and error, "Immobile space exhausted". We have avoided this error by building SBCL from source rather than obtaining a binary, using options as follows:
sh make.sh --without-immobile-space --without-immobile-code --without-compact-instance-header
[Back to Installation Guide.]