Dead-events
Using proof supporters to identify dead code and unused theorems
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/tools/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.
