Requirements

[Back to main page of Installation Guide.]

ACL2 Version 6.1 Copyright (C), Regents of the University of Texas ACL2 is licensed under the terms of the LICENSE file distributed with ACL2.

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.

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 http://www.franz.com/. 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 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 you prefer the latest release, you can obtain that instead, for example as follows. 
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.3/linuxx86/ccl
Then create a suitable script, say as follows, where DIR is 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
Now rebuild the CCL lisp image by invoking the above script and then executing the following commands. 
(ccl:rebuild-ccl :full t)
(quit)
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 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 (.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/.

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

IMPORTANT: Here we are referring to the non-ANSI version (sometimes called the "CLtL1 version") of GCL. It is probably impossible to build ACL2 with ANSI GCL just now, but that may be coming. Note: On rare occasions you may see a hard error, sometimes (not always) labeled as "bad plist", that appears to be specific to GCL. We have worked with the main GCL implementor but have not found a way to eliminate these rare errors.

Debian package. You do not need to fetch GCL if you download the binary Debian package for ACL2. Thanks to Camm Maguire for maintaining this package. It may take some time after each ACL2 release for this binary Debian package to be updated for that release.

GCL may be fetched from http://www.gnu.org/software/gcl/. If that site goes down, you may be able to find useful information from the GCL Temporary Distribution Site. GCL maintainer Camm Maguire suggests the following, in order of preference (most to least):

  1. apt-get -q install gcl gcl-doc if running Debian
  2. Download and install the prebuilt binaries otherwise (if available for your platform)
  3. Download the latest (stable) source tarball and build yourself otherwise
  4. Download the latest (stable) cvs branch and build yourself
As of December 2005, the latest recommended version is 2.6.7, and the latest development version is 2.7.0. But see below for suggestions for building GCL on a Macintosh running OS X. And see the next paragraph:

You may obtain a recent CVS version by executing, for example, the following command (if you have CVS installed on your system). This particular command will retrieve (as of August 2010) the latest development/unstable cvs sources. 

cvs -z9 -q -d:pserver:anonymous@cvs.sv.gnu.org:/sources/gcl \
     co -d gcl-2.6.8pre -r Version_2_6_8pre gcl

Macintosh. Robert Krug has provided instructions for building GCL on Mac OS X, which we include here (very slightly modified, in part with help from Camm Maguire) in case others find them helpful. 

The normal build process for GCL on Mac OS X assumes that
you have installed fink on your Mac.  (If you do not know
what this is, don't worry; you probably don't have it or
want it.)  Here we give instructions that have worked for
building GCL on OS X without fink.

   A. Obtain recent sources (there is a problem, e.g., with
      gcl-2.6.7).  For example, you can do the following:

      export CVSROOT=:pserver:anonymous@cvs.sv.gnu.org:/sources/gcl
      cvs -z9 -q co -d gcl-2.6.8pre -r Version_2_6_8pre gcl

      At some point you may be able to obtain GCL from
      ftp://ftp.gnu/org/, cd gnu, cd gcl, get
      gcl-2.6.8.tar.gz, tar xfz gcl-2.6.8.tar.gz)

   B. Make sure that /usr/local/bin is in your PATH; if not, run:
      PATH="$PATH:/usr/local/bin"

   C. cd <gcl directory>

   D. You now need to patch file h/powerpc-macosx.defs (this might not be
      necessary starting with GCL 2.6.8):

      Replace the line:
      LIBS := `echo $(LIBS) | sed -e 's/-lncurses/ /'` /sw/lib/libintl.dylib
      With:
      LIBS := `echo $(LIBS) | sed -e 's/-lncurses/ /'` /usr/local/lib/libintl.dylib

   E. Configure and start to build gcl:
      ./configure
      make

   F. Install gcl:
      sudo make install

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/.

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 $*
Your results may vary; one user has reported solving the problem with --dynamic-space-size 2000000000.

Performance comparisons

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

[Back to Installation Guide.]