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: Dec 05 2023 at 12:01 UTC