Skip to content

feature request: more robust output format for dpdusage #63

@chdoc

Description

@chdoc

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)

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions