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/. Also see community-books.
defpkgs reside
include-book read the correct files
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).
