Using proof supporters to identify dead code and unused theorems

Below, when we talk about ``an event

When event `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

Note that if proofs are skipped when admitting event `include-book` (or
`include-book`), then there will
be no entry in that alist 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

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

A community book, `ld` to
process the events, with proofs, in a book intended to prove theorems
`certify-book` will not save
such information.) Suppose furthermore that the book begins with some `include-book` forms followed by

(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

You might also find the code in the above book to be helpful for writing your own utilities based on the proof-supporters-alist.