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 :uncertified-okp t/nil ; [default t] :defaxioms-okp t/nil ; [default t] :skip-proofs-okp t/nil ; [default t] :ttags ttags ; [default nil] :dir directory :doc doc-string)where
fileis a book name. See books for general information, see book-name for information about book names, and see pathname for information about file names.
Actionis one of
:comp; these values are explained below, and the default is
:default. The three
-okpkeyword arguments, which default to
t, determine whether errors or warnings are generated under certain conditions explained below; when the argument is
t, warnings are generated. The
dirargument, 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
fileargument to an absolute pathname. In particular, by default
books/directory of your ACL2 installation, unless your ACL2 executable was built somewhere other than where it currently resides; please see the ``Books Directory'' below. To define other keywords that can be used for
dir, see add-include-book-dir.
Doc-stringis an optional documentation string; see doc-string. If the book has no
certificate, if its
certificateis 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, perhaps mitigated by the presence of a
.portfile from an earlier certification; 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-
localevents 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 printed,
include-bookplaces a burden on you; see certificate.
If you use guards, please note
include-book is executed as though
(set-guard-checking nil) has been evaluated; see set-guard-checking. If
you want guards checked, please see ld and/or see rebuild.
:load-compiled-file controls whether a compiled
file is loaded by
include-book. If compilation has been suppressed by
(set-compiler-enabled nil), then
action is coerced to
see compilation. Otherwise, if
action is missing or its value is the
:default, then it is treated as
nil, no attempt is made to load the compiled file for the book provided.
In order to load the compiled file, it must be more recent than the book's
certificate (except in raw mode, where it must be more recent than the
book itself; see set-raw-mode). For non-
nil values of
do not result in a loaded compiled file, ACL2 proceeds as follows. Note that
a load of a compiled file or expansion file aborts partway through whenever
include-book form is encountered for which no suitable compiled or
expansion file can be loaded. For much more detail, see book-compiled-file.
t: Cause an error if the compiled file is not loaded. This same requirement is imposed on every
include-bookform evaluated during the course of evaluation of the present
include-bookform, except that for those subsidiary
include-books that do not themselves specify
:load-compiled-file t, it suffices to load the expansion file (see book-compiled-file).
:warn: An attempt is made to load the compiled file, and a warning is printed if that load fails to run to completion.
:comp: A compiled file is loaded as with value
t, except that if a suitable ``expansion file'' exists but the compiled file does not, then the compiled file is first created. See book-compiled-file.
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
The keyword argument
:ttags may normally be omitted. A few constructs,
used for example if you are building your own system based on ACL2, may
require it. See defttag for an explanation of this argument.
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 several 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
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
local forms). 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.
At the beginning of execution of an
include-book form, even before
executing portcullis commands, the value of
acl2-defaults-table is restored to the value it had at startup, except
that the value of key
:inhibit-warnings is preserved. After execution of
include-book form, the value of
acl2-defaults-table is restored
to what it was immediately before that
include-book form was executed.
Books Directory. We refer to the ``books directory'' of an executable
image as the full pathname string of the directory associated with
include-book keyword option
:dir :system for that image. By default,
it is the
books/ subdirectory of the directory where the sources reside
and the executable image is thus built (except for ACL2(r) -- see real
--, where it is
books/nonstd/). If those books reside elsewhere, the
ACL2_SYSTEM_BOOKS can be set to the
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, for example:
export ACL2_SYSTEM_BOOKS ACL2_SYSTEM_BOOKS=/home/acl2/4-0/acl2-sources/booksIf you follow suggestions in the installation instructions, these books will be the ACL2 community books; see community-books.
This concludes the guided tour through books. See set-compile-fns for a
subtle point about the interaction between
include-book and on-the-fly
compilation. See certify-book for a discussion of how to certify a