coq-dpdgraph icon indicating copy to clipboard operation
coq-dpdgraph copied to clipboard

feature request: more robust output format for dpdusage

Open chdoc opened this issue 6 years ago • 1 comments

Currently, dpdusage prints unused lemmas in an unspecified order that can change unpredictably when including another module in the analysis. In my current use-case (moving a theorem and everything only used to prove this theorem to a separate file) I was interested in the diff between the unused lemmas with and without the extra file. This required a sorted output without the Info line.

A typical invocation of dpdusage might thus look as follows:

dpdusage graph.dpd | grep -v '^Info:' | sed 's/\([^ :]*\):\([^\t]*\).*$/\1.\2/' | sort

(the use of . over : simplyfies copying lemma names into a "whitelist definition" as a hack until #14 is merged)

chdoc avatar Apr 05 '19 08:04 chdoc

OK. I'll see if I can add more features to dpdusage to match your needs.

Karmaki avatar Apr 05 '19 08:04 Karmaki