		Search-engine friendly clone of the ACL2 documentation.

Books-tour

Book-name

Conventions associated with book names

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.