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.
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
"/home/smith/acl2/book-1.lisp"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".
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.
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.
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.