feature request: whitelist for dpdusage

[hendriktews]

Thanks for this very nice tool set!! Since I use Coq I have always been looking for a way to find unused definitions and lemmas.

My project has quite a few top-level theorems. They are reported by dpdusage, but I don't want to delete them. Moreover, I have a fair amount of technical lemmas that I want to keep, even though they are not used (currently). Because of this I am interested in a white-listing feature for dpdusage.

I am considering to open a PR that adds three things to dpdusage:

• an option -white-list <path>:<name>

• an option -white-list-file <file> that reads a file of white-listed names in the same format

• an option -strict-white-list that warns about a white-listed item with usage count above the threshold

What do you think?

[hendriktews]

In the future, it would be nice to extract the white list from the source code. For instance, I would like to white list all Theorem's and Proposition's. Or maybe there should be a dpdgraph command that adds an identifier to the white list.

[Karmaki]

Good idea. I am waiting for your PR then. Thanks.

[Karmaki]

It seems that your last proposition (white list all Theorem's and Proposition's) would need to add a new node_attribute in the .dpd format.

[chdoc]

I recently stumbled across this tool and I would like to second this feature request, in particular the whitelisting by keywords (i.e., Theorem as well as Proposition, Fact, and Example). Distinguishing between desired and undesired leaves in the graph could also allow for meaningful transitive reporting (e.g., reporting lemmas that are only used to prove undesired leaves).

[Karmaki]

OK. Maybe I should finish the old pull-request then (mainly add tests and resolve conflicts). I'll see if I can find some time to do that next week...

[chdoc]

It seems this issue has been dormant for a while. However, together with #63 it is what's currently keeping me from using dpdraph for my graph theory project. This project has some 1200 Lemmas and some 30+ Theorems, Propositions, and Facts (desired leaves), and I would be happy to better understand the (grown) dependency structure.