Table of Contents
ACL2 is more than just the executable image. You should obtain the standard
books and a local copy of the documentation. Start here and we will take
you through the whole process of obtaining and installing ACL2.
First, create a directory in which to store ACL2 Version 3.3. We will
call this directory dir. For example, dir might be
The sources come with a
books subdirectory (here
for the latest non-incremental release)
that you may find helpful in your proof development and programming with ACL2.
The following two collections of books are not included with the sources. You
can extract them in the
books/ subdirectory of your ACL2
distribution; see the discussion on certifying
books for information on using them.
For Linux (especially Debian GNU Linux), you can download the Debian package for Linux. Thanks to Camm Maguire for maintaining this package, and for pointing out that as Debian packages are simply ar and tar archives, they can be unpacked on any linux system, and who says: If someone is running Debian, all they want to do is 'apt-get install acl2', doing likewise for any optional add-on package they wish as well, e.g. emacs, infix, etc.
You can fetch the above package for a linux
system other than Debian and unpack it as follows. First, connect to the
directory under which you install ACL2 versions and download the
.deb file there. Then submit these commands (changing
2.9-7" and "
i386" as appropriate).
mkdir acl2_2.9-7 cd acl2_2.9-7 mv ../acl2_2.9-7_i386.deb . ar x acl2_2.9-7_i386.deb tar xvfz data.tar.gzThis will create subdirectory
usr/bin/acl2by replacing "
/usr" with the full pathname for "
Alternatively, you can use the program
alien to convert the
.deb file to
.rpm format. Of course, with the method
shown above or with
alien, you will not have the benefit of
ACL2 versions are sometimes made available under MacPorts (formerly darwinports) for Mac OS X, courtesy of Greg Wright, who has graciously provided the initial version of the following insructions.
ACL2 can be built on OS X using the MacPorts system. For more information on
MacPorts, including instructions on downloading and installing the
MacPorts infrastructure, see
http://macports.org. One thing to
remember is to add MacPorts executable directory (
by default) to your path.
Once MacPorts is installed, do the following. You can stand in any directory when executing these commands, as the installation is independent of where these commands are run. You can skip the first three if you haven't installed previous versions of MacPorts or DarwinPorts.
# sudo port clean --all acl2 # sudo port uninstall acl2 +certify # sudo port uninstall acl2 +regression # sudo port install acl2 +certifyIt's not necessary to obtain a Lisp implementation first, as one is automatically downloaded and built as a dependency of ACL2.
To build the system without certifying books (though you probably will want to certify books, by using the preceding install command), change the install command to:
# sudo port install acl2
To build the system and certify the workshop books in addition to the distributed books, change the install command to the following (but note that this full regression takes a long time, more than 12 hours on a PowerBook G4 800 MHz).
# sudo port install +regression
The default build uses SBCL, which works for both Intel and PPC. If you want
to use OpenMCL on PPC, add
+openmcl to your install command.
To build ACL2(r) -- Ruben Gamboa's extension of ACL2 for reasoning about the real numbers using non-standard analysis -- use the following command, which will build both ACL2 and ACL2(r) and will certify books for ACL2(r).
# sudo port install +nonstd
Once ACL2 is installed, it can be invoked using '
acl2' at the
command prompt. (Use '
acl2r' for ACL2(r) instead.)
More on dealing with old versions (for MacPorts).
If you have an old version around from MacPorts or DarwinPorts, an
deactivate. Greg Wright
explains as follows:
The only difference between "uninstall" and "deactivate" is that uninstall saves the files in a tarball and deletes the installed files. Deactivate, by contrast, keeps the files in an internal directory and unlinks them from the user-visible directory. You can reactivate by using "port activate", which is faster than a reinstall from the tarball. Of course, only one version of a port may be active at a time.If an attempt to use
deactivatereports an error, then you may need to provide a version as suggested by the error message, e.g.:
# sudo port deactivate acl2 @3.0_1+certify
The Windows Installer for ACL2 includes a Unix environment, pre-certified standard and workshop books, and a copy of Gnu Emacs. This has not been tested on Vista.
md5sumand compare with acl2-tar-gz-md5sum if you wish to verify the transmission.)
tar xpvfi acl2.tar", if you have problems with other than Gnu tar. You can see if you have Gnu tar by running "
tar xpvf acl2.tar
http://www.cs.utexas.edu/users/moore/acl2/v3-3/distrib/acl2.tar.gz, and then extract using an appropriate
tarutility. For example, for Windows systems you may be able to download a utility such as
djtarnt.exeto be used as follows:
djtarnt.exe -x acl2.tar.gzWARNING: At least one user experienced CR/LF issues when using WinZIP, but we have received the suggestion that people untarring with that utility should probably turn off smart cr/lf conversion.
You will find that the ACL2 distribution
contains many files, subdirectories, sub-subdirectories, etc. We mean
for you to copy over to your local connected directory the entire
structure of files and subdirectories. Thus, when you have completed
acl2.tar.gz, or fetching all files directly
is done, your local connected directory should have a subdirectory
acl2-sources under which everything resides.
Now proceed to Creating or Obtaining an Executable Image.
PLEASE NOTE: The available memory for ACL2 is determined by the underlying Common Lisp executable. If you need more memory, refer to your Common Lisp's instructions for building an executable.
-md5sumfile was created using
md5sum. We may add additional links from time to time.
Note that the Debian images may work with other Linux systems as well.
Now proceed to Using ACL2.
By default, if no
LISP=xxx is specified,
LISP=gcl is used. On our hosts,
gcl is the name of
GNU Common Lisp, which can be obtained as explained in the Requirements document.
This will create executable
saved_acl2 in the
The time taken to carry out this process depends on the host processor but may be only a few minutes for a fast processor. The size of the resulting binary image is dependent on which Lisp was used, but it may be in the vicinity of 17 megabytes.
make works for the Common Lisps listed in Requirements document on systems we have
tested. See the file
acl2-sources/GNUmakefile for further details.
make command does not work for you, please see the
instructions for non-Unix/Linux systems below.
You can now skip to Using ACL2.
See also Building an Executable Image on Some Particular Systems, in case you want to skip directly to the instructions in one of its subtopics.
Otherwise, proceed as follows.
Your Common Lisp should be one of those listed in
Requirements document. Filenames
below should default to the dir
directory, e.g., for GCL, connect to
/acl2-sources before invoking GCL or, after
entering GCL, do
nsaved_acl2if it exists.
acl2-sourcesdirectory and submit the following sequence of commands.
; Compile (load "init.lisp") (in-package "ACL2") (compile-acl2)The commands above will compile the ACL2 sources and create compiled object files on your
acl2-sourcessubdirectory. In the fresh Lisp type:
; Initialization, first pass (load "init.lisp") (in-package "ACL2") (load-acl2) (initialize-acl2)This will load the new object files in the Lisp image and bootstrap ACL2 by reading and processing the source files. But the attempt at initialization will end in an error saying that it is impossible to finish because a certain file was compiled during the processing, thus dirtying the image yet again. (If however the attempt ends with an error during compilation of file
TMP1.lisp, see the first troubleshooting tip below.)
acl2-sourcessubdirectory). Then, in the fresh Lisp type:
; Initialization, second pass (load "init.lisp") (in-package "ACL2") (save-acl2 (quote (initialize-acl2)) "saved_acl2")You have now saved an image. Exit Lisp now. Subsequent steps will put the image in the right place.
osaved_acl2if it exists.
saved_acl2.dxlboth exist THEN:
saved_acl2.dxl(at end of line) to
nsaved_acl2.dxlshould exist; move it to
Otherwise here are steps to follow.
ftp://ftp.gnu.org/gnu/gcl/or as explained above. You may wish to pick a
.zipfile from the
cvs/subdirectory (containing pre-releases) that has "
mingw32" in the name.
gclm/bin/gclm.batthat came with
gcl-cvs-20021014-mingw32from the above ftp site, a separate window popped up, and with an error. Many ACL2 users prefer running in an emacs shell buffer. (We obtained emacs for Windows from
ftp://ftp.gnu.org/gnu/windows/emacs/21.2/emacs-21.2-fullbin-i386.tar.gz.) The following modification of
gclm.batseemed to solve the problem (your pathnames may vary).
@ % do not delete this line % @ECHO off set cwd=%cd% path C:\gcl\gclm\mingw\bin;%PATH% C:\gcl\gclm\lib\gcl-2.6.1\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.1/unixport/ -libdir C:/gcl/gclm/lib/gcl-2.6.1/ -eval "(setq si::*allow-gzipped-file* t)" %1 %2 %3 %4 %5 %6 %7 %8 %9
acl2.batas explained in
We hope that the above simply works. If you experience problems, the following hints may help.
TMP1.lisp. That was easily remedied by starting up a fresh GCL session and invoking
(compile-file "TMP1.lisp")before proceeding to the next step.
http://www.faculty.idc.ac.il/yishai/reasoning/win-install.htm, some of which we have tried to incorporate here. A useful point made there is that when you want to quit ACL2, use
(good-bye)which works even in raw Lisp). Or you can use
(user::bye)in raw Lisp. The point is: Avoid
control-c control-d, even thought that often works fine in emacs under Unix/Linux.
\gcc\bin, where gcl-dir is the directory where GCL is installed. To get to the place to set environment variables, you might be able to go to the control panel, under system, under advanced. Alternately, you might be able to get there by opening
My Computerand right-clicking to get to
Properties, then selecting the
Advancedtab. At one time, when GCL/Windows was release as Maxima, Pete Manolios suggested adding the system variable LD_LIBRARY_PATH with the value "maxima-dir\gcc\i386-mingw32msvc\include"; this may or may not be necessary for your GCL installation (and the path would of course likely be different).
Building ACL2 on Windows from Scratch _____________________________________________________________ Note: The disk space requirements are large. Not including emacs, I had about 275 MB taken up by msys/mingw32/gcl/acl2 during the build process. You can probably use much less space by removing files after you use them, but I didn't bother to do that. Here are the steps I took: Downloaded emacs 21.3 full distribution and installed Downloaded msys 1.10.10, installed to c:\acl2 Downloaded mingw 3.1.0-1, installed to c:\acl2\mingw Downloaded gcl 2.5.3, extracted to c:\acl2\mingw Downloaded acl2 2.8, extracted to c:\acl2\sources Compiling gcl: in msys: cd /acl2/ming2/gcl-2.5.3 ./configure make make install Compiling acl2: copy "etags.exe" to /mingw/bin. you can find this program in your emacs folder, under "bin". in msys: cd /sources make Certifying ACL2 books: This took 111 minutes on my Athlon 2500+ in msys: cd /sources mv nsaved_acl2.gcl.exe saved_acl2.exe vim books/Makefile-generic, remove "nice" from this line: ACL2=time nice ../../saved_acl2 make certify-books ACL2=/sources/saved_acl2.exe
We assume you have obtained ACL2 and placed it in directory dir, as
described above for Unix/Linux or other platforms.
(If you downloaded a pre-built ACL2 image, then you may skip this section.)
Connect to subdirectory
acl2-sources of dir,
start up your Common Lisp, and compile by executing the following forms.
This sequence of steps need only be performed once.
(load "init.lisp") (in-package "ACL2") (compile-acl2)Now each time you want to use ACL2, you need only execute the following forms after starting up Common Lisp in subdirectory
(load "init.lisp") (in-package "ACL2") (load-acl2) (initialize-acl2)Note. The resulting process includes the ACL2 documentation, and hence will probably be considerably larger (perhaps twice the size) than the result of running an executable image created as described above.
Now proceed to read more about Using ACL2.
acl2-sourcesmay be found in the file
all-files.txtin that directory.
Readme.html; This file acl2-sources/ LICENSE ; GNU General Public License GNUmakefile ; For Unix/Linux make. TAGS ; Handy for looking at source files with emacs *.lisp ; ACL2 source files all-files.txt ; List of all files in this directory and subdirectories books/ ; Examples, potentially useful in others' proofs. See books/Readme.html. doc/ ; ACL2 documentation in various formats emacs/ ; Miscellaneous emacs and file utilities, especially emacs-acl2.el init.lisp; Useful for building the system interface/ emacs/ ; Support for ACL2 "proof trees". See interface/emacs/README.doc. infix/ ; ACL2 infix printer by Mike Smith. See interface/infix/README. saved/ ; Empty directory for backing up copies during make; not important acl2.tar.gz; gzip'd tar file containing all of acl2-sources/ (see below) images/ ; Some gzip'd tar'd executables; see images/Readme.html split/ ; The result of splitting up acl2.tar.gz; see split/Readme.html
The entire acl2.tar.gz is about 7 megabytes, which expands out to over 38 megabytes. Additional space is required to build an image, perhaps 30 to 100 megabytes or more depending on the Lisp, and to certify books.
[Back to Installation Guide.]