DOCUMENTATION

functions that display documentation 
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 :more to see the next block of documentation.

Topics related to documentation are documented individually:

Some Related Topics

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 execute 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 helpful. 

; 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 name
in 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, nil is returned.

Every name that is documented contains a one-line description, a few notes, and some details. :Doc will print the one-liner and the notes. When :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 !>:more
a 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 :more until 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 name
We have documented not just function names but names of certain important ideas too. For example, see rewrite and see meta to learn about :rewrite rules and :meta rules, respectively. See hints to learn about the structure of the :hints argument to the prover. The deflabel event (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 :docs command.

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 sect
or equivalently 
ACL2 !>:doc sect
you will get an enumeration of the topics within that section. Those topics can be further explored by using :doc (and :more) on them. In fact the section name itself is just a documented name. :more generally 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 ``apropos'' command. 

ACL2 !>:docs "functional inst"
will list every documented topic whose :doc or :more-doc text 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 fn
will 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 fn is defined as a function or macro.

You might also want to type: 

ACL2 !>:pc fn
which will print the command which introduced fn. You should see command-descriptor for details on the kinds of input you can give the :pc command.

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 characters ``:Doc-Section''. When such a documentation string is seen, it is stored in the database and may be displayed via :doc, :more, :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 (certify-book "write-acl2-html").

2. Exit ACL2 and start it up again (or, evaluate :u).

3. Include the documented books within your ACL2 loop using include-book.

4. Evaluate (include-book "../doc/write-acl2-html" :dir :system).

5. Call macro write-html-file, following the instructions at the end of distributed file doc/write-acl2-html.lisp.