The "acl2+books" combined manual contains both the ACL2 User's Manual and documentation from the ACL2 community books. The links below will take you to versions of that manual.
If you are using a release copy of ACL2, you may wish to follow the first link below. If you use github snapshots of ACL2 and the community books (see the project page), then you may wish to follow the second link.
Click below to access web-based acl2+books combined manuals for:
ACL2-Doc is an Emacs-based browser for the acl2+books combined
manual, distributed with ACL2 in file
It is easy to invoke. First, load the above file or
emacs/emacs-acl2.el (which loads the above file).
It is probably simplest to insert the form
"DIR/emacs/emacs-acl2.el") into your
file, before starting up Emacs, where
DIR is the
directory of your local ACL2 installation. Then execute:
Control-x a aYou can then type '
h' for help, or go to topic acl2-doc.
You can stop reading here, but for those who are interested we provide further details below.
You will need to create a data file in order to use ACL2-Doc on the
acl2+books combined manual, for ``bleeding edge'' copies of ACL2 and
the books available from github.
Emacs will handle this for you by downloading from this website if you
y' to the query it makes when you start ACL2-Doc.
If you prefer, you can build it yourself; see
But in case you wish to download and install the file manually, we
make it available here, for you to install as
books/system/doc/rendered-doc-combined.lsp in your
local ACL2 installation.
Click below to access gzipped
rendered-doc-combined.lsp.gz (which will need to
be installed by running