-
Notifications
You must be signed in to change notification settings - Fork 43
/
Makefile
85 lines (60 loc) · 2.09 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
# One of these two files will have been generated
.PHONY: all default makefiles clean-makefiles
all: Makefile.coq
$(MAKE) -f Makefile.coq
test -f Makefile.hott && $(MAKE) -f Makefile.hott || true
install: Makefile.coq
$(MAKE) -f Makefile.coq install
test -f Makefile.hott && $(MAKE) -f Makefile.hott install || true
makefiles: test-suite/Makefile examples/Makefile
clean-makefiles:
rm -f test-suite/Makefile examples/Makefile
test-suite/Makefile: test-suite/_CoqProject
cd test-suite && coq_makefile -f _CoqProject -o Makefile
examples/Makefile: examples/_CoqProject
cd examples && coq_makefile -f _CoqProject -o Makefile
pre-all:: makefiles
# Ensure we make the bytecode version as well
post-all:: bytefiles
clean-examples: makefiles
cd examples && $(MAKE) clean
clean-test-suite: makefiles
cd test-suite && $(MAKE) clean
test-suite: makefiles all
cd test-suite && $(MAKE)
.PHONY: test-suite
examples: examples/Makefile all
cd examples && $(MAKE)
.PHONY: examples
clean: clean-makefiles makefiles
$(MAKE) -f Makefile.coq clean
test -f Makefile.hott && make -f Makefile.hott clean || true
$(MAKE) clean-examples clean-test-suite
siteexamples: examples/*.glob
sh siteexamples.sh
doc: html
mkdir -p html/api && ocamldoc -html -d html/api \
`ocamlfind query -r coq-core.lib coq-core.kernel coq-core.tactics coq-core.proofs \
coq-core.toplevel coq-core.ltac coq-core.plugins.extraction -i-format` \
-I src src/*.ml
toplevel: src/equations_plugin.cma bytefiles
"$(OCAMLFIND)" ocamlc -linkpkg -linkall -g $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-package coq-core.toplevel,coq-core.plugins.extraction \
$< $(COQLIB)/toplevel/coqtop_bin.ml -o coqtop_equations
dune:-
dune build
ci-dune:
opam install -j 2 -y coq-hott.dev
dune build
ci-hott:
opam install -j 2 -y coq-hott.dev
test -f Makefile.hott && $(MAKE) -f Makefile.hott all
$(MAKE) -f Makefile.hott install
$(MAKE) -f Makefile.hott uninstall
ci-local:
$(MAKE) -f Makefile.coq all
$(MAKE) test-suite examples
$(MAKE) -f Makefile.coq install
$(MAKE) -f Makefile.coq uninstall
ci: ci-local
.PHONY: ci-dune ci-hott ci-local