ACL2 Version 6.5
Copyright (C) 2014, 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.
The website for Allegro Common Lisp, a commercial implementation, is
http://www.franz.com/.
You may be able to obtain a trial version there.
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.''
Here is an easy way to obtain and build the latest version (generally
recommended) for Linux (or another OS; see below) running on an x86 or
x86-64. First execute the following shell command to create
a ccl directory, but substituting
for linuxx86, if appropriate, any of
darwinx86 (which we use for modern Macs), freebsdx86,
solarisx86, windows, darwinppc,
or linuxppc.
svn co http://svn.clozure.com/publicsvn/openmcl/trunk/linuxx86/cclNote: if however you insist on using 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 linuxx86 if 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 "./dx86cl64".
./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 ccl directory.
#!/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-script then 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
http://trac.clozure.com/openmcl/wiki/UpdatingFromSource
has more details on building from source.
Alternatively, you can download a gzipped tar
file; see the main
Clozure CL page. (Note: Subversion and gzipped tar
files are great, but not so much a CCL disk image (.dmg
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
edit file 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
http://clisp.cons.org/.
We do not recommend CLISP as a platform for ACL2, for the following
reasons.
CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from http://www.cons.org/cmucl/.
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. Here is a shell command that might be used to obtain that package (if running Debian).
apt-get -q install gcl gcl-docOtherwise, it should be easy to obtain and build GCL yourself. There are two recommended versions of GCL for building ACL2: GCL 2.6.8 and GCL 2.6.10. (GCL 2.6.9, which is not recommended, has some issues that were fixed in GCL 2.6.10.) GCL 2.6.8 appeared initially to be faster for ACL2 regressions than GCL 2.6.10, but we recently measured GCL 2.6.10 (actually GCL 2.6.10pre, as of Oct. 1, 2013) to be slightly faster, using non-ANSI builds for both. We have also had better success with GCL 2.6.10 than GCL 2.6.8 on a Mac, where 2.6.8 ran out of memory for two regression tests but 2.6.10 (again, actually 2.6.10pre) did not. Note that GCL 2.6.10 probably has better ANSI support than 2.6.8, and ANSI support is needed if you choose to build ACL2(h)).
You can fetch either GCL 2.6.8 and GCL 2.6.10 as a tarball from the
main GNU website for
GCL. From GCL source you can build an executable by extracting
from the tarball, standing in the resulting gcl/
directory, and issuing one of the following commands.
# Recommended for 64-bit Linux: ./configure --enable-maxpage=1048576 && make # Recommended for Mac OS: ./configure && make # If you want an ANSI build # (but add "--enable-maxpage=1048576" in the case of 64-bit Linux, as above): ./configure --enable-ansi && make
LispWorks is a commercial Common Lisp implementation. You can download
a free, restricted, version
from http://www.lispworks.com/.
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 http://sbcl.sourceforge.net/.
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
the option --dynamic-space-size 2000 following works well
on 64-bit linux, for example using a script like the following for
SBCL.
#!/bin/sh <sbcl-dir-path>/src/runtime/sbcl --core <sbcl-dir-path>/output/sbcl.core --dynamic-space-size 2000 "$@"