using proof supporters to identify dead code and unused theorems
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
 (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 distributed 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.