|
|
|---|
|
|
|
|---|
Books are files of ACL2 events—they are the main way to split up large ACL2 developments into separate modules.
This documentation topic is about ACL2 source code files. However, there are also traditional, paper books published about ACL2 and its applications.
You will almost surely want to organize your own ACL2 work into books. They facilitate reuse, allow you to reload proofs more quickly, allow you to rebuild parts of your proof in parallel, and so forth. You will also want to be aware of the many community books, which provide useful tools and lemmas to build upon. See community-books for more information, including how to contribute.
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. A
successful
Successful book inclusion is consistency preserving, provided that the book itself is consistent, as discussed later. However, include-book assumes the events in a book are valid, so if you include a book that contains an inconsistency (e.g., an inadmissible definition) then the resulting theory is inconsistent!
Certify-book lets you certify a book to guarantee that its successful inclusion is consistency preserving. During certification, both the local and non-local forms are processed. This lets you mark as local any events you need for certification, but that you want to hide from users of the book—e.g., the hacks, crocks, and kludges on the way to a good set of rewrite rules.
Certification can also
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 book-example.