ACL2 Version 3.6 Copyright (C) 2009 University of Texas at Austin. ACL2 is licensed under the terms of the GNU General Public License. See below for details.
Often we put timing comparisons between different lisps in the ACL2 News.
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. 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
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):
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:firstname.lastname@example.org:/cvsroot/gcl co gclIf you happen to know a particular version of GCL that you wish to obtain, perhaps by following GCL mailing lists, there are alternatives. The following was recommended in Feb. 2009 by the main GCL developer, and may be the best option.
cvs -d:pserver:email@example.com:/sources/gcl co -r Version_2_6_8pre -d gcl-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:firstname.lastname@example.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,
Obtaining CMU Common Lisp
CMU Common Lisp (sometimes called CMUCL) is a non-commercial Common Lisp
implementation, available from
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 $*
CLISP is a non-commercial Common Lisp implementation, available from
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.''
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
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.
svn co http://svn.clozure.com/publicsvn/openmcl/release/1.3/linuxx86/cclThen create a suitable script, say as follows, where
DIRis 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
(ccl:rebuild-ccl :full t) (quit)Your script 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).
[Back to Installation Guide.]