Dead "code" detection / GC of unused definitions · Coq devs & plugin devs

Stream: Coq devs & plugin devs

Topic: Dead "code" detection / GC of unused definitions

Vincent Siles (May 31 2022 at 06:42):

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 !

Ali Caglayan (May 31 2022 at 09:38):

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

Ali Caglayan (May 31 2022 at 09:38):

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?

Ali Caglayan (May 31 2022 at 09:43):

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).