coq-dpdgraph
coq-dpdgraph copied to clipboard
coq-community
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
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...
This is a PR for the whitelist feature that I suggested in #14.
The dpd file should contain line number and/or character position information and dpdusage should print it in a popular error message format, such that any decent editor can visit items...
Now that Coq 8.19.0 is out, a corresponding release of coq-dpdgraph should be done. The current version doesn't compile with error: ``` CAMLOPT -c searchdepend.ml File "searchdepend.mlg", line 53, characters...
Not an issue, more a progress report When this preparation is done, this issue could be kept open for later reference, but the similar issur for coq-8.16 should be closed....
- A COQBIN variable, if set and non-null is prepended to the PATH in `configure.ac`. The variables COQC, COQDOC and COQTOP now contain an absolute path. - I have also...
It's more or less standard that the `COQBIN` environment variable sets the directory where `coq` executables are to be found (this is especially convenient with a dev build). This should...
This time let us make sure that we are actually running the tests on CI for coq master: - [ ] CI running tests
Metadata
Owner
Metadata
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]