Requirements

[Back to main page of Installation Guide.]


ACL2 Version 3.4 Copyright (C) 2008 University of Texas at Austin. ACL2 is licensed under the terms of the GNU General Public License. See below for details.

Obtaining Common Lisp

ACL2 works on Unix/Linux, Macintosh, and some 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:

Often we put timing comparisons between different lisps in the ACL2 News.

Obtaining GCL

Gnu Common Lisp (GCL) has probably been the most commonly-used platform for ACL2. 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.

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.

You may obtain recent CVS versions by executing the following commands if you have CVS installed on your system, which will retrieve the latest development/unstable cvs sources by default.

export CVS_RSH=ssh [or, if using csh: setenv CVS_RSH ssh]
cvs -d:ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co gcl
If you happen to know a particular version of GCL that you wish to obtain, perhaps by following GCL mailing lists, you can replace the commands above by commands such as the following.
export CVS_RSH=ssh [or, if using csh: setenv CVS_RSH ssh]
cvs -d:ext:anoncvs@subversions.gnu.org:/cvsroot/gcl co -r Version_x_y_z -d gcl-x.y.z 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 Allegro Common Lisp

Allegro Common Lisp is probably the most commonly-used commercial platform for ACL2. You may be able to obtain a trial version from its web site, http://www.franz.com/.

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 SBCL

SBCL (Steel Bank Common Lisp) is a non-commercial Common Lisp implementation, available from http://sbcl.sourceforge.net/.

Obtaining CLISP

CLISP is a non-commercial Common Lisp implementation, available from http://clisp.cons.org/.

Obtaining OpenMCL

OpenMCL is a free Common Lisp implementation that runs on Macintosh OS X and PPC Linux, and also on x86-64 OSX, Linux, and FreeBSD. We recommend that you visit the page of stable OpenMCL snapshots for ACL2 users and download the one suitable for your platform. Visit the OpenMCL home page, http://openmcl.clozure.com/, for more information. After obtaining OpenMCL, you may want to edit the file ccl/scripts/openmcl or file ccl/scripts/openmcl64, depending on whether you want to use a 32-bit or 64-bit version (respectively).

Obtaining Lispworks

Lispworks is a commercial Common Lisp available from http://www.lispworks.com/.

Lispworks note. We initially encountered a problem in getting ACL2 to run under LIspworks 4.2.0. The Lispworks folks provided a patch and suggested that we make the following announcement.

Users with LispWorks4.2.7 should ask us at lisp-support@xanalys.com for the transform-if-node patch. It will be helpful if they quote (Lisp Support Call #11372) when doing so. Also, they must send a bug form generated from their LispWorks image: instructions at http://www.lispworks.com/support/bug-report.html.

Performance comparisons

Please go to the ACL2 home page and follow the link "Recent changes to this page" to see recent performance numbers.

[Back to Installation Guide.]