Major Section: SWITCHES-PARAMETERS-AND-MODES
Example Form: (add-include-book-dir :smith "/u/smith/") ; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".where
General Form: (add-include-book-dir kwd dir)
diris the pathname of a directory. The effect of this event is to modify the meaning of the
:dirkeyword argument of
include-bookas indicated by the examples above, namely by associating the indicated directory with the indicated keyword for purposes of the
:dirargument. By the ``indicated directory'' we mean, in the case that the pathname is a relative pathname, the directory relative to the current connected book directory; see cbd. See delete-include-book-dir for how to undo this effect.
A keyword that is already associated with a directory string by an existing
add-include-book-dir cannot be associated with a different
directory string. If that is your intention, first apply
delete-include-book-dir to that keyword; see delete-include-book-dir.
If however the new directory string is identical with the old, then the call
add-include-book-dir will be redundant (see redundant-events).
:system can never be redefined. It will always point to the
absolute pathname of the distributed books directory, which by default is
immediately under the directory where the ACL2 executable was originally
built (see include-book, in particular the discussion there of ``books
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
This macro generates a call
(table acl2-defaults-table :include-book-dir-alist ...)
and hence is
local to any books and
in which it occurs. See acl2-defaults-table. Even if you invoke
add-include-book-dir before certifying a book, so that this event is in a
book's portcullis rather than the book itself, nevertheless that
add-include-book-dir event will not be visible after the book is