Cbd
Connected book directory string
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.)
Similarly, ld elaborates relative pathnames into full pathnames using
the connected book directory string. (The effect of the cbd on ld
carries over to utilities that invoke ld as well, notably, rebuild.) Furthermore, include-book and ld temporarily set
the connected book directory to the directory string of the resulting full
pathname so that references to files 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); similarly for ld. 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; similarly for ld. 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 sub-book, 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.
