Add-include-book-dir!
Non-locally link keyword for :dir argument of ld
and include-book
This topic assumes familiarity with 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.
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.
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.
