Skip to content

Commit 8fb4e39

Browse files
proux01proux01
committed
Add dependency graph
1 parent 1bbde78 commit 8fb4e39

File tree

5 files changed

+167
-13
lines changed

5 files changed

+167
-13
lines changed

‎Makefile

+5-1
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,13 @@ FOOTER=doc/common/styles/html/coqremote/header.html
3030

3131
stdlib-html: all doc/stdlib/index-list.html
3232
mkdir -p html
33+
cp doc/stdlib/depends.png html/
3334
coqdoc -q -d html --with-header $(HEADER) --with-footer $(FOOTER) --multi-index --html -g -R theories Stdlib $(shell find theories -name "*.v")
3435
mv html/index.html html/genindex.html
3536
cat $(HEADER) doc/stdlib/index-list.html $(FOOTER) > html/index.html
3637

37-
doc/stdlib/index-list.html: doc/stdlib/make-library-index doc/stdlib/index-list.html.template doc/stdlib/hidden-files
38+
doc/stdlib/depends.png: doc/stdlib/depends
39+
dot -Tpng $< -o $@
40+
41+
doc/stdlib/index-list.html: doc/stdlib/depends.png doc/stdlib/make-library-index doc/stdlib/index-list.html.template doc/stdlib/hidden-files
3842
doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files

‎dev/tools/depends-rm-loops.awk

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{
2+
if ($1 != substr($3, 1, length($3)-1)) {
3+
print $0
4+
}
5+
}

‎dev/tools/make-depends.sh

+86-12
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,90 @@
11
#!/bin/sh
22

3-
DIR= $(dirname $0)
4-
echo "DIR = \"$DIR\""
3+
# this should be call from root as
4+
# % dev/tools/make-depends.sh
55

6+
(echo "digraph stdlib_deps {";
7+
coqdep -R theories Coq theories | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*v//p' | \
8+
while read src dst; do
9+
for d in $dst; do
10+
d=${d#theories.}
11+
echo "\"${src#theories.}\" -> \"${d%.vo}\" ;"
12+
done
13+
done;
14+
echo "}") | tred \
15+
| sed -e 's/"Arith[.]All[.][^"]*"/"coq-stdlib-arith"/g' \
16+
| sed -e 's/"Arith[.]Base[.][^"]*"/"coq-stdlib-arith-base"/g' \
17+
| sed -e 's/"Numbers[.]NumPrelude"/"coq-stdlib-arith-base"/g' \
18+
| sed -e 's/"Numbers[.]NatInt[.][^"]*"/"coq-stdlib-arith-base"/g' \
19+
| sed -e 's/"Numbers[.]Natural[.]Abstract[.][^"]*"/"coq-stdlib-arith-base"/g' \
20+
| sed -e 's/"Classes[.]Arith[.][^"]*"/"coq-stdlib-arith-base"/g' \
21+
| sed -e 's/"Bool[.][^"]*"/"coq-stdlib-bool"/g' \
22+
| sed -e 's/"Classes[.]All[.][^"]*"/"coq-stdlib-classes"/g' \
23+
| sed -e 's/"Logic[.]Classical[.][^"]*"/"coq-stdlib-classical-logic"/g' \
24+
| sed -e 's/"Compat[.][^"]*"/"coq-stdlib-compat"/g' \
25+
| sed -e 's/"derive[.][^"]*"/"coq-stdlib-derive"/g' \
26+
| sed -e 's/"extraction[.]All[.][^"]*"/"coq-stdlib-extraction"/g' \
27+
| sed -e 's/"extraction[.]Base[.][^"]*"/"coq-stdlib-extraction-base"/g' \
28+
| sed -e 's/"QArith[.]Field[.][^"]*"/"coq-stdlib-field"/g' \
29+
| sed -e 's/"setoid_ring[.]Q[.][^"]*"/"coq-stdlib-field"/g' \
30+
| sed -e 's/"FSets[.][^"]*"/"coq-stdlib-fmaps-fsets-msets"/g' \
31+
| sed -e 's/"MSets[.][^"]*"/"coq-stdlib-fmaps-fsets-msets"/g' \
32+
| sed -e 's/"funind[.][^"]*"/"coq-stdlib-funind"/g' \
33+
| sed -e 's/"omega[.][^"]*"/"coq-stdlib-lia"/g' \
34+
| sed -e 's/"micromega[.]Zify[.][^"]*"/"coq-stdlib-lia"/g' \
35+
| sed -e 's/"micromega[.]Lia[.][^"]*"/"coq-stdlib-lia"/g' \
36+
| sed -e 's/"Lists[.][^"]*"/"coq-stdlib-list"/g' \
37+
| sed -e 's/"Numbers[.]NaryFunctions"/"coq-stdlib-list"/g' \
38+
| sed -e 's/"Logic[.]Lists[.][^"]*"/"coq-stdlib-list"/g' \
39+
| sed -e 's/"Classes[.]Lists[.][^"]*"/"coq-stdlib-list"/g' \
40+
| sed -e 's/"Logic[.]Base[.][^"]*"/"coq-stdlib-logic"/g' \
41+
| sed -e 's/"micromega[.]Lqa[.][^"]*"/"coq-stdlib-lqa"/g' \
42+
| sed -e 's/"NArith[.][^"]*"/"coq-stdlib-narith"/g' \
43+
| sed -e 's/"nsatz[.][^"]*"/"coq-stdlib-nsatz"/g' \
44+
| sed -e 's/"Structures[.]Ex[.][^"]*"/"coq-stdlib-orders-ex"/g' \
45+
| sed -e 's/"Numbers[.]AltBinNotations"/"coq-stdlib-orders-positive"/g' \
46+
| sed -e 's/"PArith[.][^"]*"/"coq-stdlib-positive"/g' \
47+
| sed -e 's/"Array[.][^"]*"/"coq-stdlib-primitive-array"/g' \
48+
| sed -e 's/"Floats[.][^"]*"/"coq-stdlib-primitive-floats"/g' \
49+
| sed -e 's/"Numbers[.]Cyclic[^"]*"/"coq-stdlib-primitive-int"/g' \
50+
| sed -e 's/"micromega[.]Int63[^"]*"/"coq-stdlib-primitive-int"/g' \
51+
| sed -e 's/"Strings[.]PString"/"coq-stdlib-primitive-string"/g' \
52+
| sed -e 's/"Program[.]All[.][^"]*"/"coq-stdlib-program"/g' \
53+
| sed -e 's/"QArith[.]All[.][^"]*"/"coq-stdlib-qarith"/g' \
54+
| sed -e 's/"Numbers[.]Q[.][^"]*"/"coq-stdlib-qarith"/g' \
55+
| sed -e 's/"QArith[.]Base[.][^"]*"/"coq-stdlib-qarith-base"/g' \
56+
| sed -e 's/"Reals[.][^"]*"/"coq-stdlib-reals"/g' \
57+
| sed -e 's/"setoid_ring[.]R[.][^"]*"/"coq-stdlib-reals"/g' \
58+
| sed -e 's/"micromega[.]Lra[.][^"]*"/"coq-stdlib-reals"/g' \
59+
| sed -e 's/"Numbers[.]R[.][^"]*"/"coq-stdlib-reals"/g' \
60+
| sed -e 's/"Relations[.]All[.][^"]*"/"coq-stdlib-relations"/g' \
61+
| sed -e 's/"ZArith[.]Ring[.][^"]*"/"coq-stdlib-ring"/g' \
62+
| sed -e 's/"setoid_ring[.]Z[.][^"]*"/"coq-stdlib-ring"/g' \
63+
| sed -e 's/"rtauto[.][^"]*"/"coq-stdlib-rtauto"/g' \
64+
| sed -e 's/"Sets[.][^"]*"/"coq-stdlib-sets"/g' \
65+
| sed -e 's/"Sorting[.][^"]*"/"coq-stdlib-sorting"/g' \
66+
| sed -e 's/"Streams[.][^"]*"/"coq-stdlib-streams"/g' \
67+
| sed -e 's/"Strings[.][^"]*"/"coq-stdlib-string"/g' \
68+
| sed -e 's/"Numbers[.]Strings[.][^"]*"/"coq-stdlib-string"/g' \
69+
| sed -e 's/"Structures[.]Def[.][^"]*"/"coq-stdlib-structures"/g' \
70+
| sed -e 's/"Unicode[.][^"]*"/"coq-stdlib-unicode"/g' \
71+
| sed -e 's/"Vectors[.][^"]*"/"coq-stdlib-vectors"/g' \
72+
| sed -e 's/"Wellfounded[.][^"]*"/"coq-stdlib-wellfounded"/g' \
73+
| sed -e 's/"Numbers[.]Natural[.]Binary[.][^"]*"/"coq-stdlib-zarith"/g' \
74+
| sed -e 's/"ZArith[.]All[.][^"]*"/"coq-stdlib-zarith"/g' \
75+
| sed -e 's/"Numbers[.]Integer[.]Binary[.][^"]*"/"coq-stdlib-zarith"/g' \
76+
| sed -e 's/"Numbers[.]Integer[.]NatPairs[.][^"]*"/"coq-stdlib-zarith"/g' \
77+
| sed -e 's/"Numbers[.]Z[.][^"]*"/"coq-stdlib-zarith"/g' \
78+
| sed -e 's/"btauto[.][^"]*"/"coq-stdlib-zarith"/g' \
79+
| sed -e 's/"Numbers[.]Integer[.]Abstract[.][^"]*"/"coq-stdlib-zarith-base"/g' \
80+
| sed -e 's/"ZArith[.]Base[.][^"]*"/"coq-stdlib-zarith-base"/g' \
81+
| tail -n +2 | head -n -1 \
82+
| sort | uniq \
83+
> depends_core
684

7-
# (echo "digraph stdlib_deps {";
8-
# echo "node [shape=ellipse, style=filled, color=lightblue];";
9-
# coqdep -R ../coq/theories Coq ../coq/theories | sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*v//p' | \
10-
# while read src dst; do
11-
# for d in $dst; do
12-
# d=${d#...coq.theories.}
13-
# echo "\"${src#...coq.theories.}\" -> \"${d%.vo}\" ;"
14-
# done
15-
# done;
16-
# echo "}") | tred >> depends
85+
(echo "digraph stdlib_deps {";
86+
echo "node [shape=ellipse, style=filled, color=lightblue];";
87+
awk -f dev/tools/depends-rm-loops.awk depends_core;
88+
echo "}") | tred > depends
89+
90+
rm -f depends_core

‎doc/stdlib/depends

+69
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,69 @@
1+
digraph stdlib_deps {
2+
node [color=lightblue,
3+
shape=ellipse,
4+
style=filled
5+
];
6+
"coq-stdlib" -> "coq-stdlib-compat";
7+
"coq-stdlib-compat" -> "coq-stdlib-fmaps-fsets-msets";
8+
"coq-stdlib-compat" -> "coq-stdlib-wellfounded";
9+
"coq-stdlib-compat" -> "coq-stdlib-derive";
10+
"coq-stdlib-compat" -> "coq-stdlib-rtauto";
11+
"coq-stdlib-compat" -> "coq-stdlib-extraction";
12+
"coq-stdlib-compat" -> "coq-stdlib-reals";
13+
"coq-stdlib-compat" -> "coq-stdlib-streams";
14+
"coq-stdlib-compat" -> "coq-stdlib-funind";
15+
"coq-stdlib-arith" -> "coq-stdlib-ring";
16+
"coq-stdlib-ring" -> "coq-stdlib-zarith-base";
17+
"coq-stdlib-ring" -> "coq-stdlib-list";
18+
"coq-stdlib-arith-base" -> "coq-stdlib-structures";
19+
"coq-stdlib-classes" -> "coq-stdlib-program";
20+
"coq-stdlib-classes" -> "coq-stdlib-relations";
21+
"coq-stdlib-structures" -> "coq-stdlib-bool";
22+
"coq-stdlib-bool" -> "coq-stdlib-classes";
23+
"coq-stdlib-program" -> "coq-stdlib-logic";
24+
"coq-stdlib-classical-logic" -> "coq-stdlib-arith";
25+
"coq-stdlib-lia" -> "coq-stdlib-arith";
26+
"coq-stdlib-extraction" -> "coq-stdlib-extraction-base";
27+
"coq-stdlib-extraction" -> "coq-stdlib-primitive-array";
28+
"coq-stdlib-extraction" -> "coq-stdlib-primitive-floats";
29+
"coq-stdlib-extraction" -> "coq-stdlib-primitive-string";
30+
"coq-stdlib-primitive-array" -> "coq-stdlib-primitive-int";
31+
"coq-stdlib-primitive-floats" -> "coq-stdlib-primitive-int";
32+
"coq-stdlib-primitive-int" -> "coq-stdlib-zarith";
33+
"coq-stdlib-primitive-int" -> "coq-stdlib-unicode";
34+
"coq-stdlib-string" -> "coq-stdlib-arith";
35+
"coq-stdlib-zarith" -> "coq-stdlib-lia";
36+
"coq-stdlib-field" -> "coq-stdlib-zarith";
37+
"coq-stdlib-field" -> "coq-stdlib-qarith-base";
38+
"coq-stdlib-qarith-base" -> "coq-stdlib-ring";
39+
"coq-stdlib-zarith-base" -> "coq-stdlib-narith";
40+
"coq-stdlib-fmaps-fsets-msets" -> "coq-stdlib-zarith";
41+
"coq-stdlib-fmaps-fsets-msets" -> "coq-stdlib-orders-ex";
42+
"coq-stdlib-orders-ex" -> "coq-stdlib-string";
43+
"coq-stdlib-orders-ex" -> "coq-stdlib-sorting";
44+
"coq-stdlib-sets" -> "coq-stdlib-classical-logic";
45+
"coq-stdlib-sorting" -> "coq-stdlib-lia";
46+
"coq-stdlib-sorting" -> "coq-stdlib-sets";
47+
"coq-stdlib-sorting" -> "coq-stdlib-vectors";
48+
"coq-stdlib-funind" -> "coq-stdlib-arith-base";
49+
"coq-stdlib-funind" -> "coq-stdlib-extraction-base";
50+
"coq-stdlib-list" -> "coq-stdlib-arith-base";
51+
"coq-stdlib-narith" -> "coq-stdlib-positive";
52+
"coq-stdlib-lqa" -> "coq-stdlib-field";
53+
"coq-stdlib-positive" -> "coq-stdlib-arith-base";
54+
"coq-stdlib-nsatz" -> "coq-stdlib-zarith";
55+
"coq-stdlib-nsatz" -> "coq-stdlib-qarith-base";
56+
"coq-stdlib-primitive-string" -> "coq-stdlib-primitive-int";
57+
"coq-stdlib-primitive-string" -> "coq-stdlib-orders-ex";
58+
"coq-stdlib-qarith" -> "coq-stdlib-field";
59+
"coq-stdlib-reals" -> "coq-stdlib-classical-logic";
60+
"coq-stdlib-reals" -> "coq-stdlib-lqa";
61+
"coq-stdlib-reals" -> "coq-stdlib-nsatz";
62+
"coq-stdlib-reals" -> "coq-stdlib-qarith";
63+
"coq-stdlib-reals" -> "coq-stdlib-vectors";
64+
"coq-stdlib-vectors" -> "coq-stdlib-list";
65+
"coq-stdlib-rtauto" -> "coq-stdlib-list";
66+
"coq-stdlib-rtauto" -> "coq-stdlib-positive";
67+
"coq-stdlib-streams" -> "coq-stdlib-logic";
68+
"coq-stdlib-wellfounded" -> "coq-stdlib-list";
69+
}

‎doc/stdlib/index-list.html.template

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@
55
It provides a set of modules directly available
66
through the <tt>Require Import</tt> command.</p>
77

8+
<img src="depends.png">
9+
810
<p>The standard library is composed of the following subdirectories:</p>
911

1012
<dl>

0 commit comments

Comments
 (0)