With-cbd
To bind the connected book directory
With-cbd sets the connected book directory (see cbd)
within its scope.
Example Forms:
; Equivalent to (include-book "dir1/dir2/foo"):
(with-cbd "dir1"
(include-book "dir2/foo"))
; Equivalent to evaluation of the form,
; (include-book "arithmetic/top" :dir :system)'):
(with-cbd (cdr (assoc-eq :system (project-dir-alist (w state))))
(include-book "arithmetic/top"))
See cbd for a description of the connected book directory. The
“Technical Remark” there, about Lisp using the cbd to
elaborate relative pathnames, applied to with-cbd as well.
General Form:
(with-cbd str form)
where str evaluates to a nonempty string that represents the desired
directory (see pathname) and form evaluates to an error-triple.
The effect of (with-cbd str form) is to evaluate first (set-cbd
str) and then to evaluate form, after which the connected book
directory is restored to the value it had before that evaluation of
set-cbd. However, the implementation is designed so that the connected
book directory is restored even when the evaluation of form causes an
error.
The form (with-cbd str ev) is an event form if ev is an
event form; thus, it may occur in books as well as encapsulate
and progn events. See embedded-event-form. But in an event context, str must be a string, not merely an expression that
evaluates to a string.
Finally, note that Lisp compilers may vary in how they handle functions
defined within the scope of with-cbd. If you find an example of slower
execution caused by using with-cbd, please feel free to send it to the
ACL2 implementors.
