Table of Contents
ACL2 is more than just the executable image. In particular, it comes with a user's manual, and the system is distributed with libraries developed by the ACL2 community, the community books. Start here and we will take you through the whole process of obtaining and installing ACL2.
First, create a directory under which to store ACL2 Version 8.5. We will
call this directory dir. For example, dir might be
WARNING: Some of these packages might be for old versions of ACL2. We recommend that you use the latest version of ACL2 (Version 8.5).
The ACL2 Sedan
(ACL2s) is an Eclipse-based IDE for ACL2 that is distributed with pre-certified
books and pre-built binaries, though it is not always based on the
latest ACL2 version. If you
use an alternative development environment (such as Emacs), you
can still fetch a
tarball for your x86-based Linux/Mac/Windows system that contains a
pre-built binary of (pure) ACL2, using the following instructions
based on information kindly provided by Harsh Raju Chamarthi.
Just extract the
appropriate tarball (using
tar xfz on Linux or Mac
unzip on Windows)
under a path with no spaces.
Then run the script you will
run_acl2 on Linux or Mac
run_acl2.exe on Windows, to start an ACL2 session.
(Note that The first time you execute that command,
the certificate (
.cert) files are automatically
fixed, according to the full pathname of your
documentation topic on the ACL2 Sedan.
In the past, a Windows Installer for ACL2 has included a Unix environment, pre-certified standard and workshop books, and a copy of Gnu Emacs. This capability has largely been superseded by the section on Building an Executable Image on Some Particular Systems and the Shortcut using the ACL2 Sedan, above. See also information about ACL2 on Windows.
ACL2 versions are sometimes been made available under MacPorts. We have been informed that ACL2 Version 8.5 can be installed on MacOS via MacPorts.
A Debian Gnu Linux package is available, which is likely to work on
other Linux systems as well. 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
has said: "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." Alternatively, Debian GNU
Linux users may wish
to download the
ACL2 Debian package for Linux. An alternate location you might
want to check
(First, a note for Windows users only: we suggest that you obtain a
Unix-like environment or, at least, download a utility such as
djtarnt.exe to use with the
-x option on
gzipped tarfiles. WARNING: 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
tar xpvfi 8.5.tar", if you have problems with other than Gnu tar. You can see if you have Gnu tar by running "
tar -v".) The resulting tarball and its extracted directory may consist of close to 230 MB and 960 MB, respectively. Additional space is required to build an executable image, for example, perhaps about 160 MB if you use CCL and 210 MB if you use SBCL; and considerably more will be required to certify books.
tar xfz acl2-8.5.tar.gz
Note: You can also fetch the latest GitHub distribution the ACL2 system and the community books, as shown below.
git clone https://github.com/acl2/acl2Moreover, you can contribute books by joining the GitHub project.
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.
Now proceed to Using ACL2.
By default, if no
LISP=xxx is specified,
LISP=ccl is used. On our hosts,
ccl is the name of
Clozure Common Lisp (CCL), 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 a couple hundred megabytes or so.
make works for the Common Lisp implementations listed
in Requirements document on systems we
have tested. See the file
further details. If this
make command does not work for
you, please see the instructions below for other
than Unix-like systems.
You can now skip to Using ACL2.
make' utility. If you are using a trial version of Allegro Common Lisp, then you may not be able to save an image. In that case, skip to Running Without Building an Executable Image.
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; please change to that directory before continuing.
nsaved_acl2if it exists.
acl2-8.5directory 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-8.5subdirectory. Here we assume that executables have extension
.dxl, but this will depend on your host Lisp and operating system.
acl2-8.5subdirectory. 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-8.5subdirectory). 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.suffix is created for some suffix. Move it to:
saved_acl2is executable. For Windows this involves two mini-steps:
(a) Remove the
saved_acl2script (because Windows does not understand
$*). Consequently, any arguments you pass to ACL2 via the command line will be ignored.
saved_acl2.bat, for example by executing the following command.
rename saved_acl2 saved_acl2.bat
Otherwise here are steps to follow. (These are quite old and may have bugs. Please report any bugs to the Matt KaufmannACL2 implementors.)
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.2\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.6.2/unixport/ -libdir C:/gcl/gclm/lib/gcl-2.6.2/ -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-like systems.
\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 released 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).
We assume you have obtained ACL2 and placed it in directory dir, as
described above for Unix-like systems or other platforms.
(If you downloaded a pre-built ACL2 image, then you may skip this section.)
Change to subdirectory
acl2-8.5 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, execute the following forms after starting up Common Lisp in subdirectory
acl2-8.5of dir. This may take a minute or two (which is another reason to consider installing an executable image as described above, using `
make' if possible).
(load "init.lisp") (in-package "ACL2") (load-acl2) (initialize-acl2) (lp) ; enter the ACL2 read-eval-print loop
Now proceed to read more about Using ACL2.
We discuss above how to obtain a gzipped
tarfile that contains both the ACL2 sources and
books. Below we describe the ACL2 distribution only (without the
community books) from the University of Texas at Austin. Its files
are available by exploring the
directory on this website or by obtaining a gzipped tarfile,
which extracts to the contents
which in turn contains the ACL2 source files as well as the following
(and a few others not mentioned here).
LICENSE ; ACL2 license file GNUmakefile ; For GNU make TAGS ; Handy for looking at source files with emacs TAGS-acl2-doc ; Handy for finding code in books, e.g., with the acl2-doc browser bin/ ; Contains an executable script, bin/acl2, which invokes ACL2 doc/ ; ACL2 documentation emacs/ ; Some helpful emacs utilities installation/ ; Installation instructions (start with installation.html)Also available are the following.
images/: Some gzip'd tar'd executables; see
split/: The result of splitting up