1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
<html>
<head><title>ADD-INCLUDE-BOOK-DIR.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ADD-INCLUDE-BOOK-DIR</h2>associate directory to keyword for <code><a href="INCLUDE-BOOK.html">include-book</a></code>'s <code>:dir</code> argument
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example Form:
(add-include-book-dir :smith "/u/smith/")
; For (include-book "foo" :dir :smith), prepend "/u/smith/" to "foo".
<p>
General Form:
(add-include-book-dir kwd dir)
</pre>
where <code>kwd</code> is a <code><a href="KEYWORDP.html">keywordp</a></code> and <code>dir</code> is the absolute pathname
(see <a href="PATHNAME.html">pathname</a>) of a directory. The effect of this event is to modify the
meaning of the <code>:dir</code> keyword argument of <code><a href="INCLUDE-BOOK.html">include-book</a></code> as indicated
by the examples above, namely by associating the indicated directory with
the indicated keyword for purposes of the <code><a href="INCLUDE-BOOK.html">include-book</a></code> <code>:dir</code>
argument. See <a href="DELETE-INCLUDE-BOOK-DIR.html">delete-include-book-dir</a> for how to undo this effect.<p>
Caveat: The keyword <code>:system</code> cannot be redefined. It will always point to
the absolute pathname of the distributed books directory, which by default is
immediately under the directory where the ACL2 executable was originally
built (see <a href="INCLUDE-BOOK.html">include-book</a>, in particular the discussion there of ``books
directory'').<p>
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical <a href="WORLD.html">world</a> and is so recorded.<p>
This macro generates a call
<code>(table acl2-defaults-table :include-book-dir-alist ...)</code>
and hence is <code><a href="LOCAL.html">local</a></code> to any <a href="BOOKS.html">books</a> and <code><a href="ENCAPSULATE.html">encapsulate</a></code> <a href="EVENTS.html">events</a>
in which it occurs. See <a href="ACL2-DEFAULTS-TABLE.html">acl2-defaults-table</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
