|
|
|---|
|
|
|
|---|
Conventions associated with book-names
Examples: "list-processing" "/usr/home/smith/my-arith"
A book-name is typically a string constant that represents a file.
(Much later below we discuss other book-names that are not strings, namely,
sysfiles; but till then we consider only strings.) We elaborate book
names by concatenating the ``connected book directory'' (see cbd)
string on the left and perhaps a
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 a book-name to include a directory or part of a directory
name. Book-names often do not include the extension, since ACL2 must
routinely tack several different extensions onto the name during include-book. For example, include-book uses the
A book-name is elaborated into a full-book-name 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/project/task-1/arith.lisp".
Observe that while the events in this
"/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
Finally we mention another kind of book-name: a sysfile, which is a pair that associates a keyword with a directory pathname. This kind of book-name is used by the implementation, for example in certificate files, but is rarely visible to users. If you run across a sysfile and want to understand more about it, see sysfile.
See book-contents to continue the guided tour.