BOOKS

Major Section:  ACL2 Documentation

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.

• BOOK-CONTENTS -- restrictions on the forms inside books

• BOOK-EXAMPLE -- how to create, certify, and use a simple book

• BOOK-NAME -- conventions associated with book names

• CBD -- connected book directory string

• CERTIFICATE -- how a book is known to be admissible and where its defpkgs reside

• CERTIFY-BOOK -- how to produce a certificate for a book

• FULL-BOOK-NAME -- book naming conventions assumed by ACL2

• INCLUDE-BOOK -- load the events in a file

• KEEP -- how we know if include-book read the correct files

• PATHNAME -- introduction to filename conventions in ACL2

• PORTCULLIS -- the gate guarding the entrance to a certified book

• SET-CBD -- to set the connected book directory

• UNCERTIFIED-BOOKS -- invalid certificates and uncertified books

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).