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: GCL (Gnu Common Lisp; see also
Allegro Common Lisp, CMUCL (CMU Common Lisp), CLISP, MCL (Macintosh Common Lisp), and Lispworks.
We believe that ACL2 can be run successfully on systems with 32 megabytes of
memory, perhaps even as little as 16. (However, we have had a report that
certification of the full suite of distributed books was problematic with 32
megabytes, specifically, under
books/rtl/rel2/. This problem can be worked around with Makefile
changes; email the authors if you have questions.)
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 firstname.lastname@example.org 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.
/home/jones/acl2/v2-7. Begin by clicking on one of the following links.
The sources come with books that you may find helpful in your proof development and programming with ACL2. Two collections of books are not included with the sources:
md5sumand compare with acl2.tar.gz.md5sum if you wish to verify the transmission.)
tar xpvf acl2.tar
[Note for Windows systems: You may be able to download a
gunzip/tar utility from the internet for your system, in which case you may not
need to fetch individual files as discussed below. For example,
ftp://ftp.gnu.org/gnu/windows/emacs/utilities/i386/djtarnt.exe can be used as follows:
djtarnt.exe -x acl2.tar.gzThen again,
acl2.tar.gzcontains files in Unix format, hence if you encounter problems, fetch the files individually.]
Create a subdirectory of dir named
Open an ftp connection to
ftp.cs.utexas.edu by anonymous login and ftp
to the local
acl2-sources subdirectory all of the files
and directories in and below the ftp directory
pub/moore/acl2/v2-7/acl2-sources. You may link to our
ftp sources directory by clicking
[Note: You may need to use text mode, not binary mode, for example if you use Fetch on a Macintosh.]
You will find that
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 this ftp operation
is done, your local connected directory should have a subdirectory
acl2-sources and it should contain (at some level)
everything obtained by the ftp. Your local
subdirectory will now look exactly as though you had obtained our
acl2.tar.gz and done the
rm steps of the Unix instructions.
Tip for Windows users: We have received the suggestion that people untarring with winzip should probably turn off smart cr/lf conversion.
Now proceed to Creating An Executable Image.
mcl-acl2-startup.lispto complete the installation, and then proceed to Using ACL2.
.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. You can fetch GCL without fee from
as well, perhaps, as recent versions from
Linux notes. We have successfully built ACL2 under Debian Gnu Linux and Redhat 7.3, using GCL 2.5.0.
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 above. It may only work on Sun
Sparcs and 486/66 PCs, for all we know about the portability of Unix
Makefile code. See the file
acl2-sources/Makefile for further details. If this
make command does not work for you, please see the
instructions for non-Unix systems below.
You can now skip to Using ACL2.
mcl-acl2-startup.lispand then skip to Using ACL2. 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.
If you are building under Windows using GCL, you may want to proceed directly to instructions for building on Windows using GCL.
Otherwise, proceed as follows.
Your Common Lisp should be one of those listed in
Requirements above. 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.lsp") (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.lsp") (in-package "ACL2") (load-acl2) (initialize-acl2 (quote include-book) *acl2-pass-2-files* t t)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.lsp") (in-package "ACL2") (save-acl2 (quote (initialize-acl2 (quote include-book) *acl2-pass-2-files* t)) "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
ftp://ftp.gnu.org/gnu/gcl/. 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.5.0\unixport\saved_gcl.exe -dir C:/gcl/gclm/lib/gcl-2.5.0/unixport/ -libdir C:/gcl/gclm/lib/gcl-2.5.0/ -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).
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.
Otherwise, 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.lsp") (in-package "ACL2") (compile-acl2 nil)Now each time you want to use ACL2, you need only execute the following forms after starting up Common Lisp in subdirectory
(load "init.lsp") (in-package "ACL2") (load-acl2 nil) (initialize-acl2 (quote include-book) *acl2-pass-2-files* nil)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 Makefile ; For Unix make. See README. 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.lsp ; 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 split/ ; The result of splitting up acl2.tar.gz; see split/README
The entire acl2.tar.gz is roughly 4.6 megabytes, which expands out to roughly
19 megabytes. Additional space is required to build an image, perhaps 17
megabytes (though this depends on the Lisp), and to certify books.
acl2.tar.gzfile in order to build acl2. That file includes more than just the ACL2 sources proper. It suffices, for building ACL2, via the instructions above, to fetch only the
acl2-sources/*.lispfiles, which take up `only' about 5 megabytes, together with the files
acl2-sources. The sources and perhaps an executable image are located on that subdirectory. However, if you have not saved an image but instead use the directions above for Running Without Building an Executable Image, skip to When ACL2 Starts Up below.
The executable image is called
acl2-sources/saved_acl2. You can
invoke ACL2 by running that image, e.g.,
If on a Unix/Linux system, then to make it easy to invoke ACL2 by typing a short command, e.g.,
you may want to install an executable file on your path, e.g.,
/usr/local/bin/acl2, containing the following two lines:
Note: A carriage return in the file after the last line above is important!
Some hosts then automatically enter the ACL2 ``command loop,'' an ACL2 read-eval-print loop with the prompt:
ACL2 !>Other hosts will leave you in Common Lisp's read-eval-print loop. If yours is one of the latter, evaluate the Common Lisp expression
(LP)if the current package is
Once in the ACL2 command loop, you can type an ACL2 term, typically followed by ``return'' or ``enter,'' and ACL2 will evaluate the term, print its value, and prompt you for another one. Below are three simple interactions:
ACL2 !>t T ACL2 !>'abc ABC ACL2 !>(+ 2 2) 4
To get out of the ACL2 command loop, type the
This returns you to the host Common Lisp. We sometimes call this
``raw Lisp.'' You may re-enter the command loop with
(LP) as above.
Note that when you are in raw Lisp you can overwrite or destroy ACL2 by executing inappropriate Common Lisp expressions. All bets are off once you've exited our loop. That said, many users do it. For example, you might exit our loop, activate some debugging or trace features in raw Lisp, and then reenter our loop. While developing proofs or tracking down problems, this is reasonable behavior.
Now you are ready to test your image.
An easy way to test the theorem prover is to type the following term to the ACL2 command loop:
:mini-proveallThis will cause a moderately long sequence of commands to be processed, each of which is first printed out as though you had typed it. Each will print some text, generally a proof of some conjecture. None should fail.
A more elaborate test is to certify the ``books'' that come with the distribution, which is a good idea anyhow; this is our next topic. On a Unix/Linux system, you can also certify just a small but useful subset of the books in a few minutes by executing, in the top-level ACL2 directory (called dir: above):
acl2-sources/books/README.htmlfor information. The general topic of books is discussed thoroughly in the ACL2 documentation; see the
BOOKSnode in the documentation tree.
Books should be ``certified'' before they are used. We do not distribute certificates with our books, mainly because certification produces compiled code specific to the host. You should certify the books locally as a test of your ACL2 image.
It is easy to re-certify all the distributed books in Unix. We recommend you do this. If you have entered ACL2, exit to the operating system, e.g., by control-d in many systems.
While connected to dir
make certify-booksThis will generate minimal output to the screen and will probably take an hour or two. To remove the files thus created, invoke:
certify-books target does not cause workshop books to be
certified. If you want to certify those books as well, you will first need to
the gzipped tar file to the
books/ directory, and then gunzip
and extract it. You can certify all the books, including books for the
workshops (including those from the 1999 workshop as described in the
(hardbound) book Computer-Aided
Reasoning: ACL2 Case Studies), using the command:
By default, certification uses the image
/acl2-sources/saved_acl2. You may specify any ACL2
image, as long as it is either a command on your Unix path or an absolute file
name, for example as follows.
make certify-books ACL2=my-acl2 make regression ACL2=/u/smith/projects/acl2/saved_acl2
We apologize to non-Unix users: we do not provide non-Unix
instructions for recertifying the distributed books. The
certification methods provided by the authors of the books vary
greatly and we codified them in the Unix Makefile used above. Most
acl2-sources/books contain either a
README file or a
certify.lsp file. Users
who wish to certify one of these books and who cannot figure out (from
these scant clues) what to type to ACL2 should not hesitate to contact
Next proceed to the section on Documentation.
ACL2's documentation is a hypertext document that, if printed in book form, is about 800 pages or about 1.5 megabytes of text. Its hypertext character makes it far more pleasing to read with an interactive browser. The documentation is available in four formats: HTML, Texinfo, Postscript and ACL2 documentation strings. All of this material is copyrighted by the University of Texas at Austin and is derived under the GNU General Public License from material copyrighted by Computational Logic, Inc.
Two Web-based guided tours of ACL2 are available from the home page
noted below. If you are already familiar with Nqthm, you might find
it useful to look at the documentation node
NQTHM-TO-ACL2. Another useful documentation topic for
beginning ACL2 users is the node
The ACL2 Home Page is
The home page provides a selected bibliography, a search button (near the top of the page), guided tours of the system, and the complete hypertext documentation tree.
Once you have installed ACL2, the HTML form of the documentation is
available locally as
We urge you to browse your local copy of the documentation rather than our Web copy, simply to reduce Web traffic and the demand on our server.
This is a very convenient format for accessing the ACL2 documentation from within Emacs. In Emacs, invoke
meta-x infoand then, if you are unfamiliar with Info, type
control-h mto see a list of commands available. In particular, type
* ACL2 i.j: (dir
Documentation for ACL2 version i.j.
acl2-sources/doc/texinfo.texwhich is copyrighted by the Free Software Foundation, Inc. (See that file for copyright and license information.)
Users new to emacs may find it helpful to load into emacs the file
offered by this file are documented near the top of the file.
The Postscript version of the documentation is not included in our normal distribution because it is so much less useful than the hyper-text versions. But a gzipped Postscript (1.2 MB) version is available. It prints as a book of about 1000 pages and contains a Table of Contents and an index to all documented topics.
ACL2 Documentation Strings
The ACL2 system has facilities for browsing the documentation. However this
requires that the documentation be stored as strings in the Lisp image. To
save space, the images mentioned so far in this document do not contain
resident documentation strings. To build such an image on a Unix system,
make large LISP=xxx
while connected to the
acl2-sources directory. The
xxx above should be replaced by the name of your local Common
Lisp. (By default, if no
LISP=xxx is specified,
LISP=gcl is used. On our hosts,
gcl is the
name of GNU Common Lisp.) This will create dir
(note that this is the same name previously used for the image without
documentation strings). The new image may be 30 megabytes in size and
take several minutes to build on a fast (in June 2000) machine.
For non-Unix systems, the ``large'' image can be built in your local Common
Lisp by following instructions given above and then
saving the image created by the final
initialize-acl2 form to an
executable binary file.
Once you have an image of ACL2 containing documentation strings, and you are in
the ACL2 command loop, you may query the documentation on a given topic
by typing the command
where topic is the Lisp symbol naming the topic you want to learn about. To learn more about the on-line documentation, type
:help and then return.
This completes the installation of ACL2 Version 2.7. You may wish to
return to the Table of Contents.
gettimes out, an alternative is to get all of the many files in the directory
split/, each of which matches the pattern
split-acl2.tar.gz*(e.g., using an `mget' command). Once you have got all these files, concatenate them together in alphabetic order, e.g., with the command
cat split-acl2.tar.gz* > acl2.tar.gz
If you are using Version 3.2.0 of Lispworks, there is probably a bug
in the definition of
logeqv. Harlequin has sent us a
patch; if anyone asks us for it, we will ask Harlequin if we may
forward their patch.
If you are running Linux Slackware v3.0:
#+gcl (setq COMPILER::*SPLIT-FILES* 100000)This way the lisp compiler splits large C source files in files of about 100K. Without this line, some systems do not have enough memory to compile the C files. (We saw this problem arise on a machine with 16Mb of actual memory plus 16Mb of virtual memory.)
Thanks to Vanderlei Moraes Rodrigues for the Slackware notes.
REALfor information about this extension and how to build it, and a warning about its experimental nature.
You will probably want to
download the non-standard analysis books (gzipped tar file) if you care to
http://www.cs.utexas.edu/users/moore/acl2/admin/forms/email.html. You should receive a confirmation of the request a short time later, along with instructions for using the mailing list (e.g., how to retrieve archive messages). If you need further assistance, please send a message to
To send a message to all who receive ACL2 mail, send the message to
You can post messages to the ACL2 mailing
list only if you are a member of the list.
You can retrieve archive files or search the archives using a web interface
You can search the ACL2 documentation, workshops, and publications online from
Finally, please report bugs in ACL2 to
This version of ACL2 is a descendent of ACL2 Version 1.9, Copyright (C) 1997 Computational Logic, Inc.
This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
Matt Kaufmann (Kaufmann@cs.utexas.edu)
J Strother Moore (Moore@cs.utexas.edu)
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.