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 emacs/acl2-doc.el
It is easy to invoke. First, load the above file or
file emacs/emacs-acl2.el (which loads the above file).
It is probably simplest to insert the form (load
"DIR/emacs/emacs-acl2.el") into your ~/.emacs
file, before starting up Emacs, where DIR is the
directory of your local ACL2 installation. Then execute:
meta-x acl2-doc
or
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
answer 'y' to the query it makes when you start ACL2-Doc.
If you prefer, you can build it yourself; see
:DOC acl2-doc.
But in case you wish to download and install the file manually, we
make it available here, for you to install as
file books/system/doc/rendered-doc-combined.lsp in your
local ACL2 installation.
Click below to access gzipped
file rendered-doc-combined.lsp.gz (which will need to
be installed by running gunzip):
rendered-doc-combined.lsp.gz
built 2024-11-20
(the latest version posted here)rendered-doc-combined.lsp.gz built 2024-11-19