		Search-engine friendly clone of the ACL2 documentation.

Documentation

ACL2-doc

A custom Emacs browser for reading ACL2 documentation

As discussed elsewhere (see documentation), the web-based ACL2+Books Manual provides a way to browse the combined documentation for the ACL2 system and community books. Such documentation can also be read at the terminal using the :doc command, though documentation for books will only be included for those books that have been included in the session. In this topic we describe how to browse the documentation using ACL2-Doc, a browser for reading documentation inside Emacs. It supports reading the combined documentation (ACL2 plus books), but it also supports reading the ACL2-only manual as well as custom manuals. We assume some familiarity with Emacs, for example, the notion of a ``prefix argument'': a numeric value given first with the meta key (or, probably the control key), for example, meta-0 control-t g or control-3 control-t /.

Note: If you are not happy with the way text is displayed with ACL2-Doc, see xdoc::terminal.

While ACL2-Doc is much like Emacs Info, it is a separate system that provides some additional functionality. ACL2-Doc is text-based. Any word that names a topic is a link: you can hit the <Return> key while standing on that topic to go to the page of documentation for that topic. However, many links are shown explicitly, inside square brackets. For example, here is a link that will take you to the BOOKS topic; it should show up surrounded by square brackets if you are now reading at the terminal or in ACL2-Doc, but there are no square brackets for this link if you are reading on the web.

books

It should be very rare for square brackets to be intended simply as square brackets, not as link indicators.

In order to use ACL2-Doc, load into Emacs the distributed file acl2-doc.el from an appropriate directory; see emacs. This will happen automatically if you load emacs-acl2.el from an appropriate directory; again, see emacs. Then to start the browser at the top-level topic, either execute the Emacs command

meta-x acl2-doc

or else type:

Control-t g

Thus, you can put the following form in your .emacs file if you want acl2-doc to run automatically when Emacs starts up.

(acl2-doc)

By default you will browse the ACL2+Books Manual, though if you are using a git version between ACL2 releases then you may be queried; more on that below. Or, see below for how to set a variable in your .emacs file, *acl2-doc-manual-name*, so that you will browse a custom manual. You can enter the ACL2-Doc browser at a specific documentation topic as follows (in analogy to Emacs command Meta-.):

Control-t .

In each of the cases above, you will now be in a buffer called "acl2-doc", which will be displaying the top-level ACL2 topic in a special mode, the ACL2-Doc major mode. That mode provides the following key bindings; you can also see these by typing Control-h m while in that buffer.

<Return>        acl2-doc-go!
Shift-<Return>  acl2-doc-go!-new-buffer
g               acl2-doc-go
G               acl2-doc-go-new-buffer
h               acl2-doc-help
?               acl2-doc-summary
i               acl2-doc-index
,               acl2-doc-index-next
<               acl2-doc-index-previous
K               acl2-doc-kill-buffers
l               acl2-doc-last
n               acl2-doc-search-next
p               acl2-doc-search-previous
q               acl2-doc-quit
r               acl2-doc-return
s               acl2-doc-search
S               acl2-doc-re-search
t               acl2-doc-top
u               acl2-doc-up
w               acl2-doc-where
SPC             scroll-up
TAB             acl2-doc-tab
<backtab> (which often is Shift-TAB):
                acl2-doc-tab-back
D               acl2-doc-rendered-combined-download
H               acl2-doc-history
I               acl2-doc-initialize
/               acl2-doc-definition
Control-t /     acl2-doc-definition
W               acl2-doc-where-definition

You can see the documentation for each of these in the usual way, using Control-h k {key} or Control-h f {command}. Here is what you will find in each case if you do that.

<Return>      acl2-doc-go!
   Go to the topic occurring at the cursor position.  In the case
   of <NAME>, instead go to the source code definition of NAME for
   the current manual (as for `/', but without a minibuffer query).

Shift-<Return>  acl2-doc-go!-new-buffer
   Go to the topic occurring at the cursor position in a new buffer.  In the
   case of <NAME>, instead go to the source code definition of NAME for the
   current manual (as for `/', but without a minibuffer query).  The new
   buffer's name reflects that topic name, but it stays the same even if the
   topic is subsequently changed there.

g             acl2-doc-go
   Go to the specified topic; performs completion.  The new buffer's name
   reflects that topic name, but it stays the same even if the topic is
   subsequently changed there.

G             acl2-doc-go-new-buffer
   Go to the specified topic in a new buffer; performs completion.

h             acl2-doc-help
   Go to the ACL2-DOC topic to read about how to use the ACL2-Doc browser.

?             acl2-doc-summary
   Go to the ACL2-Doc-summary topic for one-line summaries of ACL2-Doc
   browser commands.

i             acl2-doc-index
   Go to the specified topic or else one containing it as a substring;
   performs completion.  If the empty string is supplied, then go to the
   index buffer.  Otherwise, with prefix argument, consider only descendents
   of the topic supplied in response to a prompt.  Note that the index buffer
   is in ACL2-Doc mode; thus, in particular, you can type <RETURN> while
   standing on a topic in order to go directly to that topic.

,             acl2-doc-index-next
   Find the next topic containing, as a substring, the topic of the most
   recent i command.  Note: if this is the first "," or "<" after an
   exact match from "i", then start the topic search alphabetically from
   the beginning, but avoid a second hit on the original topic.  Also note
   that this command is buffer-local; it will follow the most recent i
   command executed in the current ACL2-Doc buffer.

<             acl2-doc-index-previous
   Find the previous topic containing, as a substring, the topic of the most
   recent i command.  Note: if this is the first "," or "<" after an
   exact match from "i", then start the topic search alphabetically
   (backwards) from that exact match.  Also note that this command is
   buffer-local like the "," command.

l             acl2-doc-last
   Go to the last topic visited in the current buffer.  This command is
   buffer-local.

n             acl2-doc-search-next
   Find the next occurrence for the most recent search or regular expression
   search.  Note that this command is buffer-local; it will follow the most
   recent search initiated in the current buffer.

p             acl2-doc-search-previous
   Find the previous occurrence for the most recent search or regular
   expression search.  Note: as for "n", the cursor will end up at the end
   of the match, and this command is buffer-local.

q             acl2-doc-quit
   Quit the current ACL2-Doc buffer.

K             acl2-doc-kill-buffers
   Kill all background ACL2-Doc buffers.  If invoked in an ACL2-Doc buffer,
   all ACL2-Doc buffers except the current one will be killed.  If invoked in
   any other buffer, all ACL2-Doc buffers will be killed.  With prefix
   argument, avoid a query that asks for confirmation.

r             acl2-doc-return
   Return to the last topic visited in the current buffer, popping the stack
   of such topics.  This command is buffer-local.

s             acl2-doc-search
   Search forward from the top of the manual for the input string.  If the
   search succeeds, then go to that topic with the cursor put immediately
   after the found text, with the topic name displayed in the minibuffer.
   With prefix argument, consider (also for subsequent "n" and "p"
   commands) only descendents of the topic supplied in response to a prompt.

S             acl2-doc-re-search
   Perform a regular expression search, forward from the top of the manual,
   for the input string.  If the search succeeds, then go to that topic with
   the cursor put immediately after the found text, with the topic name
   displayed in the minibuffer.  With prefix argument, consider (also for
   subsequent "n" and "p" commands) only descendents of the topic
   supplied in response to a prompt.

t             acl2-doc-top
   Go to the top topic.

u             acl2-doc-up
   Go to the parent of the current topic.

w             acl2-doc-where
   Display the topic name in the minibuffer, together with the manual name
   (ACL2+Books Manual or ACL2 User's Manual)

SPC           scroll-up
   Scroll up (same as Control-v)

TAB           acl2-doc-tab
   Visit the next link after the cursor on the current page, searching from
   the top if no link is below the cursor.

<backtab> (which often is Shift-TAB):
              acl2-doc-tab-back
   Visit the previous link before the cursor on the current page, searching
   from the bottom if no link is below the cursor.

D
   Download the ``bleeding edge'' ACL2+Books Manual from the web; then
   restart the ACL2-Doc browser to view that manual.  If this fails,
   evaluate Emacs variable acl2-doc-download-error for information on
   how to perform the download without Emacs.

H             acl2-doc-history
   Visit a buffer that displays the names of all topics visited (in any
   ACL2-Doc buffer) in order, newest at the bottom.  That buffer is in
   acl2-doc mode; thus the usual acl2-doc commands may be used.  In
   particular, you can visit a displayed topic name by putting your cursor on
   it and typing <RETURN>.

I             acl2-doc-initialize
   Restart the ACL2-Doc browser, clearing its state.  With a prefix argument,
   a query asks you to select the name of an available manual, using
   completion.  See the section on "Selecting a Manual", below,
   for more information.

/             acl2-doc-definition
(also control-t /)
   Find an ACL2 definition (in analogy to built-in Emacs command meta-.).
   With numeric prefix argument, find the next matching definition;
   otherwise, the user is prompted, where the default is the name at
   the cursor, obtained after stripping off any enclosing square
   brackets ([..]), angle brackets (<..>) as from srclink tags, and
   package prefixes.  With control-u prefix argument, search only
   ACL2 source definitions; otherwise, books are searched as well.
   As with built-in Emacs command meta-. , exact matches are given
   priority.  For more information, see the Section on "Selecting a
   Manual" in the acl2-doc online XDOC-based documentation.

W             acl2-doc-where-definition
   Find an ACL2 definition.  This is the same as
   acl2-doc-definition (the acl2-doc `/' command, as well as
   control-t /), except that the default comes from the name of the
   current page's topic instead of the cursor position.  Searches
   are continued identically when control-t / is given a numeric
   prefix argument, regardless of whether the first command was /,
   control-t /, or W; thus, a search started with W can be continued
   with, for example, meta-3 control-t /.

Selecting a Manual, Tags Files, and Custom Manuals

ACL2-Doc can display the ACL2 User's Manual, which includes documentation for the ACL2 system but not for the community-books. But by default, ACL2-Doc will display the ACL2+Books Manual, which includes documentation for those books as well. To change which of these two manuals you display, just give a prefix argument to the `I' command, as described briefly above.

For the `/' and `W' commands, you will need tags table files. These come with the ACL2 gzipped tarfile distribution, but if you obtain ACL2 from github then you will need to build them. The file "TAGS" is used when these commands are given a prefix argument (to search only the ACL2 sources), and is generated when building the saved_acl2 executable with `make'. Without a prefix argument the file "TAGS-acl2-doc" is used for searching both the ACL2 sources and the books, and is created automatically if you build the manual by certifying community book books/doc/top.lisp. You can also build "TAGS-acl2-doc" by running the command bin/make-tags-acl2-doc.sh, or by building the ACL2 executable after setting variable TAGS_ACL2_DOC to a non-empty value other than SKIP either on the command line with `make' or, for example, by putting one of the following forms in your ~/.cshrc or ~/.bashrc, respectively.

setenv TAGS_ACL2_DOC t

export TAGS_ACL2_DOC=t

If you are using a git version of ACL2 and the books, between releases, then you may need to download an extra file in order to browse the ACL2+Books Manual. Most likely you will just answer y when queried about downloading the file when first using ACL2-Doc. If you want more details, see the last of the notes in the ``Notes'' section below.

As mentioned above, you can give the `I' command a prefix argument in order to select a specific manual. You will be asked for a name, which by default will be the most recently selected such name, if any. As noted above, the only two manuals initially known to acl2-doc are the ACL2+Books Manual and the ACL2 User's Manual. These have the names `combined' and `acl2-only', respectively. You can also tell acl2-doc about a custom manual, by evaluating (in Emacs) the following form, e.g., by adding it to your ~/.emacs file before starting Emacs. Here, filename is the pathname of a file typically created by calling xdoc::save-rendered.

(extend-acl2-doc-manual-alist
 'name          ; the name of the manual
 filename       ; documentation source, typically of the form *doc*.lsp
 'top           ; the top node name, typically TOP
 printname      ; optional print name (user-level name) of manual
 url            ; optional URL of gzipped file to download into filename
 tags-file-name ; optional tags filename (from output of etags)
 acl2-tags-file-name ; as above, but without files from books/ directory
 )

For example, acl2-doc is initially built with the following two forms, which is why you can respond to the query mentioned above with `combined' or `acl2-only'.

(extend-acl2-doc-manual-alist
 'combined
 (concat *acl2-sources-dir*
         "books/system/doc/rendered-doc-combined.lsp")
 'TOP
 "ACL2+Books Manual"
 "https://acl2.org/doc/rendered-doc-combined.lsp.gz"
 (concat *acl2-sources-dir* "TAGS-acl2-doc")
 (concat *acl2-sources-dir* "TAGS"))

(extend-acl2-doc-manual-alist
 'acl2-only
 (concat *acl2-sources-dir* "doc.lisp")
 'ACL2
 "ACL2 User's Manual"
 nil
 nil
 (concat *acl2-sources-dir* "TAGS"))

Note that the first of these forms specifies the location of the "TAGS-acl2-doc" and "TAGS" files mentioned above, but the second only specifies "TAGS" since the second form is for an ACL2-only manual (no books).

If you want a specific manual to come up when you first run acl2-doc in an Emacs session, you can put the following into your .emacs file, where 'name is the name a manual for which you have included a form (extend-acl2-doc-manual-alist 'name ...) in your .emacs file.

(setq *acl2-doc-manual-name* 'name)

Color

By default, links (indeed, any text) in square brackets will be shown in blue. You can customize this behavior by setting (e.g., in your .emacs file) the Emacs variable *acl2-doc-link-color* to the desired link color, or to nil if you don't want the links to be in color. For example:

(setq *acl2-doc-link-color* "#FF0000") ; red
(setq *acl2-doc-link-color* "Green")   ; green
(setq *acl2-doc-link-color* nil)         ; no special color for links

Notes

You might find that when you attempt to follow some-broken-link, you find yourself at the broken-link topic. If you are using the ACL2 User's Manual rather than the ACL2+Books Manual, the reason might be that some-broken-link is documented in a book, not in the ACL2 system. In that case, the broken-link page will show you where to find that book; but if you want to read the documentation for some-broken-link in the ACL2-Doc browser, you can do so by switching to the ACL2+Books Manual. See the I command, documented above.
Files with names ending in .acl2-doc will come up in ACL2-Doc mode. Thus, you may wish to save a file with that extension, for example bookmarks.acl2-doc, that contains your favorite bookmarks. You may wish to use the history command (H) to obtain a list of names of visited topics, in order to create an initial such file.
Many commands offer defaults, and many offer completion. The default is determined by cursor position: if the cursor is sitting on a letter of a documentation topic name, or on a space character immediately after it, then that name will be offered as the default. Completion tips:
- Completion is carried out with the usual emacs ``completing-read''; thus, for example, the character `?' is a help key, so if you want that character as part of your topic name, prefix it with control-q. For example, after the `g' command you can go to the topic mv? by typing the character sequence <m,v,control-q ?>.
- To find completions that have package prefixes, type a colon (:) in the front, and completion will show matching topics. For example, "g" followed by ":rew" and then two tabs will show, at least in recent versions of Emacs, a list of topics that includes "ACL2-PC::REWRITE".
Square brackets typically indicate documentation topic names, for example: [acl2-doc]. (As mentioned above, there are occasional exceptions, where square brackets are simply part of the intended documentation text.) The square brackets are really there, for example when you are searching using "s", "S", or "n". However, for purposes of determining the default name (see above), the only effect of the enclosing square brackets is to extend the region in which the default is offered. For example, consider the string "[acl2-doc]": the default name of "acl2-doc" is offered if the cursor is on either square bracket. But links have some idiosyncrasies.
1. Topic names, including links `[..]' to topic names, are printed relative to the ACL2 package. Especially in the case of the ACL2+Books Manual, you may therefore see links that include package prefixes. Here, for example, is a sentence from the documentation for gl in the ACL2+Books Manual.
```
We call these structures [gl::symbolic-objects]. 
   
```
  The "gl" package prefix allows commands to pick up "gl::symbolic-objects" as the name to use as a default, so that for example, hitting <Return> will take you to that topic. But when reading the sentence, for best results you should ignore package prefixes. So for example, you would read the sentence above as follows.
```
We call these structures symbolic-objects. 
   
```
2. Inside ACL2-Doc, topic names that originally contained spaces now have underscores in place of the spaces. So for example, the topic ACL2-tutorial in the ACL2+Books Manual contains a link to the topic originally named as follows.
  |Pages Written Especially for the Tours|
  This link shows up in the ACL2-Doc browser as:
  [Pages_Written_Especially_for_the_Tours].
Of course, the web-based browser avoids these idiosyncrasies (see xdoc::save); in particular, that browser is best for ``Tours'' pages like the one shown above and its subtopics, in part because that way you may see images. Hence the web-based browser may be more appropriate for some topics, and for those who have no particular preference for using Emacs to browse the documentation.
Searching using the "s" or "S" command is carried out by searching top-to-bottom in a hidden Emacs buffer that contains all of the documentation. The topics are listed in the following order according to topic name:
1. All topics whose names reside in the "ACL2" package;
2. All topics whose names reside in the "ACL2-PC" package; and, for the ACL2+Books Manual,
3. All other topics, sorted by symbol-name and then by symbol-package-name.
You may be queried, regarding whether you want to browse the ACL2+Books Manual, which is preferred, or the ACL2 User's Manual, which omits documentation for the books. Both of these manuals are based on files that you will have if you are using a released version of ACL2 (after Version 6.3). But if you are using a git version, then to use the ACL2+Books Manual you will need an extra file. You can build this file yourself, as described below but you may prefer to download it: for example, when you start ACL2-Doc, you may be given the option of downloading a tarball for the latest ``bleeding edge'' copy and extracting into directory system/doc/ of your community books directory. Indeed, the system will do all this for you if you answer y to that query. Alternatively, you can insist on a download of a ``bleeding edge'' version by using the `D' command. However, if you prefer to browse the ACL2 User's Manual (without the books), you can put the following form into your ~/.emacs file, above the form that loads the code for ACL2-Doc (see above).
```
(defvar *acl2-doc-manual-name* 'acl2-only)
```
If you prefer to build rendered-doc-combined.lsp yourself, you can do so as follows.
1. Build ACL2:
```
make
```
2. Build the file books/system/doc/rendered-doc-combined.lsp while standing in the books/ directory, as follows. If "acl2" invokes the ACL2 executable that you just built, then you may omit "ACL2=acl2" below; otherwise replace "acl2" by a suitable executable. On a multi-core machine you may wish to use -j, e.g., make -j 4 ....
```
cd books
make doc/top.cert USE_QUICKLISP=1 ACL2=acl2
```