forked from AU-COBRA/ConCert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
159 lines (136 loc) · 6.1 KB
/
Makefile
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
all: utils execution embedding typed-extraction extraction
.PHONY: all
utils:
+make -C utils
.PHONY: utils
execution: utils
+make -C execution
.PHONY: execution
embedding: utils execution
+make -C embedding
.PHONY: embedding
typed-extraction:
+make -C typed-extraction
.PHONY: typed-extraction
extraction: utils execution typed-extraction
+make -C extraction
.PHONY: extraction
examples: utils execution embedding extraction
+make -C examples
.PHONY: examples
clean:
+make -C utils clean
+make -C execution clean
+make -C embedding clean
+make -C typed-extraction clean
+make -C extraction clean
+make -C examples clean
rm -rf docs
.PHONY: clean
install: all
+make -C utils install
+make -C execution install
+make -C embedding install
+make -C typed-extraction install
+make -C extraction install
.PHONY: install
uninstall: all
+make -C utils uninstall
+make -C execution uninstall
+make -C embedding uninstall
+make -C typed-extraction uninstall
+make -C extraction uninstall
.PHONY: uninstall
test-extraction:
+make -C extraction test-extraction
.PHONY: test-extraction
process-extraction-examples:
+make -C extraction process-extraction-examples
.PHONY: process-extraction-examples
clean-extraction-out-files:
+make -C extraction clean-extraction-out-files
.PHONY: clean-extraction-out-files
clean-compiled-extraction:
+make -C extraction clean-compiled-extraction
.PHONY: clean-compiled-extraction
clean-extraction-examples:
+make -C extraction clean-extraction-examples
.PHONY: clean-extraction-examples
dependency-graphs: utils execution embedding extraction examples
+make -C utils dep-graphs-svg
+make -C execution dep-graphs-svg
+make -C embedding dep-graphs-svg
+make -C extraction dep-graphs-svg
+make -C examples dep-graphs-svg
file-dependency-graph:
@echo "Generate dot files"
@coqdep -dumpgraph utils-file-dep.dot -f utils/_CoqProject >/dev/null 2>&1
@coqdep -dumpgraph execution-file-dep.dot -f execution/_CoqProject >/dev/null 2>&1
@coqdep -dumpgraph embedding-file-dep.dot -f embedding/_CoqProject >/dev/null 2>&1
@coqdep -dumpgraph extraction-file-dep.dot -f extraction/_CoqProject >/dev/null 2>&1
@coqdep -dumpgraph examples-file-dep.dot -f examples/_CoqProject >/dev/null 2>&1
@echo "Add node colors"
@sed -i.tmp 's/"\]/", style=filled, fillcolor="#FFC09F"\]/' utils-file-dep.dot ; rm -f utils-file-dep.dot.tmp
@sed -i.tmp 's/"\]/", style=filled, fillcolor="#FFEE93"\]/' execution-file-dep.dot ; rm -f execution-file-dep.dot.tmp
@sed -i.tmp 's/"\]/", style=filled, fillcolor="#FCF5C7"\]/' embedding-file-dep.dot ; rm -f embedding-file-dep.dot.tmp
@sed -i.tmp 's/"\]/", style=filled, fillcolor="#A0CED9"\]/' extraction-file-dep.dot ; rm -f extraction-file-dep.dot.tmp
@sed -i.tmp 's/"\]/", style=filled, fillcolor="#ADF7B6"\]/' examples-file-dep.dot ; rm -f examples-file-dep.dot.tmp
@echo "Fix paths"
@sed -i.tmp 's/"[^"^\/]*\/\.\.\//"/g' utils-file-dep.dot ; rm -f utils-file-dep.dot.tmp
@sed -i.tmp 's/"[^"^\/]*\/\.\.\//"/g' execution-file-dep.dot ; rm -f execution-file-dep.dot.tmp
@sed -i.tmp 's/"[^"^\/]*\/\.\.\//"/g' embedding-file-dep.dot ; rm -f embedding-file-dep.dot.tmp
@sed -i.tmp 's/"[^"^\/]*\/\.\.\//"/g' extraction-file-dep.dot ; rm -f extraction-file-dep.dot.tmp
@sed -i.tmp 's/"[^"^\/]*\/\.\.\//"/g' examples-file-dep.dot ; rm -f examples-file-dep.dot.tmp
@echo "Merge files"
@dep_utils=$$(cat utils-file-dep.dot | cut -d "{" -f2 | cut -d "}" -f1); \
dep_execution=$$(cat execution-file-dep.dot | cut -d "{" -f2 | cut -d "}" -f1); \
dep_embedding=$$(cat embedding-file-dep.dot | cut -d "{" -f2 | cut -d "}" -f1); \
dep_extraction=$$(cat extraction-file-dep.dot | cut -d "{" -f2 | cut -d "}" -f1); \
dep_examples=$$(cat examples-file-dep.dot | cut -d "{" -f2 | cut -d "}" -f1); \
rm -f utils-file-dep.dot execution-file-dep.dot embedding-file-dep.dot extraction-file-dep.dot examples-file-dep.dot; \
echo "digraph dependencies {$${dep_utils}$${dep_execution}$${dep_embedding}$${dep_extraction}$${dep_examples}\n}" > file-dep.dot
@echo "Remove duplicates"
@awk '!seen[$$0]++' file-dep.dot > file-dep.tmp; mv file-dep.tmp file-dep.dot
@echo "Convert to SVG"
@dot -Tsvg -o file-dep.svg file-dep.dot ; rm -f file-dep.dot
html: all
rm -rf docs
mkdir docs
coqdoc --html --interpolate --parse-comments \
--with-header extra/header.html --with-footer extra/footer.html \
--toc \
--external https://plv.mpi-sws.org/coqdoc/stdpp stdpp \
--external https://metacoq.github.io/html MetaCoq \
--external https://coq-community.org/coq-ext-lib/v0.11.7 ExtLib \
-R utils/theories ConCert.Utils \
-R execution/theories ConCert.Execution \
-R execution/test ConCert.Execution.Test \
-R embedding/theories ConCert.Embedding \
-R embedding/extraction ConCert.Embedding.Extraction \
-R embedding/examples ConCert.Embedding.Examples \
-R typed-extraction/theories MetaCoq.TypedExtraction \
-R typed-extraction/tests MetaCoq.TypedExtraction.Tests \
-R extraction/theories ConCert.Extraction \
-R extraction/plugin/theories ConCert.Extraction \
-R extraction/tests ConCert.Extraction.Tests \
-R examples/eip20 ConCert.Examples.EIP20 \
-R examples/bat ConCert.Examples.BAT \
-R examples/fa2 ConCert.Examples.FA2 \
-R examples/fa1_2 ConCert.Examples.FA1_2 \
-R examples/dexter ConCert.Examples.Dexter \
-R examples/dexter2 ConCert.Examples.Dexter2 \
-R examples/exchangeBuggy ConCert.Examples.ExchangeBuggy \
-R examples/iTokenBuggy ConCert.Examples.iTokenBuggy \
-R examples/cis1 ConCert.Examples.CIS1 \
-R examples/stackInterpreter ConCert.Examples.StackInterpreter \
-R examples/congress ConCert.Examples.Congress \
-R examples/escrow ConCert.Examples.Escrow \
-R examples/boardroomVoting ConCert.Examples.BoardroomVoting \
-R examples/counter ConCert.Examples.Counter \
-R examples/crowdfunding ConCert.Examples.Crowdfunding \
-d docs `find . -type f \( -wholename "*theories/*" -o -wholename "*examples/*" -o -wholename "*extraction/*" -o -wholename "*test/*" \) -name "*.v" ! -name "AllTests.v" ! -wholename "./_opam/*"`
cp extra/resources/coqdocjs/*.js docs
cp extra/resources/coqdocjs/*.css docs
cp extra/resources/toc/*.js docs
cp extra/resources/toc/*.css docs
.PHONY: html