CBD

connected book directory string 
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-book is 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-book temporarily 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 ``cbd'') is used by include-book to elaborate the supplied book name into a full book name (see full-book-name). For example, if the cbd is "/usr/home/smith/" then the elaboration of the book-name "project/task-1/arith" (to the ".lisp" extension) is "/usr/home/smith/project/task-1/arith.lisp". That full-book-name is what include-book opens to read the source text for the book.

The 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 cbd is "/usr/home/smith/" then during the processing of events by 

(include-book "project/task-1/arith")
the cbd will 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-book event 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, include-book 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 cbd begin 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 cbd "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.