Tool for drawing coq project dependency graph?

Let’s suppose I downloaded, for example, Compcert development from Github and want to see dependency graph to better understand order in which to study all the files. Is there some tool to draw nice picture of the graph?


I usually use a script like the following one:



# Generate "dot" file with module dependencies
# `coqdep` is a standard utility distributed with Coq system
coqdep -f ${project_file} -dumpgraph ${dot_file} > /dev/null

# Generate a pdf with toposorted graph from the dot file
# `dot` utility is distributed with graphviz utility collection
# One can usually install it using a package manager like homebrew on macOS:
#    brew install graphviz
dot -Tpdf ${dot_file} -o ${pdf_file}

To see a finer-grained dependency graph (at the level of Coq objects), there exists a Coq plugin:


@anton-trunov note that this coqdep feature has just been removed in the master branch.

Possibly stupid question, but what to do if I can find no _CoqProject file? How to make one?

_CoqProject files simply list the files with a top line giving options such as the -R or the -Q option. Cf.

1 Like

@ppedrot Wow. That’s too bad! Is there any way to recover it? (probably using some other tool or whatever?)

@anton-trunov you might try to ask @ejgallego, he is the one who wrote that PR.

The feature was removed to simplify the code of coqdep and because it was believed that these options were unused. However, the fact that this one in particular was actually used seems for me to be reason enough to revert that particular removal (should be easy to do).

BTW, the changelog says:

several deprecated options have been removed: -w , -D , -mldep , -prefix , -slash , and -dumpbox

Shouldn’t -dumpbox be -dumpgraph?

We could re-add dumpgraph, you can also just take the regular output of coqdep and generate the graph with a very simple script.

I kind of prefer that coqdep does only one thing [well] and other tools do consume the info in the way they need, after all the format is very easy to parse.

In fact I’d be surprised if there isn’t already a Makefile to dot converter somewhere [coqdep outputs make rules]