Major Section: BOOKS
Examples: "list-processing" "/usr/home/smith/my-arith"Book names are string constants that can be elaborated into file names. We elaborate book names by concatenating the ``connected book directory'' (see cbd) string on the left and some ``extension,'' such as
".lisp", on the right. However, the
connected book directory is not added if the book name itself
already represents an absolute file name. Furthermore,
include-book and certify-book temporarily reset the connected
book directory to be the directory of the book being processed.
This allows include-book forms to use file names without explicit
mention of the enclosing book's directory. This in turn allows
books (together with those that they include, using
include-book) to be moved between directories while maintaining
their certification and utility.You may wish to read elsewhere for details of ACL2 file name
conventions (see pathname), for a discussion of the filename
that is the result of the elaboration described here
(see full-book-name), and for details of the concept of the
connected book directory (see cbd). For details of how
include-book (see include-book) and certify-book
(see certify-book) use these concepts, see below.
Often a book name is simply the familiar name of the file.
(See full-book-name for discussion of the notions of
``directory string,'' ``familiar name,'' and ``extension''. These
concepts are not on the guided tour through books and you
should read them separately.) However, it is permitted for book
names to include a directory or part of a directory name. Book
names never include the extension, since ACL2 must routinely tack
several different extensions onto the name during include-book.
For example, include-book uses the ".lisp", ".cert" and
possibly the ".o" or ".lbin" extensions of the book name.
Book names are elaborated into full file names by include-book
and certify-book. This elaboration is sensitive to the
``connected book directory.'' The connected book directory is an
absolute filename string (see pathname) that is part of the
ACL2 state. (You may wish to see cbd and to
see set-cbd -- note that these are not on the guided tour).
If a book name is an absolute filename string, ACL2 elaborates it
simply by appending the desired extension to the right.
If a book name is a relative filename string, ACL2 appends the
connected book directory on the left and the desired extension on
the right.
Note that it is possible that the book name includes some partial
specification of the directory. For example, if the connected book
directory is "/usr/home/smith/" then the book name
"project/task-1/arith" is a book name that will be elaborated
to
"/usr/home/smith/project/task-1/arith.lisp".
Observe that while the events in this "arith" book are being
processed the connected book directory will temporarily be set to
"/usr/home/smith/project/task-1/".Thus, if the book requires other books, e.g.,
(include-book "naturals")then it is not necessary to specify the directory on which they reside provided that directory is the same as the superior book.
This inheritance of the connected book directory and its use to elaborate the names of inferior books makes it possible to move books and their inferiors to new directories, provided they maintain the same relative relationship. It is even possible to move with ease whole collections of books to different filesystems that use a different operating system than the one under which the original certification was performed.
The ".cert" extension of a book, if it exists, is presumed to
contain the most recent certificate for the book.
See certificate (or, if you are on the guided tour, wait until
the tour gets there).
See book-contents to continue the guided tour.
