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.
Makefile
.
Makefile
.
books/arithmetic/top-with-meta.lisp
is the most commonly used
ACL2 arithmetic book. However, arithmetic is an extraordinarily rich
topic and none of our books do it justice. If you develop an improved
arithmetic book, let us know!
cowles
and arithmetic
books when
not using make, e.g., for example, when using a Macintosh.
acl2-sources/books/
directory,
and then gunzip and extract it there.
acl2-sources/books/
directory,
and then gunzip and extract it there.
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, send a message to the ACL2 authors, Kaufmann@cs.utexas.edu and Moore@cs.utexas.edu.
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.
EXAMPLES:
To certify the basic books, assuming that `acl2
' invokes
ACL2, execute:
makeTo 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-plusTo certify the basic books, assuming that `
my_acl2
' invokes
ACL2, execute:
make ACL2=my_acl2To 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