The ACL2 Books Directory

The word ``book'' has two senses to the ACL2 user. One is the normal one: a sequence of printed paper pages bound together between covers. There are such books about ACL2. Click here for more information.

The other sense is a technical one: an ACL2 ``book'' is a file of definitions, theorems and other commands used to extend ACL2's reasoning abilities. Commands add ``rules'' to ACL2's data base. When a book is ``certified,'' ACL2 checks that all the commands in it can be successfully processed. A book can be ``included'' into an ACL2 session to extend the data base. This is the standard way users exchange useful sets of theorems. See the online documentation topic BOOKS for details.

The standard distribution of ACL2 comes with many books. They are stored on this directory. This is a guide to the available books. We include instructions on how to certify the books in this directory at the end of this note.

Some of the links below are to files. Others are to directories. When you visit a directory, look at its README file. Most of these books were written by ACL2 users other than the authors of ACL2. Authorship is acknowledged in the individual files.

If you seek a book you suspect someone might have created but which is not here, join the ACL2 mailing list and ask the community.

If you develop a book you think will be useful to the community, please submit it following the instructions for contributing books to ACL2.

Certification Instructions

Many of these books are easily imagined to be of general value to ACL2 users, while others are more specialized. Although this subdivision is a bit arbitrary, we refer to books in the former category as "basic" books. By default, the make process certifies only the basic books. It may take several hours to certify all the books, but only a couple of hours to certify only the "basic" books.

All of the instructions below assume that you are standing in subdirectory books of the ACL2 distribution.


To certify the basic books, assuming that `acl2' invokes ACL2, execute:

To certify all books, assuming that `acl2' invokes ACL2, execute the following after you download workshops.tar.gz to your acl2-sources/books/ directory, and then gunzip and extract it there.
make all-plus
To certify the basic books, assuming that `my_acl2' invokes ACL2, execute:
make ACL2=my_acl2
To certify all books using an image with absolute pathname /u/bin/allegro_acl2 on a Sparc, execute the following. Note that pathnames of images must be absolute pathnames (except that commands observable via the Unix path are OK).
make all-plus ACL2=/u/bin/allegro_acl2