Hi ! I'd like to garbage collect my current projects: I've got some definitions/lemmas/theorems that are no longer used, and I want to detect them to remove them altogether. I thought of hacking a quick lexer to detect their names and "grep" them (I don't use much `Hint Resolve`

so it should be kind of ok), but I'm pretty sure there is a better way, or maybe an existing tool / solution around.

Could you point me in the right direction on how to perform dead code detection ? Thanks !

There is some "dead code removal" in the scripts for the bug minimizer: https://github.com/JasonGross/coq-tools

However it mostly acts on a single file AFAIK, and for multifile projects it tries to stick them into a single file.

Perhaps you could do some hackery with a purposely failing definition that contains all your "alive" theorems and minimize that. Then you could grep and compare what got left over?

Small example:

```
Definition a := 3.
Definition b := 2.
Definition c := 1.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0).
Fail Definition myStuff := (a, b).
```

If I minimize this, the bug minimizer should get rid of c. The notation lets me in theory have a very long list.

But then you need to already know which of your definitions are dead.

Only the "end results".

https://github.com/coq-community/coq-dpdgraph/ may have something for this

Say the goal of your project is to formalize some big theorem, then you can just keep that. All the deps will be kept.

Fair enough

https://github.com/coq-community/coq-dpdgraph/#dpdusage-find-unused-definitions-via-dpd-file

Gaëtan Gilbert said:

https://github.com/coq-community/coq-dpdgraph/ may have something for this

That is probably the better solution IMO. No hackery needed.

Thanks for all the ideas !

another form of analysis that finds "unused" stuff: https://github.com/engineeringsoftware/mcoq

Last updated: Aug 03 2024 at 00:02 UTC