Major Section: EVENTS
Examples: (include-book "my-arith") (include-book "/home/smith/my-arith") (include-book "/../../my-arith")
General Form: (include-book file :load-compiled-file action ; [default :warn] :uncertified-okp t/nil ; [default t] :defaxioms-okp t/nil ; [default t] :skip-proofs-okp t/nil ; [default t] :dir directory :doc doc-string)
file is a book name. See books for general information,
see book-name for information about book names, and see pathname for
information about file names.
Action is one of
:comp; these values are explained below. The
-okp keyword arguments, which default to
whether errors or warnings are generated under certain conditions explained
below; when the argument is
t, warnings are generated. The
argument, if supplied, is a keyword that represents an absolute pathname for
a directory (see pathname), to be used instead of the current book directory
(see cbd) for resolving the given
file argument to an absolute pathname.
:dir :system resolves
file using the distributed
books/ directory of your ACL2 installation, unless your ACL2 executable
was built somewhere other than where it currently resides; please see the
``Distributed Books Directory'' below. To define other keywords that can be
dir, see add-include-book-dir.
Doc-string is an optional
documentation string; see doc-string. If the book has no
certificate, if its
certificate is invalid or if the certificate
was produced by a different version of ACL2, a warning is printed and
the book is included anyway; see certificate. This can lead to serious
errors; see uncertified-books. If the portcullis of the certificate
(see portcullis) cannot be raised in the host logical world, an error
is caused and no change occurs to the logic. Otherwise, the non-
events in file are assumed. Then the keep of the certificate
is checked to ensure that the correct files were read; see keep. A warning
is printed if uncertified books were included. Even if no warning is
include-book places a burden on you; see certificate.
If there is a compiled file for the book that was created more recently than
the book itself and the value
action of the
argument is not
nil, or is omitted, then the compiled file is
automatically loaded; otherwise it is not loaded. If
then the compiled file must be loaded or an error will occur; if
:warn (the default) then a warning will be printed; if
:try then no warning will be printed; and if
the file will be immediately compiled (if the compiled file does not already
exist) and loaded.
Certify-book can also be used to compile a book.
An effect of compilation is to speed up the execution of the functions
defined within the book when those functions are applied to specific values.
Compilation can also remove tail recursion, thus avoiding stack overflows.
The presence of compiled code for the functions in the book should not
otherwise affect the performance of ACL2. See guard for a discussion. NOTE:
:load-compiled-file argument is not recursive; that is, calls of
include-book that are inside the book supplied to
use their own
:load-compiled-file arguments (default
:warn), not the
:load-compiled-file argument for the enclosing book.
skip-proofs-okp, determine the system's behavior when
the book or any subbook is found to be uncertified, when the book
or any subbook is found to contain
defaxiom events, and when
the book or any subbook is found to contain
respectively. All three default to
t, which means it is ``ok''
for the condition to arise. In this case, a warning is printed but
the processing to load the book is allowed to proceed. When one of
these arguments is
nil and the corresponding condition arises,
an error is signaled and processing is aborted. Exception:
:uncertified-okp is ignored if the
include-book is being
performed on behalf of a
Include-book is similar in spirit to
encapsulate in that it is
a single event that ``contains'' other events, in this case the
events listed in the file named.
Include-book processes the
local event forms in the file, assuming that each is
Local events in the file are ignored. You may
include-book to load multiple books, creating the logical
world that contains the definitions and theorems of all of
If any non-
local event of the book attempts to define a name
that has already been defined -- and the book's definition is not
syntactically identical to the existing definition -- the attempt to
include the book fails, an error message is printed, and no change
to the logical world occurs. See redundant-events for the
When a book is included, the default defun-mode
(see default-defun-mode) for the first event is always
logic. That is, the default defun-mode ``outside'' the book --
in the environment in which
include-book was called -- is
irrelevant to the book. Events that change the defun-mode are
permitted within a book (provided they are not in
However, such changes within a book are not exported, i.e., at the
conclusion of an
include-book, the ``outside'' default defun-mode
is always the same as it was before the
Unlike every other event in ACL2,
include-book puts a burden on
you. Used improperly,
include-book can be unsound in the sense
that it can create an inconsistent extension of a consistent logical
world. A certification mechanism is available to help you
carry this burden -- but it must be understood up front that even
certification is no guarantee against inconsistency here. The
fundamental problem is one of file system security.
See certificate for a discussion of the security issues.
After execution of an
include-book form, the value of
acl2-defaults-table is restored to what it was immediately before
include-book form was executed.
Distributed Books Directory. We refer to the ``books directory'' of an
executable image as the full pathname string of the books directory
:dir :system for that image. This is where the
distributed books directory should reside. By default, it is the
subdirectory of the directory where the sources reside and the executable
image is thus built. If those books reside elsewhere, the environment
variable ACL2_SYSTEM_BOOKS can be set to the
books/ directory under which
they reside (a Unix-style pathname, typically ending in
books, is permissible). In most cases, your ACL2 executable is a small
script in which you can set this environment variable just above the line on
which the actual ACL2 image is invoked.
This concludes the guided tour through books.
See set-compile-fns for a subtle point about the interaction
include-book and on-the-fly compilation.
See certify-book for a discussion of how to certify a book.