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
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
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
Observe that while the events in this
Thus, if the book requires other books, e.g.,
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.
See book-contents to continue the guided tour.