BOOKS

files of ACL2 event forms
Major Section:  ACL2 Documentation

This documentation topic is about ACL2 input files. However, there are two traditional (paper) books published about ACL2: a textbook and a case studies book. Further information on those two paper books is available by following links from the ACL2 home page, http://www.cs.utexas.edu/users/moore/acl2/.

A ``book'' is a file of ACL2 events that have been certified as admissible. Using include-book you can construct a new logical world by assuming the events in any number of mutually compatible books. Relevant documented topics are listed below. Following this list is a ``guided tour'' through the topics.

You can contribute books to the ACL2 community and obtain updates inbetween ACL2 releases by visiting the acl2-books project web page, http://acl2-books.googlecode.com/.

Introduction.

A ``book'' is a file of ACL2 forms. Books are prepared entirely by the user of the system, i.e., they are ``source'' files not ``object'' files. Some of the forms in a book are marked local and the others are considered ``non-local.''

Include-book lets you load a book into any ACL2 world. If completed without error, the inclusion of a book extends the logic of the host world by the addition of just the non-local events in the book. You may extend the world by successively including a variety of books to obtain the desired collection of definitions and rules. Unless name conflicts occur (which are detected and signalled) inclusion of a book is consistency preserving provided the book itself is consistent as discussed later. However, include-book merely assumes the validity of the events in a book; if you include a book that contains an inconsistency (e.g., an inadmissible definition) then the resulting theory is inconsistent.

It is possible to ``certify'' a book, with certify-book, guaranteeing that the error-free inclusion of the certified forms will produce a consistent extension of a consistent logic. Certification processes both the local and non-local forms, so you can mark as local those events you need for certification that you want to hide from users of the book (e.g., hacks, crocks, and kludges on the way to a good set of :rewrite rules). Certification can also ``compile'' a book, thereby speeding up the execution of the functions defined within it. The desire to compile books is largely responsible for the restrictions we put on the forms allowed in books.

Extensive documentation is available on the various aspects of books. We recommend that you read it all before using books. It has been written so as to make sense when read in a certain linear sequence, called the ``guided tour'', though in general you may browse through it randomly. If you are on the guided tour, you should next read the documentation on book-example (see book-example).