Overview graph

[yforster]

When @dominik-kirst was hunting the universe problem, I tried to create a dependency graph of the library, but without success. With the help of the Enrico Tassi I managed to do it based on some mathcomp scripts.

Here's the code:

-- coqdep -f _CoqProject > depend
-- cat depend | ./buildgraph > depend.dot
-- dot -Tsvg depend.dot > depend.svg

with the adapted buildlibgraph file from https://github.com/math-comp/math-comp/blob/master/etc/buildlibgraph as attached. I also attach the svg output and conclude that's it's pretty much useless unless one really has a specific dependency to trace for e.g. universe problems.

(GitHub doesn't allow me to upload arbitrary file endings. The buildlibgraph file should have no ending, the other one should be depend.svg)

buildlibgraph.txt depend.txt