Stream: Coq devs & plugin devs

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


view this post on Zulip 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 !

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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).

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

view this post on Zulip Ana de Almeida Borges (May 31 2022 at 09:44):

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

view this post on Zulip Ali Caglayan (May 31 2022 at 09:46):

Only the "end results".

view this post on Zulip Gaëtan Gilbert (May 31 2022 at 09:46):

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

view this post on Zulip Ali Caglayan (May 31 2022 at 09:46):

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

view this post on Zulip Ana de Almeida Borges (May 31 2022 at 09:46):

Fair enough

view this post on Zulip Gaëtan Gilbert (May 31 2022 at 09:47):

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

view this post on Zulip Ali Caglayan (May 31 2022 at 09:47):

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.

view this post on Zulip Vincent Siles (May 31 2022 at 11:39):

Thanks for all the ideas !

view this post on Zulip Karl Palmskog (May 31 2022 at 16:40):

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


Last updated: Feb 06 2023 at 00:03 UTC