ACL2 works on the Unix (and some variants, including Linux) and Macintosh operating systems. It is built on top of any of the following Common Lisps: Allegro, GCL (Gnu Common Lisp) [or, AKCL], Lispworks, Lucid, and MCL (Macintosh Common Lisp).
We have successfully run a small but nontrivial test suite on a Sparc
2 with 16 megabytes of main memory, but performance appears better
with more memory. For more on this, see Problems.
tar xpvf acl2.tar
gunzip solaris-7-sparc-saved_acl2.tar.gz tar xpvf solaris-7-sparc-saved_acl2.tar rm solaris-7-sparc-saved_acl2.tar mv solaris-7-sparc-saved_acl2 acl2-sources/saved_acl2 chmod a+x acl2-sources/saved_acl2
gunzip debian-gnu-linux-saved_acl2.tar.gz tar xpvf debian-gnu-linux-saved_acl2.tar rm debian-gnu-linux-saved_acl2.tar mv debian-gnu-linux-saved_acl2 acl2-sources/saved_acl2 chmod a+x acl2-sources/saved_acl2
acl2-sources. The sources and an executable image are located on that subdirectory. The executable image is called
acl2-sources/saved_acl2. You can invoke ACL2 by running that image, e.g.,
/usr/local/bin/acl2, containing the following two lines:
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. These ``books'' have been contributed mainly by users
and are on the subdirectory
acl2-sources/books/README for information. The general
topic of books is discussed thoroughly in the ACL2 documentation; see
the BOOKS node 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-books-testThis will create several megabytes of output and take several hours. To remove the output, stand in the same directory as above and execute:
rm -f books/*.log rm -f books/*/*.out rm -f books/*/*.logWe 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 subdirectories of
acl2-sources/bookscontain either a
READMEfile or a
certify.lispfile. 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 the authors.
Next proceed to the section on Documentation.
LISP=xxx is specified,
The time taken to carry out this process depends on the host processor but may be an hour or two. 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 Invoking ACL2.
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-4/acl2-sources. You may link to our
ftp sources directory by clicking
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.
Next we describe how to create a suitable binary image containing
ACL2. This takes some time and you are urged first to find out
(perhaps from a local Common Lisp authority) how to save the resulting
image so that it does not have to be constructed from scratch each
time you wish to use ACL2. The time taken to carry out the
initialization process depends on the host processor but may be an
hour or two. The size of the resulting binary image is dependent on
which Lisp was used, but it may be in the vicinity of 17 megabytes.
See the file
mcl-acl2-startup.lisp for Macintosh
Invoke your local Common Lisp, which should be one of those listed in
Requirements above. Filenames in this
Lisp session should default to the dir
directory, e.g., for GCL, connect to
/acl2-sources before invoking GCL or, after
entering GCL, do
Then type the following sequence of Lisp commands,
(load "acl2.lisp") (in-package "ACL2") (compile-acl2)
The commands above will compile the ACL2 sources and create compiled
object files on your
acl2-sources subdirectory. Now exit
your Common Lisp and invoke a fresh copy of it (mainly to avoid saving
an image with the garbage created by the compilation process). Again
arrange to connect to the
acl2-sources subdirectory. In the fresh
(load "acl2.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! The message will say that it is
impossible to finish because a certain file was compiled during the
processing, thus dirtying the image yet again. So now exit your
Common Lisp and invoke a fresh copy of it (again arranging to connect
acl2-sources subdirectory). Then, in the fresh
(load "acl2.lisp") ; (load "acl2-init.lisp") ; if to use our save (in-package "ACL2") (quick-compile-acl2 t t) (initialize-acl2)
This will load the new object files into the Lisp image, and bootstrap ACL2 by reading and processing the source files. This run will succeed and leave you at the top level of your Lisp.
If you were to invoke
(LP) now, you will enter the
ACL2 command loop as discussed in Invoking
ACL2. However, we recommend that instead of doing this you save
the current image to an executable file using whatever save mechanism
exist in your Common Lisp. For consistency with these installation
instructions, we suggest you save the binary image to the file named
/acl2-sources/saved_acl2. The function
save-acl2 in file
acl2-init.lisp shows how
we save an image in various Common Lisps.
You may now proceed to Invoking ACL2.
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
http://www.cs.utexas.edu/users/moore/acl2/index.htmlThe home page provides a selected bibliography, 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.)
A Postscript file containing all the documentation is in
The file currently prints out as about 800 pages. There is an Index, followed by a Table of Contents, both at the end of the document. The corresponding
.tex file is also provided.
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. 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
may take an hour or two to build.
For non-Unix systems, the ``large'' image can be built in your local Common
(load "acl2.lisp") (in-package "ACL2") (compile-acl2 nil) (load-acl2 nil) (initialize-acl2 'include-book *acl2-pass-2-files* nil)Non-Unix users should then save the image 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.4. You may wish to
return to the Table of Contents.
all-files.txt. The distribution includes the following.
README.html; This file acl2-sources/ LICENSE ; GNU General Public License 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. doc/ ; ACL2 documentation in various formats emacs/ ; Miscellaneous emacs and file utilities, not well documented 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. makefile ; For Unix make. See 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) acl2.tar.gz.SUM ; result of our running sum acl2.tar.gz images/ ; Some gzip'd tar'd executables; see images/README. split/ ; The result of splitting up acl2.tar.gz; see split/README
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
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 on GCL or AKCL on a machine with only 16 megabytes
of RAM, it may be a good idea to have a file
~/acl2-init.lsp containing the following form, which will
help to keep the ACL2 process small as you are running it:
(setq acl2::*acl2-allocation-alist* nil).In one test on a not-quite-current version of the system, we found the following times (minutes:seconds) using a Sparc 2.
31:42 64 megabytes main memory 33:37 64 megabytes main memory, using the SETQ form above 63:52 16 megabytes main memory 43:09 16 megabytes main memory, using the SETQ form above
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.
firstname.lastname@example.org. The body of the message should contain the line:
To send a message to all who receive ACL2 mail, send the message to
email@example.com. You can post messages to the ACL2 mailing
list only if you are a member of the list.
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.