Load the events in a file
; Include using relative pathnames:
; Include using absolute pathname:
; Include a community book:
(include-book "arithmetic/top-with-meta" :dir :system)
(include-book file :load-compiled-file action
:uncertified-okp t/nil/:ignore-certs ; [default t]
:defaxioms-okp t/nil ; [default t]
:skip-proofs-okp t/nil ; [default t]
:ttags ttags ; [default nil]
where 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 t, nil,
:default, :warn, or :comp; these values are explained below,
and the default is :default. The three -okp keyword 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 dir 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. In particular, by default
:dir :system resolves file using the 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. If the book has no certificate, if its
certificate is invalid (say, because its book-hash shows that books
have changed after their certification), 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 .port file 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-local 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 printed, include-book places
a burden on you; see certificate.
If you use guards, please note include-book is executed as
though (set-guard-checking t) has been evaluated; see set-guard-checking. If you want to run with different guard-checking,
consider using ld instead, or in addition; see ld.
The value of :load-compiled-file controls whether a compiled file for
the given file is loaded by include-book. Note that this keyword
applies only to the given file, not to any included sub-books. In order
to skip loading all compiled files, for the given file as well as all
included sub-books — for example, to avoid Lisp errors such as ``Wrong
FASL version'' — use (set-compiler-enabled nil state); see compilation. Otherwise, if keyword argument :load-compiled-file is
missing or its value is the keyword :default, then it is treated as
:warn. If its value is 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 :load-compiled-file that 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 an 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-book form evaluated during the
course of evaluation of the present include-book form, 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.
The three -okp arguments, :uncertified-okp, defaxioms-okp,
and skip-proofs-okp, determine the system's behavior when the book or any
sub-book is found to be uncertified, when the book or any sub-book is found to
contain defaxiom events, and when the book or any sub-book is found to
contain skip-proofs events, 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. Exceptions:
:uncertified-okp t is ignored if the include-book is being performed
on behalf of a certify-book, and :uncertified-okp :ignore-certs
is an advanced option explained later in this topic.
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
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 non-local event forms in the file, assuming that each is admissible. Local events in the file are ignored. You may use include-book
to load several books, creating the logical world that contains
the definitions and theorems of all of them.
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 details.
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 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 include-book.
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. After
execution of an include-book form, the value of ACL2-defaults-table is restored to what it was immediately before that
include-book form was executed. See ACL2-defaults-table.
An advanced option is :uncertified-okp :ignore-certs. This tells ACL2
to ignore all certificate files while including the book and its
sub-books, thus treating all these books as uncertified. This option may be
useful when writing a .acl2x file for the first ``run'' of a ``two-runs
approach'' to certification; see set-write-ACL2x. Note however that
ordinary certification (the second ``run'') will then fail unless care is
taken to avoid :uncertified-okp :ignore-certs during that second
certification run. Finally (and speaking in general, not particularly about a
certify-book context), we emphasize that the option
:uncertified-okp :ignore-certs applies when including all sub-books, not
only for the current book. In particular, a subsidiary include-book call
specifying :uncertified-okp nil will fail, because the superior
:ignore-certs value causes the subsidiary book to be treated as
uncertified, which conflicts with the requirement of :uncertified-okp
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 environment variable ACL2_SYSTEM_BOOKS can be set to the
books/ directory under which they reside (a Unix-style pathname,
typically ending in books/ or 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:
If 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 book.