ACL2 Manuals

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.

Web-based manuals

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 manuals

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 a
You 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):