forked from AU-COBRA/ConCert
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
90 lines (74 loc) · 2.22 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
all: utils execution embedding extraction
.PHONY: all
utils:
+make -C utils
.PHONY: utils
execution: utils
+make -C execution
.PHONY: execution
embedding: utils execution
+make -C embedding
.PHONY: embedding
extraction: utils execution
+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 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 extraction install
.PHONY: install
uninstall: all
+make -C utils uninstall
+make -C execution uninstall
+make -C embedding 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
html: all
rm -rf docs
mkdir docs
coqdoc --html --interpolate --parse-comments \
--with-header extra/header.html --with-footer extra/footer.html \
--toc \
-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 extraction/theories ConCert.Extraction \
-R extraction/plugin/theories ConCert.Extraction \
-R extraction/tests ConCert.Extraction.Tests \
-R examples ConCert.Examples \
-d docs `find . -type f \( -wholename "*theories/*" -o -wholename "*examples/*" -o -wholename "*extraction/*" -o -wholename "*test/*" \) -name "*.v"`
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