Table of Contents
Here we begin with a discussion of how to invoke ACL2
interactively. We then discuss testing as well as the
certification of ACL2 community
books. We conclude with a discussion of
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 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 you on a Unix-like 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 may be important!
Most or all hosts then automatically enter the ACL2 ``command loop,'' an ACL2 read-eval-print loop with the prompt:
ACL2 !>If however a host leaves you in Common Lisp's read-eval-print loop, then you'll need to 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
books, which is a good idea anyhow; this is our next
topic. On a Unix-like system, you can also certify just a
small but useful subset of the books in a few minutes by
executing, in directory
Certifying ACL2 Books
The community books have been contributed mainly by users and may
elsewhere, to create subdirectory
The general topic of books is discussed thoroughly in the ACL2
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, both as a test of your ACL2 image and because books generally need to be certified before they can be used.
It is easy to re-certify all the community books on a Unix-like system.
We recommend you do this. If you have entered ACL2, exit to the
operating system, e.g., evaluting the form,
(quit), or 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. Failure is indicated by the presence of
CERTIFICATION FAILEDin the log.
To remove the files thus created, invoke:
certify-books target does not cause
workshops/ books to
be certified. If you want to certify those books as well, you will
first need to
the gzipped tar file of the workshops books
from the Google Code website to
books/ directory, and then gunzip and extract it
to create subdirectory
You can certify all the community books, including books for the workshops
(including those from the 1999 workshop as described in the
Reasoning: ACL2 Case Studies), using the command:
make regressionOur main installation page contains a discussion of options for the above command, such as avoidance of `
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 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 users of other than Unix-like systems (i.e., other
than Unix, GNU-Linux, and Mac OS X): we do not provide instructions
for recertifying all the community books on such systems, though
there are such environments that can be installed on Windows (e.g.,
Cygwin). The certification methods provided by the authors of the
books vary greatly and we codified them in the makefile, which is
GNUmakefile, used above. Some subdirectories
of the community book (typically installed in
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 just over 2050 pages, or about 2.4 megabytes of gzipped postscript. Its hypertext character makes it far more pleasing to read with an interactive browser. The documentation is available in several formats: HTML, Texinfo, Postscript and ACL2 documentation strings, and more recently, in web-browsable form with some community books' documentation, courtesy of Jared Davis. The ACL2 documentation is copyrighted by the Regents of the University of Texas under the terms of the LICENSE file distributed with ACL2.
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. (Macintosh users using MacOS 9 and earlier may, however, find filenames being truncated and hence will want to avoid the local documentation.)
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 (2.6 MB) version is available. It prints as a book of over 2200 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. When 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.
Note, however, that you may find it more convenient to view the documentation
in a web browser (starting at
doc/HTML/acl2-doc.html) or in Emacs
info (starting at
[Back to Installation Guide.]