how we know if include-book read the correct files
Major Section:  BOOKS

The certificate (see certificate for general information) of a certified file is divided into two parts, a portcullis and a keep. These names come from castle lore. The keep is the strongest and usually tallest tower of a castle from which the entire courtyard can be surveyed by the defenders. The keep of a book is a list of file names and check sums used after the book has been included, to determine if the files read were (up to check sum) those certified.

Once the portcullis is open, include-book can enter the book and read the event forms therein. The non-local event forms are in fact executed, extending the host theory. That may read in other books. When that has been finished, the keep of the certificate is inspected. The keep is a list of the book names which are included (heritarily through all subbooks) in the certified book (including the certified book itself) together with the check sums of the objects in those books at the time of certification. We compare the check sums of the books just included to the check sums of the books stored in the keep. If differences are found then we know that the book or one of its subbooks has been changed since certification.

See include-book to continue the guided tour through books.


introduction to filename conventions in ACL2
Major Section:  BOOKS

The notion of pathname objects from Common Lisp is not supported in ACL2, nor is the function pathname. However, ACL2 supports file operations, using conventions for naming files based on those of the Unix (trademark of AT&T) operating system, so that character / is used to terminate directory names. Some file names are ``absolute'' (complete) descriptions of a file or directory; others are ``relative'' to the current working directory or to the connected book directory (see cbd). We emphasize that even for users of Windows-based systems or Macintosh computers, ACL2 file names are in the Unix style. We will call these ACL2 pathnames, often omitting the ``ACL2.''

Pathnames starting with the directory separator (/) are absolute pathnames. All other pathnames are relative pathnames. An exception is in the Microsoft Windows operating system, where the drive may be included, e.g., "c:/home/smith/acl2/book-1.lisp". In fact, the drive must be included in the portcullis of a book; see portcullis.

Consider the following examples. The filename string

is an absolute pathname, with top-level directory "home", under that the directory "smith" and then the directory "acl2", and finally, within that directory the file "book-1.lisp". If the the connected book directory is "/home/smith/" (see cbd), then the filename string above also corresponds to the relative filename string "acl2/book1.lisp".


the gate guarding the entrance to a certified book
Major Section:  BOOKS

The certificate (see certificate for general information) of a certified file is divided into two parts, a portcullis and a keep. These names come from castle lore. The portcullis of a castle is an iron grate that slides up through the ceiling of the tunnel-like entrance. The portcullis of a book insures that include-book does not start to read the book until the appropriate context has been created.

Technically, the portcullis consists of the version number of the certifying ACL2, a list of commands used to create the ``certification world'' and an alist specifying the check sums of all the books included in that world. The portcullis is constructed automatically by certify-book from the world in which certify-book is called, but that world must have certain properties described below. After listing the properties we discuss the issues more leisurely.

Each command in the portcullis must be either a defpkg form or an embedded event form (see embedded-event-form). In addition, we exclude include-book events unless the name of the included book is an absolute filename (see pathname). Thus, under Unix (trademark of AT&T) any string supplied to include-book in the portcullis must begin with a slash (/); under MacOS, this string must not begin with a colon (:); and under Windows, this string must begin with a drive followed by a colon and a slash (e.g., C:/). Since the portcullis commands are recovered automatically by certify-book, this restriction on the form of portcullis commands naturally becomes a restriction on the world in which certify-book may be called. We explain the exclusion after discussing the general issues.

Consider a book to be certified. The book is a file containing event forms. Suppose the file contains references to such symbols as my-pkg::fn and acl2-arith::cancel, but that the book itself does not create the packages. Then a hard Lisp error would be caused merely by the attempt to read the expressions in the book. The corresponding defpkgs cannot be written into the book itself because the book must be compilable and Common Lisp compilers differ on the rules concerning the inline definition of new packages. The only safe course is to make all defpkgs occur outside of compiled files.

More generally, when a book is certified it is certified within some logical world. That ``certification world'' contains not only the necessary defpkgs but also, perhaps, function and constant definitions and maybe even references to other books. When certify-book creates the certificate for a file it recovers from the certification world the commands used to create that world from the initial ACL2 world. Those commands become part of the portcullis for the certified book. In addition, certify-book records in the portcullis the check sums (see check-sum) of all the books included in the certification world.

Include-book presumes that it is impossible even to read the contents of a certified book unless the portcullis can be ``raised.'' To raise the portcullis we must be able to execute (possibly redundantly, but certainly without error), all of the commands in the portcullis and then verify that the books thus included were identical to those used to build the certification world (up to check sum). This raising of the portcullis must be done delicately since defpkgs are present: we cannot even read a command in the portcullis until we have successfully executed the previous ones, since packages are being defined.

Clearly, a book is most useful if it is certified in the most elementary extension possible of the initial logic. If, for example, your certification world happens to contain a defpkg for "MY-PKG" and the function foo, then those definitions become part of the portcullis for the book. Every time the book is included, those names will be defined and will have to be either new or redundant (see redundant-events). But if those names were not necessary to the certification of the book, their presence would unnecessarily restrict the utility of the book.

Recall that we disallow include-book events from the portcullis unless the included book's name is an absolute filename (See pathname). Thus, for example, under the Unix operating system it is impossible to certify a book if the certification world was created with

ACL2 !>(include-book "arith")
The problem here is that the file actually read on behalf of such an include-book depends upon the then current setting of the connected book directory (see cbd). That setting could be changed before the certification occurs. If we were to copy (include-book "arith") into the portcullis of the book being certified, there is no assurance that the "arith" book included would come from the correct directory. However, by requiring that the include-books in the certification world give book names that begin with slash we effectively require you to specify the full file name of each book involved in creating your certification world. Observe that the execution of
(include-book "/usr/local/src/acl2/library/arith")
does not depend on the current book directory. On the other hand, this requirement -- effectively that absolute file names be used in the certification world -- means that a book that requires another book in its certification world will be rendered uncertified if the required book is removed to another directory. If possible, any include-book command required for a book ought to be placed in the book itself and not in the certification world. The only time this cannot be done is if the required book is necessary to some defpkg required by your book. Of course, this is just the same advice we have been giving: keep the certification world as elementary as possible.

See keep to continue the guided tour of books.


to set the connected book directory
Major Section:  BOOKS

Example Forms:
ACL2 !>:set-cbd "/usr/home/smith/"
ACL2 !>:set-cbd "my-acl2/books"
See cbd for a description of the connected book directory.

General Form:
(set-cbd str)

where str is a nonempty string that represents the desired directory (see pathname). This command sets the connected book directory (see cbd) to the string representing the indicated directory. Thus, this command may determine which files are processed by include-book and certify-book commands typed at the top-level. However, the cbd is also temporarily set by those two book processing commands.

IMPORTANT: Pathnames in ACL2 are in the Unix (trademark of AT&T) style. That is, the character ``/'' separates directory components of a pathname, and pathnames are absolute when they start with this character, and relative otherwise. See pathname.


invalid certificates and uncertified books
Major Section:  BOOKS

Include-book has a special provision for dealing with uncertified books: If the file has no certificate or an invalid certificate (i.e., one whose check sums describe files other than the ones actually read), a warning is printed and the book is otherwise processed as though it were certified and had an open portcullis. (For details see books, see certificate, and see portcullis.)

This can be handy, but it can have disastrous consequences.

The provision allowing uncertified books to be included can have disastrous consequences, ranging from hard lisp errors, to damaged memory, to quiet logical inconsistency.

It is possible for the inclusion of an uncertified book to render the logic inconsistent. For example, one of its non-local events might be (defthm t-is-nil (equal t nil)). It is also possible for the inclusion of an uncertified book to cause hard errors or breaks into raw Common Lisp. For example, if the file has been edited since it was certified, it may contain too many open parentheses, causing Lisp to read past ``end of file.'' Similarly, it might contain non-ACL2 objects such as 3.1415 or ill-formed event forms that cause ACL2 code to break.

Even if a book is perfectly well formed and could be certified (in a suitable extension of ACL2's initial world), its uncertified inclusion might cause Lisp errors or inconsistencies! For example, it might mention packages that do not exist in the host world. The portcullis of a certified book insures that the correct defpkgs have been admitted, but if a book is read without actually raising its portcullis, symbols in the file, e.g., acl2-arithmetic::fn, could cause ``unknown package'' errors in Common Lisp. Perhaps the most subtle disaster occurs if the host world does have a defpkg for each package used in the book but the host defpkg imports different symbols than those required by the portcullis. In this case, it is possible that formulas which were theorems in the certified book are non-theorems in the host world, but those formulas can be read without error and will then be quietly assumed.

In short, if you include an uncertified book, all bets are off regarding the validity of the future behavior of ACL2.

That said, it should be noted that ACL2 is pretty tough and if errors don't occur, the chances are that deductions after the inclusion of an uncertified book are probably justified in the (possibly inconsistent) logical extension obtained by assuming the admissibility and validity of the definitions and conjectures in the book.