Major Section: ACL2 Documentation
This section explains the ACL2 online documentation system. Thus, most of it assumes that you are typing at the terminal, inside an ACL2 session. If you are reading this description in another setting (for example, in a web browser, in Emacs info, or on paper), simply ignore the parts of this description that involve typing at the terminal.
ACL2 users are welcome to contribute additional documentation. See the web page http://www.cs.utexas.edu/users/moore/acl2/contrib/.
For an introduction to the ACL2 online documentation system, type
more below. Whenever the documentation system concludes with
``(type :more for more, :more! for the rest)'' you may type
to see the next block of documentation.
Topics related to documentation are documented individually:
constraint, etc., of a function symbol
To view the documentation in a web browser, open a browser to file
doc/HTML/acl2-doc.html under your ACL2 source directory, or just go to
the ACL2 home page at http://www.cs.utexas.edu/users/moore/acl2/.
Alternatively, follow a link on the ACL2 home page to a manual, known as the
xdoc manual, which incorporates (but rearranges) the ACL2 documentation as
well as documentation from many ACL2 community books. You can build a local
copy of that manual; see for example the section ``BUILDING THE XDOC MANUAL''
in the community books
Makefile for instructions.
To use Emacs Info (inside Emacs), first load distributed file
emacs/emacs-acl2.el (perhaps inside your
.emacs file) and then
meta-x acl2-info. In order to see true links to external web
pages, you may find the following addition to your
.emacs file to be
; For emacs-version 22 or (presumably) later, you can probably set ; arrange that in Emacs Info, URLs become links, in the sense that ; if you hit
<RETURN>while standing on a URL, then you will be ; taken to that location in a web browser. If this does not happen ; automatically, then evaluating the `setq' form below might work ; if you have firefox. If that does not work, then you can probably ; figure out what to do as follows. First type ; control-h v browse-url-browser-function ; and then from the resulting help page, ; hit <return> on the link ``customize'' in: ; ``You can customize this variable'' ; and then follow instructions. (setq browse-url-browser-function (quote browse-url-firefox))
There is a print version of the documentation, though we recommend using one of the other methods (web, Emacs Info, or online) to browse it. If you really want the print version, you can find it here: http://www.cs.utexas.edu/users/moore/publications/acl2-book.ps.gz.
Below we focus on how to access the online documentation, but some of the discussion is relevant to other formats.
The ACL2 online documentation feature allows you to see extensive documentation on many ACL2 functions and ideas. You may use the documentation facilities to document your own ACL2 functions and theorems.
If there is some name you wish to know more about, then type
ACL2 !>:doc namein the top-level loop. If the name is documented, a brief blurb will be printed. If the name is not documented, but is ``similar'' to some documented names, they will be listed. Otherwise,
Every name that is documented contains a one-line description, a few
notes, and some details.
Doc will print the one-liner and the
doc has finished it stops with the message
``(type :more for more, :more! for the rest)'' to remind you that details are
available. If you then type
ACL2 !>:morea block of the continued text will be printed, again concluding with ``(type :more for more, :more! for the rest)'' if the text continues further, or concluding with ``
*-'' if the text has been exhausted. By continuing to type
moreuntil exhausting the text you can read successive blocks. Alternatively, you can type
more!to get all the remaining blocks.
If you want to get the details and don't want to see the elementary
stuff typed by
doc name, type:
ACL2 !>:MORE-DOC nameWe have documented not just function names but names of certain important ideas too. For example, see rewrite and see meta to learn about
metarules, respectively. See hints to learn about the structure of the
hintsargument to the prover. The
deflabelevent (see deflabel) is a way to introduce a logical name for no reason other than to attach documentation to it; also see defdoc.
How do you know what names are documented? There is a documentation
database which is querried with the
The documentation database is divided into sections. The sections are listed by
ACL2 !>:docs *Each section has a name,
sect, and by typing
ACL2 !>:docs sector equivalently
ACL2 !>:doc sectyou will get an enumeration of the topics within that section. Those topics can be further explored by using
more) on them. In fact the section name itself is just a documented name.
moregenerally gives an informal overview of the general subject of the section.
ACL2 !>:docs **will list all documented topics, by section. This fills several pages but might be a good place to start.
If you want documentation on some topic, but none of our names or
brief descriptions seem to deal with that topic, you can invoke a
command to search the text in the database for a given string.
This is like the GNU Emacs ``
ACL2 !>:docs "functional inst"will list every documented topic whose
more-doctext includes the substring
"functional inst", where case and the exact number of spaces are irrelevant.
If you want documentation on an ACL2 function or macro and the documentation database does not contain any entries for it, there are still several alternatives.
ACL2 !>:args fnwill print the arguments and some other relevant information about the named function or macro. This information is all gleaned from the definition (not from the documentation database) and hence this is a definitive way to determine if
fnis defined as a function or macro.
You might also want to type:
ACL2 !>:pc fnwhich will print the command which introduced
fn. You should see command-descriptor for details on the kinds of input you can give the
The entire ACL2 documentation database is user extensible. That is, if you document your function definitions or theorems, then that documentation is made available via the database and its query commands.
The implementation of our online documentation system makes use of
Common Lisp's ``documentation strings.'' While Common Lisp permits a
documentation string to be attached to any defined concept, Common
Lisp assigns no interpretation to these strings. ACL2 attaches
special significance to documentation strings that begin with the
:Doc-Section''. When such a documentation string is
seen, it is stored in the database and may be displayed via
docs, etc. Such documentation strings must follow rigid
syntactic rules to permit their processing by our commands. These
are spelled out elsewhere; see doc-string.
A description of the structure of the documentation database may also be found; see doc-string.
Finally: To build the HTML documentation, proceed with the following sequence of steps.
1. In the
doc/subdirectory of the ACL2 distribution, start ACL2 and then evaluate
2. Exit ACL2 and start it up again (or, evaluate
3. Include the documented books within your ACL2 loop using
(include-book "../doc/write-acl2-html" :dir :system).
5. Call macro
write-html-file, following the instructions at the end of distributed file