Add-include-book-dir
Link keyword for :dir argument of ld and include-book
Example Forms:
; For (include-book "foo" :dir :smith), prepend to "foo" the absolute
; directory pathmame "/u/smith/":
(add-include-book-dir :smith "/u/smith/")
; For (include-book "bar" :dir :util), prepend to "bar" the absolute
; directory pathname corresponding to the interpretation of "utilities/"
; with respect to the current connected-book-directory (cbd):
(add-include-book-dir :util "utilities")
; For (include-book "lib/floor-mod/top" :dir :arith), prepend to
; "lib/floor-mod/top" the string "<dir>/arithmetic-5/" where "<dir>"
; is the community books directory pathname string:
(add-include-book-dir :arith (:system . "arithmetic-5"))
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
event.
General Form:
(add-include-book-dir kwd dir)
where kwd is a keywordp and dir represents a directory:
either a relative or absolute pathname string or a sysfile. 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, when a relative pathname is supplied, 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
directory.
The keyword :system can never be redefined. It will always point to
the absolute pathname of the community-books directory, which by
default is the subdirectory "books/" of the directory where the ACL2
executable was built (see include-book, in particular the discussion
there of ``Books Directory'').
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.
