Add-include-book-dir!
Non-locally link keyword for :dir argument of ld
and include-book
Please see add-include-book-dir, which has completely
analogous syntax and semantics, except that add-include-book-dir! is not
local to the encapsulate or the book in which it occurs.
Probably add-include-book-dir is to be preferred unless you have a
good reason for wanting to export the effect of this event outside the
enclosing encapsulate or book.
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 is essentially 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.
