Add-include-book-dir
Link keyword for :dir argument of ld and include-book
Example Forms:
; 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
event.
General Form:
(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 (:system
. filename) described in 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 or 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).
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
directory'').
This macro generates a table event that updates the table
include-book-dir!-table, which associates keywords with absolute
pathnames. However, as with add-include-book-dir, direct table
updates are disallowed; you must use add-include-book-dir! to add to the
table and delete-include-book-dir! to remove from the table.
It is illegal to call add-include-book-dir! in a local
context. (If you are tempted to do that, consider using add-include-book-dir instead.) To understand this restriction, imagine a
book that contains the following sequence of events.
(add-include-book-dir! :my-dir "path/to/BAD/dir")
(local (delete-include-book-dir! :my-dir))
(local (add-include-book-dir! :my-dir "path/to/GOOD/dir"))
(include-book "foo" :dir :my-dir)
(defthm f-def
(equal (f x) x))
During the first (proof) pass of certify-book, the book
path/to/GOOD/dir/foo.lisp will be included. But on the second pass, the
book path/to/BAD/dir/foo.lisp will be included. Now imagine that the
``good'' version contains the event (defun f (x) x) but the ``bad''
version instead contains the event (defun f (x) (not x)). Then we can
easily prove nil from the theorem f-def! Although it is likely that
book-hash values could catch this error at include-book time,
we prefer not to rely on these for soundness.
