Include-book
Load the events in a file
Examples:
; Include using relative pathnames:
(include-book "my-arith")
(include-book "/../../my-arith")
; Include using absolute pathname:
(include-book "/home/smith/my-arith")
; Include a community book:
(include-book "arithmetic/top-with-meta" :dir :system)
; Include a project book:
(include-book "my-subdir/my-book" :dir :my-project)
General Form:
(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]
:dir directory)
where file is a book-name without the ".lisp" extension. 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, 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
the given file using the books/ directory of your ACL2 installation;
see ``Books Directory'' below. To define other keywords that can be used with
:dir, see add-include-book-dir, add-include-book-dir!, and
project-dir-alist. 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
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 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
nil.
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). If those books reside
elsewhere, the environment variable ACL2_SYSTEM_BOOKS can be set to the
directory under which they reside. 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/books
If you follow suggestions in the installation instructions, these books
will be the ACL2 community books; see community-books. For another way
to set the system books directory, which also permits similar handling for
other directories, see project-dir-alist.
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.
Subtopics
- Fast-cert
- A mode for faster, but possibly unsound, book certification
- Show-books
- Return a tree representing the included books.
