Major Section: OTHER
Below, when we talk about ``an event A'', we mean an event whose name is
A.
When event A is used in a proof performed to admit event B that you
submit to ACL2, we say that A is a ``proof-supporter'' of B. ACL2
stores an association list such that for every event B with at least one
proof-supporter, B is associated with a list of all of its
proof-supporters, sorted by symbol-<. The following form evaluates to
that alist, which is called the ``proof-supporters-alist''.
(global-val 'proof-supporters-alist (w state))By ``used in a proof'' above, we mean: applied as a rule or supplied explicitly via hints of type
:use, :by, or
:clause-processor. That is, the events ``used in a proof'' for
admitting an event E are those listed in the summary printed at the
conclusion of admitting E.
Note that if proofs are skipped when admitting event E, say because the
last admission of E was done by include-book (or certify-book,
which ends with an include-book), then there will be no entry in that
alist for E. (An exception is made however for encapsulate
events, where proof-supporters are remembered from the first pass; see
below.) So if you want the proof-supporters-alist to include supporters for
events in a book, use ld rather than include-book or
certify-book to process the events in that book. If however you are
interested in the proof-supporters FROM a book that support a later event,
then it is fine to include that book.
The case for encapsulate is slightly tricky. Consider an example of
the following form.
A ; event preceding the encapsulate (encapsulate () B (local C) ; uses A and B in a proof D ; uses C in a proof )At the conclusion of this
encapsulate event, the proof-supporters-alist
associates D with A and B, but not C (which has disappeared,
since it is local).Note that this sort of ``transitive closure'' operation is only performed
when necessary due to the disappearance of local events. For
example, if we replace (local C) above by just C, then D is
associated in the proof-supporters-alist only with C, not with A or
B. If you want the transitive closure of the relation computed by the
proof-supporters-alist, you have to compute it yourself. (This was a
deliberate design decision, in order to avoid slowing down event processing.)
However, there is help available on how to do such a computation:
A community book, books/misc/dead-events.lisp, does such a transitive
closure, and moreover uses that information to find ``dead events'' relative
to a list of ``desired'' events. For example, suppose you use LD to
process the events, with proofs, in a book intended to prove theorems
MAIN-1 and MAIN-2. (Remember, certify-book will not save such
information.) Suppose furthermore that the book begins with some
include-book forms followed by (deflabel book-start). You could
evaluate this form:
(dead-events '(main-1 main-2) :start 'book-start)The result is a list of events that you probably can delete from the book without causing any proofs to fail. See the
dead-events.lisp book for
further documentation.You might also find the code in the above book to be helpful for writing your own utilities based on the proof-supporters-alist.
