include-book
's :dir
argument
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".whereGeneral Form: (add-include-book-dir kwd dir)
kwd
is a keywordp
and dir
is the pathname of a
directory. The effect of this event is to modify the meaning of the :dir
keyword argument of include-book
as indicated by the examples above,
namely by associating the indicated directory with the indicated keyword for
purposes of the include-book
:dir
argument. 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
invocation of 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
of add-include-book-dir
will be redundant (see redundant-events).
The keyword :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
directory'').
This macro generates (in essence) a call
(table acl2-defaults-table :include-book-dir-alist ...)
and hence is local
to any books and encapsulate
events
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
among the book's portcullis commands rather than in the book itself,
nevertheless that add-include-book-dir
event will not be visible after
the book is included. (Note: The above behavior is generally preserved in
raw-mode (see set-raw-mode),though by means other than a table.)