Tool for drawing coq project dependency graph?

Using Coq
1

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?

2 Likes
2

I usually use a script like the following one:

#!/bin/sh

project_file=_CoqProject
name=dependency_graph
dot_file=${name}.dot
pdf_file=${name}.pdf

# 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}
3 Likes
3

To see a finer-grained dependency graph (at the level of Coq objects), there exists a Coq plugin: https://github.com/Karmaki/coq-dpdgraph/

3 Likes
4

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

5

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

6

_CoqProject files simply list the files with a top line giving options such as the -R or the -Q option. Cf. https://coq.inria.fr/refman/practical-tools/utilities.html#building-a-coq-project.

1 Like
7

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

8

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

9

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?

10

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.

11

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

12

What’s the status of this? dumpgraph is also used here:

Dpd-graph seems complicated.

Here’s a haskell tool to build a graph. Maybe it should be moved to a more central place?
https://github.com/HoTT/HoTT/blob/master/etc/DepsToDot.hs

13

There’s this, but I haven’t tried it yet.
I’m hesitant just running unknown code from the internet.

14

What did you find complicated about dpd-graph? I remember using it once or twice, and besides maybe a missing shell script wrapper calling the necessary conversion programs I remember it working pleasantly. Maybe that changed in the more recent Coq versions?

coq-dpdgraph seems however to only give you a graph with theorems as nodes, rather than modules / files as nodes.

15

It’s been a constant source of trouble in the HoTT library. Perhaps it’s better now.

And indeed, I’m more interested in a depgraph of the files/modules.

16

For what is worth, here is the snippet of code I use to generate my dependency graphs:

( echo "digraph interval_deps {" ;
  echo "node [shape=ellipse, style=filled, URL=\"html/Interval.\N.html\", color=black];";
  ( cd src; coqdep -R . Interval $VFILES ) |
    sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
    while read src dst; do
      color=$(echo "$src" | sed -e 's,Real.*,turquoise,;s,Interval[.].*,plum,;s,Integral.*,lightcoral,;s,Poly.*,yellow,;s,Float.*,cornflowerblue,;s,Eval.*,green,;s,[A-Z].*,white,')
      echo "\"$src\" [fillcolor=$color];"
      for d in $dst; do
        echo "\"$src\" -> \"${d%.vo}\" ;"
      done
    done;
  echo "}" ) | tred > deps.dot
dot -T png deps.dot > deps.png
dot -T cmap deps.dot | sed -e 's,>$,/>,' > deps.map

This produces two files deps.png and deps.map which can then be embedded into a webpage. The specific parts in the script above are the src physical path and the Interval logical path, as well as the color line, which is used to split the library into various sublibraries. This gives the following graph: CoqInterval. The same kind of script is used for Flocq and Coquelicot

2 Likes