Major Section: DOCUMENTATION
The value of the ACL2 constant
*terminal-markup-table* is an association
list pairing markup keys with strings, to be used for printing to the
terminal. See markup for a description of the ACL2 markup language.
The entries in
*terminal-markup-table* are of the form
(key . fmt-string)where
keyis one of the doc-string tilde directives (see markup), and
fmt-stringis a string as expected by the ACL2 printing function
fmt. The system arranges that for any
arg, when an expression ~key[arg] is encountered by the documentation printer,
fmt-stringin the association list where
#\ais bound to
#\Ais bound to the result of applying the function
It is possible to implement tools in ACL2 for printing documentation
to other than the terminal. In fact, such tools exist for Texinfo
and for HTML. For now, discussion of this capability is beyond the
scope of the present topic.
constraint, etc., of a function symbol
Major Section: DOCUMENTATION
Example: :args assoc-eq
Args takes one argument, a symbol which must be the name of a
function or macro, and prints out the formal parameters, the guard
expression, the output signature, the deduced type, the constraint
(if any), and whether documentation about the symbol is available
doc. The output signature is either
& indicating that the
function returns one value;
state, indicating that it returns a
state, or an expression
(mv & & ... state ... &) indicating how many
multiple values it returns and which if any is a state.
Major Section: DOCUMENTATION
:doc command only makes sense at the terminal.
Furthermore it only works at the terminal when a ``full-size'' image
has been built. Most users will probably access the ACL2
documentation in other ways, as explained in the file
that comes with the ACL2 distribution.
Examples: ACL2 !>:doc DEFTHM ; print documentation of DEFTHM ACL2 !>:doc logical-name ; print documentation of LOGICAL-NAME ACL2 !>:doc "MY-PKG" ; print documentation of "MY-PKG"where
Related Topics: :more ; continues last :doc or :more-doc text :more-doc name ; prints more documentation for name :docs ** ; lists all documented symbols :docs "compil" ; documented symbols apropos "compil" :DOC documentation ; describes how documentation works
General Form: ACL2>:doc logical-name
logical-nameis a logical name (see logical-name) for which you hope there is documentation. Chances are there is no documentation at the moment, but we are working on adding documentation strings for all the user level ACL2 functions.
For a general discussion of our treatment of documentation strings, see documentation.
This is the first cut at online documentation. Users can be particularly helpful by sending mail on the inadequacies of the system. Address it just to Moore and put Documentation in the subject line. There are several things that trouble me about what I've done here.
First, many concepts aren't documented. Ultimately, I'd like to
. document (a) every CLTL primitive (e.g.,
coerce) and (b)
every ACL2 extension (e.g.,
getprop). But so far I have
focussed on documenting (c) the ACL2 system primitives (e.g.,
hints look like). My priorities are (c), then (b), and
then (a), following the philosophy that the most unstable features
should get online documentation in these early releases. Having
gotten the basic documentation in place, I'll document new things as
they are added, and in response to your pleas I'll try to add
documentation to old things that are widely regarded as important.
Second, I worry that the existing documentation is unhelpful because
it provides too much or too little detail, or it provides the detail
too far away from where it is needed. Please be on the lookout for
this. Did you get what you needed when you appealed to
more-doc? If not, what was it you needed? Would more
cross-references help? Did you get lost in maze of
Major Section: DOCUMENTATION
:doc! command only makes sense at the terminal.
Examples: ACL2 !>:doc! defthm ACL2 !>:doc! certificate
This command is like
:doc name followed by
more!. It prints all
the documentation of
Major Section: DOCUMENTATION
Examples: ":Doc-Section name one-liner~/notes~/details"Use
":Doc-Section name one-liner~/ notes~/ details~/ :cite old-name1 :cited-by old-name2"
(get-doc-string 'name state)to see other examples.
Documentation strings not beginning with ``
:Doc-Section'' (case is
irrelevant) are ignored. See markup for how to supply
formatting information (such as fonts and displayed text) in
ACL2 attaches special importance to documentation strings beginning
with the header ``
:Doc-Section'' (or any variant thereof obtained by
changing case). Any documentation string that does not begin with
such a header is considered unformatted and is ignored. For the
rest of this discussion, we use the phrase ``documentation string''
as though it read ``formatted documentation string.''
Documentation strings are always processed in the context of some
name, being defined. (Indeed, if an event defines no
in-theory, then it is not permitted
to have a formatted documentation string.) The string will be
associated with name in the ``documentation data base.'' The data
base is divided into ``sections'' and each section is named by a
symbol. Among the sections are
miscellaneous. A complete list of the sections may be
obtained by typing
:docs * at the terminal. You can create new
sections. The main purpose of sections is simply to partition the
large set of names into smaller subsets whose contents can be
enumerated separately. The idea is that the user may remember (or
recognize) the relevant section name and then read its contents to
find interesting items.
Within a section are ``documentation tuples'' which associate with
each documented name its documentation string and a list of related
documented names, called the ``related names'' of the name. When
doc prints the documentation for name, it always lists the related
When a formatted documentation string is submitted with the defining event of some name, the section name and an initial set of related names are parsed from the string. In addition, the formatted string contains various ``levels'' of detail that are printed out at different times. Finally, it is possible for a string to cause the newly documented name to be added to the related names of any previously documented name. Thus, as new names are introduced they can be grouped with old ones.
The general form of an ACL2 formatted documentation string is
":DOC-SECTION <section-name> <one-liner>~/ <notes>~/ <details>~/ :CITE <n1> ... :CITE <nn> :CITED-BY <m1> ... :CITED-BY <mm>"Before we explain this, let it be noted that
(get-doc-string name state)will return the documentation string associated with
namein the documentation data base. You may want to call
union-theoriesjust to see some concrete documentation strings. This documentation string, which is rather long, is under
A formatted documentation string has five parts: the header and
section-name (terminating in the first
<details> (each terminating in a tilde-slash (``
pair), and a citation part. These five parts are parsed into six
<section-name> is read as the name of a symbol,
<details> are arbitrary
sequences of characters (ignoring initial white space and not
including the tilde-slash pairs which terminate them). The
read as symbols and assembled into a list called the ``cite''
<mi> are read as symbols and assembled into a list
called the ``cited-by'' symbols. See the warning below regarding
the hackish nature of our symbol reader.
Section-name must either be a previously documented symbol or else
name, the symbol being documented. To open a new section of the
data base, named
section-name, you should define the logical name
section-name (as by
deflabel or any other event; also
see defdoc) and attach to it a documentation string for section
section-name. You might wish to print out the documentation string
we use for some of our section names, e.g.,
(get-doc-string 'events state). By forcing section names to be
documented symbols, we permit sections themselves to have one line
descriptions and discussions, presented by the standard
documentation facilities like the facilities
may be used at the terminal.
Each of the
mi's must be previously documented symbols.
<details> must be non-empty, i.e., must contain
some non-whitespace characters.
<notes> may be empty. The
:cited-bys pairs may be intermingled and may be separated by
either newlines or spaces. The citation part may be empty. When
the citation part is empty, the tilde-slash pair terminating the
<details> part may be omitted. Thus, the simplest form of a
formatted documentation string is:
":Doc-Section <section-name> <one-liner>~/~/ <details>"Since white space at the front of
<details>is ignored, we often precede those parts by
#\Newlines to make the strings easier to read in our source files. We also typically indent all of the text in the string by starting each line with a few spaces. (The Emacs commands for formatting Lisp get confused if you have arbitrary characters on the left margin.) We assume that every line in
<details>starts with at least as many spaces as
<one-liner>does, i.e., we assume they are all indented the same amount (or more). Let
dbe the number of spaces separating
#\Newlinepreceding it. When the various parts are printed, we ``de-indent'' by stripping out the first d spaces following each
However, we find that when documentation is printed flush against
the left margin it is difficult to distinguish the documentation
text from previous output. We therefore prefix each line we print
by a special pad of characters. By default, this pad is ``
| '' so
that documentation text has a vertical bar running down the left
margin. But the pad is just the value of the global variable
doc-prefix and you may
assign it any string you wish.
To add such a string to the data base under the symbol
name we make
a new entry in the section-name section of the data base. The entry
name with the string and uses the string's cites list as
the initial value of the related names field. In addition, we add
name to the related names field of each of the names listed in the
string's cited-by list. We also add
name to the related names field
of its section-name. Observe that the cites list in a string is
only the initial value of the related names of the names. Future
documentation strings may add to it via
Indeed, this is generally the case. We discuss this further below.
When a brief description of
name is required (as by
<one-liner> are printed.
<one-liner> is usually printed
starting in column 15 (however see print-doc-start-column).
Despite its name,
<one-liner> need not be one line. It usually is
one line, however.
When you type
doc name at the terminal, the first response will be
<notes>, if any.
name is the name of a section, it prints the
for each of its related names. For example, try
:doc events. If
name is not a section name but does have some related names, they
are merely listed but not explained. Try
:more-doc name prints
Our style is to let each new concept add itself to the related names
of old concepts. To do otherwise increases the chances that
documentation gets outdated because one often forgets to update
supposedly complete lists of the relevant topics when new topics are
invented. For example,
:doc theory-functions lists each available
theory function. But
shows a few examples and has an empty cites list. From where do we
get the names of the theory functions listed by
doc? The answer is
that each theory function has its own documentation string and those
strings each specify
:cited-by theory-functions. See for example
union-theories. So by the time the entire system
is assembled, the related names of
theory-functions contains all
the (documented) theory functions. This makes it easy to add new
theory functions without changing the general discussion in
When an event or command form is printed, as by
contains a formatted documentation string, we do not print the
actual documentation string (since they are usually large and
distracting). Instead we print the string:
"Documentation available via :doc"inviting you to use
get-doc-string) if you wish to see the documentation at the terminal.
Warning on Reading Symbols from Strings: When we read a symbol, such
as the section-symbol, from a documentation string, we use a quick
and dirty imitation of the much more powerful CLTL
read program. In
particular, we scan past any whitespace, collect all the characters
we see until we get to more whitespace or the end of the string,
convert the characters to upper case, make a string out of them, and
intern that string. Thus, if you typed
":Doc-Section 123 ..." we
would read the
123 as the symbol
|123|. Observe that special
characters, such as parentheses and escape characters, are not
afforded their usual reverence by our hack. Furthermore, the
question arises: in which package do we
intern the symbol? The
answer is, usually, the package containing the name being defined.
I.e., if you are documenting
my-pkg::name and you attach a
documentation string that begins
":Doc-Section: Machines ..." then
the section-symbol will be
my-pkg::machines. We recognize two
special cases. If the first character read is a colon, we use the
keyword package. If the first five characters read are
we intern in the
"ACL2" package. Our own section names, e.g.,
events, are in the
In a related area, when you ask for the documentation of a name,
e.g., when you type
:doc name at the terminal, that name is read
with the full ACL2 reader, not the hack just described. That name
is read into the current package. Thus, if you are operating
"MY-PKG" and type
:doc events, what is read is
my-pkg::events. The data base may not contain an entry for this
symbol. Before reporting that no documentation exists, we try
One last note:
defpkg permits a formatted documentation string,
which is associated in the data base with the name of the package.
But the name of the package is a string, not a symbol. It is
permitted to access the documentation of a string (i.e., package
name). But there are no facilities for getting such a
into the related names of another name nor of making such stringp
names be section names. That is because we always read symbols from
strings and never read strings from strings. I.e., if you did write
"Doc-Section \"MY-PKG\" ..." it would read in as a weird
Major Section: DOCUMENTATION
:docs command only makes sense at the terminal.
Examples: ACL2 !>:docs * ; lists documentation sections ACL2 !>:docs ** ; lists all documented topics within all sections ACL2 !>:docs events ; lists all topics in section EVENTS ACL2 !>:docs "compil" ; lists topics ``apropos''
The data base of formatted documentation strings is structured into
sections. Within a section are topics. Each topic has a one-liner,
some notes, and some detailed discussions. The
provides a view of the entire data base.
:docs takes one argument, as described below:
* list all section headings in the data base ** list all section headings and all topics within each section name list all topics in the section named name (where name is some symbol other than * and **). This is always the same as :doc name. pattern list all topics whose :doc or :more-doc text mentions the string pattern. For purposes of this string matching we ignore distinctions of case and the amount and kind (but not presence) of white space. We also treat hyphen as whitespace.
Major Section: DOCUMENTATION
Example: ACL2 !>:help
See lp for general information about the top-level command
environment for ACL2.
Major Section: DOCUMENTATION
ACL2 documentation strings make special use of the tilde character (~). In particular, we describe here a ``markup language'' for which the tilde character plays a special role. The markup language is valuable if you want to write documentation that is to be displayed outside your ACL2 session. If you are not writing such documentation, and if also you do not use the character `~', then there is no need to read on.
Three uses of the tilde character (~) in documentation strings are as follows. Below we explain the uses that constitute the ACL2 markup language.
The other uses of the tilde character are of the following form.
Indicates the end of a documentation section; see doc-string.
Indicates the literal insertion of a tilde character (~).
This directive in a documentation string is effective only during the processing of part 2, the details (see doc-string), and controls how much is shown on each round of
moreprocessing when printing to the terminal. If the system is not doing
moreprocessing, then it acts as though the ~] is not present. Otherwise, the system put out a newline and halts documentation printing on the present topic, which can be resumed if the user types
moreat the terminal.
~key[arg]Before launching into an explanation of how this works in detail, let us consider some small examples.
Here is a word that is code:
~c[function-name].Here is a phrase with an ``emphasized'' word, ``not'':
Do ~em[not] do that.Here is the same phrase, but where ``not'' receives stronger emphasis (presumably boldface in a printed version):
Do ~st[not] do that.Here is a passage that is set off as a display, in a fixed-width font:
~bv This passage has been set off as ``verbatim''. The present line starts just after a line break. Normally, printed text is formatted, but inside ~bv...~ev, line breaks are taken literally. ~evIn general, the idea is to provide a ``markup language'' that can be reasonably interpreted not only at the terminal (via
doc), but also via translators into other languages. In fact, translators have been written into Texinfo and HTML.
Let us turn to a more systematic consideration of how to mark text
in documentation strings using expressions of the form
~key[arg], which we will call ``doc-string tilde directives.''
The idea is that
key informs the documentation printer (which
could be the terminal, a hardcopy printer, or some hypertext tool)
about the ``style'' used to display
arg. The intention is that
each such printer should do the best it can. For example, we have
seen above that
~em[arg] tells the printer to emphasize
arg if possible, using an appropriate display to indicate
emphasis (italics, or perhaps surrounding
arg with some character
_, or ...). For another example, the directive for bold
~b[arg], says that printed text for
arg should be in
bold if possible, but if there is no bold font available (such as at
the terminal), then the argument should be printed in some other
reasonable manner (for example, as ordinary text). The
is case-insensitive; for example, you can use ~BV or ~Bv or ~bV in
place of ~bv.
Every form below may have any string as the argument (inside
[..]), as long as it does not contain a newline (more on that
below). However, when an argument does not make much sense to us,
we show it below as the empty string, e.g., ``
~- Print the equivalent of a dash
~b[arg] Print the argument in bold font, if available
~bid[arg] ``Begin implementation dependent'' -- Ignores argument at terminal.
~bf Begin formatted text (respecting spaces and line breaks), but in ordinary font (rather than, say, fixed-width font) if possible
~bq Begin quotation (indented text, if possible)
~bv Begin verbatim (print in fixed-width font, respecting spaces and line breaks)
~c[arg] Print arg as ``code'', such as in a fixed-width font
~ef End format; balances ~bf
~eid[arg] ``End implementation dependent'' -- Ignores argument at terminal.
~em[arg] Emphasize arg, perhaps using italics
~eq End quotation; balances ~bq
~ev End verbatim; balances ~bv
~i[arg] Print arg in italics font
~id[arg] ``Implementation dependent'' -- Ignores argument at terminal.
~il[arg] Print argument as is, but make it a link (for true hypertext environments)
~ilc[arg] Same as ~il[arg], except that arg should be printed as with ~c[arg]
~l[arg] Ordinary link; prints as ``See :DOC arg'' at the terminal (but also see ~pl below, which puts ``see'' in lower case)
~nl Print a newline
~par Paragraph mark, of no significance at the terminal (can be safely ignored; see also notes below)
~pl[arg] Parenthetical link (borrowing from Texinfo): same as ~l[arg], except that ``see'' is in lower case. This is typically used at other than the beginning of a sentence.
~sc[arg] Print arg in (small, if possible) capital letters
~st[arg] Strongly emphasize arg, perhaps using a bold font
~t[arg] Typewriter font; similar to ~c[arg], but leaves less doubt about the font that will be used.
~terminal[arg] Terminal only; arg is to be ignored except when reading documentation at the terminal, using :DOC.
Style notes and further details
It is not a good idea to put doc-string tilde directives inside
~bv ... ~ev.
Do not nest doc-string tilde directives; that is, do not write
The ~c[~il[append] function ...but note that the ``equivalent'' expression
The ~ilc[append] function ...is fine. The following phrase is also acceptable:
~bfThis is ~em[formatted] text. ~efbecause the nesting is only conceptual, not literal.
We recommend that for displayed text,
should usually each be on lines by themselves. That way, printed
text may be less encumbered with excessive blank lines. Here is an
Here is some normal text. Now start a display: ~bv 2 + 2 = 4 ~ev And here is the end of that paragraph.The analogous consideration applies to
Here is the start of the next paragraph.
~efas well as
You may ``quote'' characters inside the
arg part of
~key[arg], by preceding them with ~. This is, in fact, the
only legal way to use a newline character or a right bracket (])
inside the argument to a doc-string tilde directive.
Write your documentation strings without hyphens. Otherwise, you may find your text printed on paper (via TeX, for example) like this --
Here is a hyphe- nated word.even if what you had in mind was:
Here is a hyphe- nated word.When you want to use a dash (as opposed to a hyphen), consider using ~-, which is intended to be interpreted as a ``dash.'' For example:
This sentence ~- which is broken with dashes ~- is boring.would be written to the terminal (using
doc) by replacing
~-with two hyphen characters, but would presumably be printed on paper with a dash.
Be careful to balance the ``begin'' and ``end'' pairs, such as
~ev. Also, do not use two ``begin''
~bv) without an
intervening ``end'' directive. It is permissible (and perhaps this
is not surprising) to use the doc-string part separator
between such a begin-end pair.
Because of a bug in texinfo (as of this writing), you may wish to
avoid beginning a line with (any number of spaces followed by) the
- character or
The ``paragraph'' directive,
~par, is rarely if ever used.
There is a low-level capability, not presently documented, that
interprets two successive newlines as though they were
This is useful for the HTML driver. For further details, see the
authors of ACL2.
Emacs code is available for manipulating documentation strings that contain doc-string tilde-directives (for example, for doing a reasonable job filling such documentation strings). See the authors if you are interested.
We tend to use
~em[arg] for ``section headers,'' such as
``Style notes and further details'' above. We tend to use
~st[arg] for emphasis of words inside text. This division
seems to work well for our Texinfo driver. Note that
arg to be printed in upper-case at the terminal (using
arg to be printed at the
terminal as though
arg were not marked for emphasis.
Our Texinfo and HTML drivers both take advantage of capabilities for
indicating which characters need to be ``escaped,'' and how. Unless
you intend to write your own driver, you probably do not need to
know more about this issue; otherwise, contact the ACL2 authors. We
should probably mention, however, that Texinfo makes the following
requirement: when using
one of the special characters
}, you must
immediately follow this use with a period or comma. Also, the Emacs
``info'' documentation that we generate by using our Texinfo driver
has the property that in node names,
: has been replaced by
(because of quirks in info); so for example, the ``proof-checker''
s, is documented under
rather than under
We have tried to keep this markup language fairly simple; in
particular, there is no way to refer to a link by other than the
actual name. So for example, when we want to make
invisible link in ``code'' font, we write the following form, which
: should be in that font and then
both be in that font and be an invisible link.
Major Section: DOCUMENTATION
NOTE: The command
:more only makes sense at the terminal.
Example: ACL2 !>:morewill continue printing whatever documentation was started by
When you type
:doc name, for some documented
name, the system
responds by typing the one-liner and the notes sections of the
name. It then types ``
(cont'd)'' which stands for
``continued''. If you then type
ACL2 !>:morethe system will start to print the details section of
name. The same thing could be achieved by typing
:more-doc name, but that requires you to type name again.
Similarly, if you have typed
more-doc name, the system will print
the first ``block'' of the details section and then print
:more at that point will cause the next block
of the details section to be printed. Eventually
conclude by printing ``
*-'' which is the indicator that the text has
What is a ``block'' of text?
:More looks for the end of a paragraph
(two adjacent newlines) after printing
n lines. If it doesn't find
one before it has printed
k lines, it just stops there.
here are the values of the two state global variables
'more-doc-max-lines. You may use
assign to inspect and set these variables, e.g.,
(@ more-doc-max-lines) will return the current maximum number of
lines printed by
(assign more-doc-max-lines 19) will
set it to 19. On terminals having only 24 lines, we find min and
max settings of 12 and 19 the most pleasant.
If you want
:more to print all of the details instead of feeding
them to you one block at a time, type