Requirements

[Back to main page of Installation Guide.]

ACL2 Version 7.1
Copyright (C) 2015, 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.

Table of Contents

Performance comparisons

You can see recent performance numbers by following this link, or by going to the ACL2 home page on the web and following the link "Recent changes to this page".

Obtaining Common Lisp

ACL2 works on Unix, GNU-Linux, and Mac OS X, which we call "Unix-like systems", as well as many Windows operating systems (at least including Windows 98, Windows 2000, and Windows XP). It can be built on top of any of the following Common Lisps, listed here alphabetically.

Obtaining Allegro Common Lisp

The website for Allegro Common Lisp, a commercial implementation, is http://www.franz.com/. 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.''

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/ccl
Note: 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/ccl
Next 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
Be sure to make your script executable. For example, if your script filename is my-script then on linux you might want to execute the following shell command. 
chmod +x my-script
Your 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).

Obtaining CLISP

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.

Obtaining CMU Common Lisp

CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp implementation, available from http://www.cons.org/cmucl/.

Obtaining GCL

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 GCL version 2.6.12 or later, which can be fetched as a tarball from the main GNU website for GCL or perhaps from backports.debian.org. After unpacking the archive, GCL can be built with 

cd gcl && ./configure --enable-ansi && make
The resulting GCL executable supports building a default, hons-enabled ACL2 executable. If you have reason to build a "classic" ACL2 executable (ACL2(c)) instead (that is, one that is not hons-enabled), you can omit the --enable-ansi flag above to generate a smaller GCL executable.

Obtaining LispWorks

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.

Obtaining SBCL

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 "$@"

[Back to Installation Guide.]