Include-book-paths
List paths via include-book down to a given book
General Form:
(include-book-paths book
&key
excluded-books ; default nil
dir ; default (cbd)
verbose ; default t
return ; default *include-book-paths-default-count*
)
where all arguments are evaluated. The value of the first argument,
book, evaluates to a string that is interpreted as a book name, where the
".lisp" suffix is optional. Excluded-books evaluates to a list of
such strings. Note that in this context, a book name can be an absolute
pathname or it can be relative to the directory dir, which by default is
the cbd but can be any directory name or any legal value of the
:dir argument for include-book, e.g., :dir :system. By
default some progress messages are printed; use :verbose nil to turn them
off. We describe the :return keyword argument later below.
Example:
(include-book "kestrel/utilities/include-book-paths" :dir :system)
(include-book "arithmetic/top" :dir :system)
(include-book-paths "cowles/acl2-asg.lisp"
:dir :system
:excluded-books '("meta/meta-times-equal")
:verbose nil
:return t)
Description
Evaluation of the form (include-book-paths A) returns an error-triple. In the case of no error, the value is a list consisting of
maximal paths through the ``immediately included by'' relation, defined below,
that terminate in the given book name, A. The form
(include-book-paths A :excluded-books (list B1 ... Bn)) produces a
similar result, except that all paths that contain any Bi are excluded
from the result. This supports the motivation for writing this tool, which is
to reduce the set of books on which a given book depends (via
include-book, hereditarily). If you are contemplating the possibility of
removing dependence on each Bi, then (include-book-paths A (list B1
... Bn)) will give you remaining paths that cause the current session to
depend on book A.
The entries in the paths may be of the form (:keyword . string), for
example, (:SYSTEM . "arithmetic/top.lisp"). See sysfile for a
discussion of this format.
By default, the maximum number of paths returned is the value of the
constant *include-book-paths-default-count*, which is
100. If the value of keyword :return
is a natural number, then this number is used in place of that default. If
the number of maximal paths exceeds the specified maximum, m, then only
the first m paths are returned; otherwise all such paths are returned.
Regardless, the full list of maximal paths is stored in state global
variable include-book-paths-last. If the value of keyword argument
:return is supplied as other than a natural number, then all such maximal
paths are returned, except that if the value is nil, then no paths are
returned.
Details: the algorithm and the notion of ``immediately included by''
The algorithm is based on the binary relation ``A is immediately included
by B'', defined as follows. First let us say that ``A is included by B'' (or
``B includes A'') if within the book B or its portcullis commands there is an include-book of A, which may be local.
Then A is immediately included by B (or, B immediately includes A) when B
includes A but there is no book C such that B includes C and C includes A.
Suppose for example that book B contains the following forms, where also book
C includes book A.
(include-book A)
(include-book C) ; where C includes A
This is equivalent to the following — and they are equivalent from a
dependency standpoint even if either or both of the include-book forms are
local.
(include-book C) ; where C includes A
Even though B includes A, nevertheless, since also B includes C which
includes A, then A is not immediately included by B. The result of
include-book-paths will include at least one path from B through C to A,
but no path for which B is adjacent to A. Our contention is that
``immediately includes'' is the right notion for dependency analysis since
seeing two paths with B connected to A — one with B adjacent to A and
one with B connected to C, which is connected to A — isn't particularly
helpful, and is perhaps misleading (given the equivalent displays above).
The ``immediately included by'' directed acyclic graph, iib-dag
The ``immediately included by'' relation is actually a directed acyclic
graph, which we call the ``iib-dag''. The first step in the
include-book-paths algorithm is to build the iib-dag from the certificates of all books included in the current ACL2 world (locally or not). You can compute the iib-dag yourself by evaluating the
form
(include-book-dag ctx state)
where ctx is a context for error messages and state is the
ACL2 state, and the result is an error-triple whose value in the
non-error case is the current iib-dag.
The iib-dag is actually cached in the state global variable
include-book-dag-cache, whose value is either nil or of the form
(cons include-book-alist-all iib-dag) where iib-dag is the iib-dag
computed in a world w for which include-book-alist-all is the value
of (global-val 'include-book-alist-all w). Thus, if no include-book events have been evaluated or undone since the last time the
iib-dag was computed, then the iib-dag will simply be looked up in the cache.
This is an important optimization, since building the iib-dag is probably the
most time-consuming part of the include-book-paths algorithm.
Remark. As noted above, the iib-dag is computed from the certificates of all of the books included in the session (locally or
not). A duplicate-free list of all such books can be computed as follows.
(remove-duplicates-equal
(strip-cars (global-val 'include-book-alist-all (w state))))
