ACL2 Version 6.3
ACL2 is part of the Boyer-Moore family of provers, for which its authors have received the 2005 ACM Software System Award.
|Start Here: Applications, Tours, and Tutorials/Demos||ACL2 Workshops, UT Seminar, and Course Materials|
|Publications about ACL2 and Its Applications||The User's Manual and Hyper-Card|
|Community Books: Lemma Libraries and Utilities||Mailing Lists|
|Recent changes to this page||Obtaining, Installing, and License|
|Differences from Version 6.2||Other Releases|
|How to contribute libraries and documentation|
Libraries of books (files containing definitions and theorems) extend
the code that we have written. These community books are contributed
and maintained by the members of the ACL2 community; see the
acl2-books project page.
The libraries and the ACL2 source code are under revision control, using svn.
Experimental copies of ACL2 and the libraries are thus available between ACL2
releases. The authors of ACL2 consider svn distributions to be
experimental; while they will likely be fully functional in most cases, they
could however be incomplete, fragile, and unable to pass our own
regression. If you decide to use svn versions of either the libraries or
ACL2, then you should use both, as they tend to be kept in sync. See the
acl2-devel, for the ACL2
libraries and development sources, respectively.
A combined manual, known as the acl2+books combined (xdoc) manual, incorporates not only The User's Manual for ACL2 (with some topics rearranged) but also documentation for many books. Thanks to Jared Davis for building the xdoc processor for creating this view of the documentation. We frequently make available recent svn copies of the manual.
The ACL2 distribution includes the following extensions, which were contributed by the individuals shown.
Another extension of ACL2 is the Eclipse-based ACL2 Sedan (ACL2s). Unlike the systems above, ACL2s is distributed and maintained by Pete Manolios and his research group. ACL2s comes with a standard executable ACL2 image for Windows, but it also comes with pre-certified community books and an extension of ACL2 with additional features, including extra automation for termination proofs as well as counterexample generation.
Here are the two common entries to the documentation graph:
|Major Topics (Table of Contents)|
|Index of all documented topics|
Here is how we recommend you use this documentation.
If you are a newcomer to ACL2, we do not recommend that you wander off into the full documentation. Instead start with the ACL2-TUTORIAL documentation topic. Experienced users tend mostly to use the ``Index'' to look up concepts mentioned in error messages or vaguely remembered from their past experiences with ACL2.
Note: The documentation is available for reading in a Web
browser (recommended), in Emacs Info, using the ACL2
or as a printed book (over 2200 pages). These are available as follows.
emacs/emacs-acl2.eldistributed with ACL2 (under the
acl2-sourcesdirectory), and then evaluating
meta-x acl2-info. Alternatively, within Emacs Info press
gand then enter the following path (of course, replacing
PATH_TO_ACL2-SOURCESby the path of your
We strongly encourage users to submit additional books by following the
instructions at the acl2-books project page hosted at
We also distribute a few interface
tools, such as support for infix printing. For these, see the Utilities
Books and Papers about ACL2 and Its Applications. Some of the
papers mentioned in that collection contain utilities, scripts, or
ACL2 books for the problem domains in question.
Also, if you have written up (or are interested in writing) text that
may be helpful to other ACL2 users, we invite you to contribute it to
the community. Such user documentation may be in any format that is
readable by web browsers (for example html, pdf, and plain text).
User-contributed documentation can link back to the ACL2 documentation
proper, by using links such as:
(In general, substitute the upper-case of the documentation topic for "
MAKE-EVENT" in the example above.)
To contribute user documentation, send email to the ACL2 developers, Matt Kaufmann and J Strother Moore.
search_term site:http://www.cs.utexas.edu/users/moore/acl2/v6-3Now simply replace the word `search_term' with your topic. For example, replace `
search_term' by `
tail recursion' to get documentation about tail recursion.
tail recursion site:http://www.cs.utexas.edu/users/moore/acl2/v6-3Now you are ready to follow the link.
tail recursion' and then
<RETURN>, you will see text from several books in the svn trunk that deal with the topic of tail recursion, with an accompanying ``File Path'' shown at the end of each book's text.