INCLUDE-BOOK

load the events in a file
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 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, :warn, :try, :comp-raw, or :comp; these values are explained below, and the default is :warn unless compilation is suppressed (see compilation). 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, :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 used for 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-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.

The value, action, of :load-compiled-file is coerced to nil if explicit compilation is suppressed (see compilation), presumably because the host Lisp implementation automatically compiles on the fly. The remainder of this paragraph assumes that explicit compilation is not suppressed. We also mention here a special value :comp! for action, which is treated exactly as described for :comp below (and hence is not mentioned further), except that if a compiled file already exists then it is deleted before any action described below. We now describe the effect of action under the above assumptions. If there is a compiled file for the book that was created more recently than the book itself and the value, action, of the :load-compiled-file argument is not nil, or is omitted, then the compiled file is automatically loaded; otherwise it is not loaded. If the compiled file is not loaded, then an error will occur if action is t; if action is :warn (the default) then a warning will be printed; if action is :try then no warning will be printed; and if action is :comp (or :comp!) then the file will be immediately compiled and loaded. In this case, :comp (likewise, :comp!) causes a file to be compiled that includes executable counterparts, in analogy to default value t for the compile-flg argument of certify-book (see certify-book). The action :comp-raw is handled just like :comp, with two exceptions: compilation may be skipped if it is not needed, and executable counterparts are not also compiled. Certify-book can also be used to compile a book; thus, :comp-raw and :comp do the same sort of compilation for include-book as is done by certify-book when the latter is given a compile-flg of :raw or t, respectively. 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. NOTES: (1) The :load-compiled-file argument is not recursive; that is, calls of include-book that are inside the book supplied to include-book will use their own :load-compiled-file arguments (default :warn), not the :load-compiled-file argument for the enclosing book. (2) Only functions defined non-redundantly in the book (and their executable counterparts in circumstances as described above) are compiled, not functions defined in sub-books or in the certification world (see portcullis).

The three -okp arguments, :uncertified-okp, defaxioms-okp, and 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 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. Exception: :uncertified-okp is ignored if the include-book is being performed on behalf of a certify-book.

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.

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.

Distributed Books Directory. We refer to the ``books directory'' of an executable image as the full pathname string of the books directory associated with :dir :system for that image. This is where the distributed books directory should reside. 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:

export ACL2_SYSTEM_BOOKS
ACL2_SYSTEM_BOOKS=/home/acl2/v3-2/acl2-sources/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.

:cited-by Programming