Documentation
Information about options for downloading and viewing the ACL2
documentation, contributing documentation, and the available tools for
documenting your own books.
Available Documentation
If you are new to ACL2, see the ACL2-tutorial for introductory
tours, tutorials, and information about textbooks about ACL2. The ACL2 home page also
provides many links to academic publications about ACL2, including the ACL2
Workshop series.
Beyond these resources, there is a vast ACL2+Books Manual with
reference material covering the ACL2 system itself and also many community-books. There are a few ways to access the manual:
- The online version (recommended). If you expect to have an internet
connection while using the documentation, you may prefer to use the online
version of the ACL2+Books Manual.
- A local version. If you sometimes work without an internet
connection, you can download a local copy of any
web-based XDOC manual using the "down arrow" icon at the top of the page.
You can alternately build your own copy of the manual; see Building
the manual in books-certification.
- The ACL2-Doc Emacs version. If you would like to view the
documentation using Emacs instead of a web browser, there is a feature-rich
Emacs-based documentation browser provided by the ACL2 system. See ACL2-doc for details.
While you are using ACL2, you can get documentation at the terminal with
the :doc command, e.g., by typing :doc rewrite. This is
often handy, but note that it won't show you any documentation for books that
you haven't loaded yet!
Separately from the ACL2+Books Manual, the ACL2 User's Manual is
distributed with ACL2. This is much like the ACL2+Books Manual but it does
not include documentation from the books. A web-based copy is included with
the ACL2 distribution in directory doc/manual/, and you can easily get to
it by opening file doc/home-page.html in your browser.
Documenting Your Books
Documentation is written using xdoc, and may be found in the community-books. Everyone is welcome to edit and contribute to that
documentation. In particular, you are welcome to edit the book that contains
ACL2 system documentation, books/system/doc/acl2-doc.lisp. (Please do
not edit ACL2 source file doc.lisp, which is generated from that book.
More generally, edit only files under the books/ directory.)
You can also use XDOC to document your own books and to build custom
manuals for your organization.
Remark for Experienced Users. Occasionally it might make sense to
add a link to your book's documentation from the ACL2 system documentation,
which is in community-book books/system/doc/acl2-doc.lisp. You are
welcome to do so, but in that case, also add to the constant
*acl2-broken-links-alist* near the top of that file, as described in a
comment in that constant. For example, that constant's value has the
following line.
(FTY::DEFPROD "[books]/centaur/fty/top.lisp")
That line may have been added because in the form (defxdoc defrec ...)
in acl2-doc.lisp, we find a link to fty::defprod. You can do
similarly for your own added link.
If your topic is not in the "ACL2" package, such as in the example
link fty::defprod above, then add a suitable include-book form to
books/system/doc/cert.acl2. For example, that file includes the line
(include-book "centaur/fty/portcullis" :dir :system)
in order to define the "FTY" package. End of Remark for
Experienced Users
Other Resources
If you want documentation on an ACL2 function or macro that is not
documented, there are still several alternatives.
ACL2 !>:args fn
will print the arguments and some other relevant information about the
named function or macro. This information is all gleaned from the definition
and hence this is a definitive way to determine if fn is defined as a
function or macro.
You might also want to type:
ACL2 !>:pc fn
which will print the command that introduced fn. You should
see command-descriptor for details on the kinds of input you can give
the :pc command.
Subtopics
- Xdoc
- XDOC is a tool for documenting ACL2 books. You can use it to
access documentation about ACL2 and its books, to document your own books, and
to create custom web-based manuals.
- ACL2-doc
- A custom Emacs browser for reading ACL2 documentation
- Recursion-and-induction
- Recursion and Induction
- Loop$-primer
- Primer for using loop$
- Operational-semantics
- Modeling State Machines
- Pointers
- Links pointing to relevant documentation topics
- Doc
- Documentation at the terminal
- Documentation-copyright
- Copyright and authorship of documentation
- Course-materials
- Some ACL2 course materials
- Args
- args, guard, type, constraint, etc., of a
function symbol
- ACL2-doc-summary
- Summary of ACL2-doc commands
- Finding-documentation
- Searching the documentation
- Broken-link
- Placeholder for broken links in a fancy xdoc manual.
- Doc-terminal-test-2
- Short
- Doc-terminal-test-1
- Short
