forked from MetaCoq/metacoq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMakefile
135 lines (109 loc) · 3.12 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
all: printconf template-coq pcuic safechecker erasure examples test-suite translations
-include Makefile.conf
ifeq '$(METACOQ_CONFIG)' 'local'
ifeq ($(shell which cygpath 2>/dev/null),)
OCAMLPATH := $(shell pwd)/template-coq/:$(OCAMLPATH)
else
OCAMLPATH := $(shell cygpath -m `pwd`)/template-coq/;$(OCAMLPATH)
endif
export OCAMLPATH
endif
.PHONY: printconf all template-coq pcuic erasure install html clean mrproper .merlin test-suite translations
printconf:
ifeq '$(METACOQ_CONFIG)' 'local'
@echo "Local configuration"
else
ifeq '$(METACOQ_CONFIG)' 'global'
@echo "Global configuration"
else
@echo "Run ./configure.sh first"
@exit 1
endif
endif
install: all translations
$(MAKE) -C template-coq install
$(MAKE) -C pcuic install
$(MAKE) -C safechecker install
$(MAKE) -C erasure install
$(MAKE) -C translations install
uninstall: all
$(MAKE) -C template-coq uninstall
$(MAKE) -C pcuic uninstall
$(MAKE) -C safechecker uninstall
$(MAKE) -C erasure uninstall
$(MAKE) -C translations uninstall
html: all
"coqdoc" --multi-index -toc -utf8 -html \
--with-header ./html/resources/header.html --with-footer ./html/resources/footer.html \
-R template-coq/theories MetaCoq.Template \
-R pcuic/theories MetaCoq.PCUIC \
-R safechecker/theories MetaCoq.SafeChecker \
-R erasure/theories MetaCoq.Erasure \
-R translations MetaCoq.Translations \
-R examples MetaCoq.Examples \
-d html */theories/*.v */theories/*/*.v translations/*.v examples/*.v
clean:
$(MAKE) -C template-coq clean
$(MAKE) -C pcuic clean
$(MAKE) -C safechecker clean
$(MAKE) -C erasure clean
$(MAKE) -C examples clean
$(MAKE) -C test-suite clean
$(MAKE) -C translations clean
vos:
$(MAKE) -C template-coq
$(MAKE) -C pcuic vos
$(MAKE) -C safechecker vos
$(MAKE) -C erasure vos
$(MAKE) -C translations vos
quick:
$(MAKE) -C template-coq
$(MAKE) -C pcuic quick
$(MAKE) -C safechecker quick
$(MAKE) -C erasure quick
$(MAKE) -C translations quick
mrproper:
$(MAKE) -C template-coq mrproper
$(MAKE) -C pcuic mrproper
$(MAKE) -C safechecker mrproper
$(MAKE) -C erasure mrproper
$(MAKE) -C examples mrproper
$(MAKE) -C test-suite mrproper
$(MAKE) -C translations mrproper
.merlin:
$(MAKE) -C template-coq .merlin
$(MAKE) -C pcuic .merlin
$(MAKE) -C safechecker .merlin
$(MAKE) -C erasure .merlin
template-coq:
$(MAKE) -C template-coq
pcuic: template-coq
$(MAKE) -C pcuic
safechecker: template-coq pcuic
$(MAKE) -C safechecker
erasure: template-coq safechecker pcuic
$(MAKE) -C erasure
examples: safechecker erasure
$(MAKE) -C examples
test-suite: template-coq safechecker erasure
$(MAKE) -C test-suite
translations: template-coq
$(MAKE) -C translations
cleanplugins:
$(MAKE) -C template-coq cleanplugin
$(MAKE) -C safechecker cleanplugin
$(MAKE) -C erasure cleanplugin
ci-local-noclean:
./configure.sh local
$(MAKE) all test-suite TIMED=pretty-timed
ci-local: ci-local-noclean
$(MAKE) clean
ci-quick:
./configure.sh --enable-quick
time $(MAKE) quick TIMED=pretty-timed
ci-opam:
# Use -v so that regular output is produced
opam install --with-test -v -y .
opam remove -y coq-metacoq coq-metacoq-template
checktodos:
sh checktodos.sh