ACL2 Version 6.2 Copyright (C), Regents of the University of Texas ACL2 is licensed under the terms of the LICENSE file distributed with ACL2.
Often we put timing comparisons between different lisps in the ACL2 News.
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 CL (CCL) was formerly known as OpenMCL. Quoting from the Clozure CL web page: ``Clozure CL is a fast, mature, open source Common Lisp implementation that runs on Linux, Mac OS X and BSD on either Intel x86-64 or PPC.''
For Windows users: We observed stalls using CCL 1.5 on Windows (in May, 2010), though not with CCL 1.4. We have been told by a CCL implementor that this bug has been fixed, and people running CCL 1.5 under Windows at a revision less than 13900 should update.
Here is an easy way to obtain and build the latest version (generally
recommended) for Linux on running on x86 or x86-64. First execute the
following shell command to create a
ccl directory, but
linuxx86, if appropriate, any of
darwinx86 (which we use for modern Macs),
svn co http://svn.clozure.com/publicsvn/openmcl/trunk/linuxx86/cclNote: if you prefer the latest release, you can obtain that instead, for example as follows (but replace "1.9" by the latest version, for example as described at
http://ccl.clozure.com/download.html, and replace
linuxx86if appropriate as described above).
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.9/linuxx86/cclNext rebuild the executable by issuing the following commands, but replace "
./lx86cl64" by a suitable executable; e.g., for 64-bit Darwin (on Mac OS) use "
./lx86cl64 (rebuild-ccl :full t) (quit) ./lx86cl64 (rebuild-ccl :full t) (quit)
Now your CCL executable is up to date. Next, create a suitable
script, say as follows, where
DIR is the full pathname
for the directory above the new
#!/bin/sh tmp=`uname -a | fgrep x86_64` export CCL_DEFAULT_DIRECTORY=DIR/ccl # Start up 64-bit or 32-bit lisp, respectively: if [ "$tmp" != "" ] ; then \ DIR/ccl/scripts/ccl64 $* ; \ else \ DIR/ccl/scripts/ccl $* ; \ fi
my-scriptthen on linux you might want to execute the following shell command.
chmod +x my-scriptYour script (invoked with a suitable pathname, or just the filename if the directory is on your path) will now start the updated CCL lisp image.
More details if you want or need them:
Step 3 in
has more details on building from source.
Alternatively, you can download a gzipped tar
file; see the main CCL
page, or visit the page of stable
Clozure CL snapshots for ACL2 users. (Subversion and gzipped tar
files are great, but not so much a CCL disk image (
file), as we have had a report of the extracted CCL opening its own
window when you start it up.) If you don't want to write your own
script (as suggested above) then after obtaining CCL, you may wish to
ccl/scripts/ccl or file
ccl/scripts/ccl64, depending on whether you want to
use a 32-bit or 64-bit version (respectively).
CLISP is a non-commercial Common Lisp implementation, available from
Obtaining CMU Common Lisp
CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from
You do not need to fetch GCL if instead you download a binary Debian package for ACL2. Thanks to Camm Maguire for maintaining this package. Note that it may take some time after each ACL2 release for this binary Debian package to be updated for that release. Here is a shell command that might be used to obtain that package.
apt-get -q install gcl gcl-doc if running DebianOtherwise, you can fetch GCL in one of the ways described below. Note that in Spring 2013 there were updates to GCL, reflected in ACL2, that allow ACL2 (starting with ACL2 Version 6.2) to build not only on traditional ("CLtL1") GCL but also on ANSI GCL.
The simplest way may be to fetch a recent version of GCL from the main GNU website for GCL. The main GCL implementor has told us that he hopes to make suitable versions of GCL Version 2.6.8 and GCL Version 2.6.9 available in tarball form at that website in approximately mid-June, 2013.
Another way to fetch a recent GCL is with one of the following commands, which will retrieve recent development/unstable cvs sources.
cvs -z9 -q -d:pserver:firstname.lastname@example.org:/sources/gcl \ co -d gcl-2.6.8 -r Version_2_6_8pre gcl cvs -z9 -q -d:pserver:email@example.com:/sources/gcl \ co -d gcl-2.6.9 -r Version_2_6_9pre gclAs per GCL installation instructions, you may wish to build GCL as follows on a 64-bit linux machine, instead using
--enable-maxpage=524288on a 32-bit linux machine, and perhaps
--enable-maxpage=262144on a Mac.
./configure --enable-maxpage=1048576 makeYou can build an ANSI image by adding
--enable-ansito the above
./configurecommand. Alternatively, you might find suitable prebuilt binaries for a variety of machines here:
Note: On rare occasions you may see a hard error when using GCL obtained before early June, 2013, sometimes (not always) labeled as "bad plist", that may be due to interaction between GCL and GNU Make. The main GCL implementor has told us that he has fixed this problem, and will provide tarballs at the main GNU website for GCL in approximately mid-June, 2013 (as noted above).
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
Note for 32-bit linux users: When building ACL2 with SBCL 1.0.18 and
1.0.39 on 32-bit Linux, we ran out of memory with the SBCL message
"Heap exhausted, game over." We solved the problem by modifying our
sbcl script to use
--dynamic-space-size 2000, for example:
#!/bin/sh export SBCL_HOME=/projects/acl2/lisps/sbcl/sbcl-1.0.39-x86-linux/output /projects/acl2/lisps/sbcl/sbcl-1.0.39-x86-linux/src/runtime/sbcl --dynamic-space-size 2000 $*
[Back to Installation Guide.]