Link keyword for :dir argument of ld and include-book
; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".
(add-include-book-dir :smith "/u/smith/")
; For (include-book "bar" :dir :util), prepend absolute directory pathname
; corresponding to the relative pathname, "utilities/".
(add-include-book-dir :util "utilities")
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded. It
is local to the book or encapsulate form in which it occurs.
See add-include-book-dir! for a corresponding non-local
(add-include-book-dir kwd dir)
where kwd is a keywordp and dir is a relative or absolute
pathname for a directory, optionally using the syntax (:keyword
. filename) where :keyword is :system or, more generally, is
assigned in the project-dir-alist; also see full-book-name. If
the final '/' is missing for the resulting directory, ACL2 will add it
for you. The effect of this event is to modify the meaning of the :dir
keyword argument of include-book and ld as indicated by the
examples above, that is, by associating the indicated directory with the
indicated keyword for purposes of the :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.
For a keyword already associated with a directory string by a previous
invocation of add-include-book-dir or add-include-book-dir!, it
is illegal to associate a different directory string until removing the
existing association; see delete-include-book-dir (and see delete-include-book-dir! if the existing association was made by add-include-book-dir!. If however the new directory string is identical with
the existing one, which was already assigned by add-include-book-dir,
then the new call of add-include-book-dir will be redundant (see redundant-events).
See project-dir-alist for another way to associate keywords with
directory names, to take place only at the time ACL2 starts up. Note that a
keyword bound in the project-dir-alist may also be bound by
add-include-book-dir, but only if both bindings are to the same
The keyword :system can never be redefined. It will always point to
the absolute pathname of the system 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
This macro generates a table event that updates the ACL2-defaults-table and thus is automcatically local to the book or
encapsulate event in which it occurs (and, it is thus illegal to call
add-include-book-dir in an explicitly local context). See add-include-book-dir! for a corresponding non-local event.
As with add-include-book-dir!, direct table updates are disallowed;
you must use add-include-book-dir to add to the acl2-defaults-table
and delete-include-book-dir to remove from it.