Major Section: BOOKS
Example: ACL2 !>:cbd "/usr/home/smith/"The connected book directory is a nonempty string that specifies a directory as an absolute pathname. (See pathname for a discussion of file naming conventions.) When
include-bookis given a relative book name it elaborates it into a full book name, essentially by appending the connected book directory string to the left and
".lisp"to the right. (For details, see book-name and also see full-book-name.) Furthermore,
include-booktemporarily sets the connected book directory to the directory string of the resulting full book name so that references to inferior books in the same directory may omit the directory. See set-cbd for how to set the connected book directory string.
General Form: (cbd)This is a macro that expands into a term involving the single free variable
state. It returns the connected book directory string.
The connected book directory (henceforth called the ``
include-book to elaborate the supplied book name into a
full book name (see full-book-name). For example, if the
"/usr/home/smith/" then the elaboration of the book-name
"project/task-1/arith" (to the
".lisp" extension) is
full-book-name is what include-book opens to read the
source text for the book.
cbd may be changed using
set-cbd (see set-cbd).
Furthermore, during the processing of the events in a book,
include-book sets the
cbd to be the directory string of the
full-book-name of the book. Thus, if the
"/usr/home/smith/" then during the processing of events by
cbdwill be set to
"/usr/home/smith/project/task-1/". Note that if
"arith"recursively includes a subbook, say
"naturals", that resides on the same directory, the
include-bookevent for it may omit the specification of that directory. For example,
"arith"might contain the event
(include-book "naturals").In general, suppose we have a superior book and several inferior books which are included by events in the superior book. Any inferior book residing on the same directory as the superior book may be referenced in the superior without specification of the directory.
We call this a ``relative'' as opposed to ``absolute'' naming. The use of relative naming is preferred because it permits books (and their accompanying inferiors) to be moved between directories while maintaining their certificates and utility. Certified books that reference inferiors by absolute file names are unusable (and rendered uncertified) if the inferiors are moved to new directories.
Technical Note and a Challenge to Users:
After elaborating the book name to a full book name,
opens a channel to the file to process the events in it. In some
host Common Lisps, the actual file opened depends upon a notion of
``connected directory'' similar to our connected book directory.
Our intention in always elaborating book names into absolute
filename strings (see pathname for terminology) is to
circumvent the sensitivity to the connected directory. But we may
have insufficient control over this since the ultimate file naming
conventions are determined by the host operating system rather than
Common Lisp (though, we do check that the operating system
``appears'' to be one that we ``know'' about). Here is a question,
which we'll pose assuming that we have an operating system that
calls itself ``Unix.'' Suppose we have a file name, filename, that
begins with a slash, e.g.,
"/usr/home/smith/...". Consider two
successive invocations of CLTL's
(open filename :direction :input)separated only by a change to the operating system's notion of connected directory. Must these two invocations produce streams to the same file? A candidate string might be something like
"/usr/home/smith/*/usr/local/src/foo.lisp"which includes some operating system-specific special character to mean ``here insert the connected directory'' or, more generally, ``here make the name dependent on some non-ACL2 aspect of the host's state.'' If such ``tricky'' name strings beginning with a slash exist, then we have failed to isolate ACL2 adequately from the operating system's file naming conventions. Once upon a time, ACL2 did not insist that the
cbdbegin with a slash and that allowed the string
"foo.lisp"to be tricky because if one were connected to
"/usr/home/smith/"then with the empty
"foo.lisp"is a full book name that names the same file as
"/usr/home/smith/foo.lisp". If the actual file one reads is determined by the operating system's state then it is possible for ACL2 to have two distinct ``full book names'' for the same file, the ``real'' name and the ``tricky'' name. This can cause ACL2 to include the same book twice, not recognizing the second one as redundant.