-
Notifications
You must be signed in to change notification settings - Fork 2
/
Makefile
77 lines (62 loc) · 1.46 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
DRIVER=OeufDriver.native
all: proof driver test
proof: Makefile.coq
ifeq ($(NPAR),)
$(MAKE) -j2 -f Makefile.coq
else
$(MAKE) -j$(NPAR) -f Makefile.coq
endif
Makefile.coq: _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq
plugin:
make -C plugin
sanitize:
_build/sanitize.sh || true
driver: compcert.ini sanitize
ocamlbuild \
-cflag -annot \
-no-hygiene \
-use-menhir -pkg menhirLib \
-yaccflag --table \
-lib str \
-lib unix \
-I src \
-I extraction \
-I compcert/driver \
-I compcert/cfrontend \
-I compcert/cparser \
-I compcert/ia32 \
-I compcert/lib \
-I compcert/common \
-I compcert/debug \
-I compcert/backend \
$(DRIVER)
rm -f $(DRIVER)
cp _build/src/$(DRIVER) $(DRIVER)
compcert.ini: compcert/Makefile.config
$(MAKE) -C compcert compcert.ini
rm -f compcert.ini
cp compcert/compcert.ini compcert.ini
test:
./test.sh
demo :
./compile_demo.sh
clean: Makefile.coq
$(MAKE) -f Makefile.coq clean
rm -rf Makefile.coq _build/
rm -f compcert.ini $(DRIVER)
rm -f extraction/*.ml extraction/*.mli
COMPCERTCONFIG=$(shell \
[ "$$(uname)" = "Darwin" ] && \
echo "ia32-macosx" || \
echo "ia32-linux" )
COMPCERTPAR=$(shell \
[ "$$(hostname -s)" = "warfa" ] && \
echo "-j6" || \
echo "" )
compcert:
cd compcert && ./configure $(COMPCERTCONFIG)
$(MAKE) $(COMPCERTPAR) -C compcert
cleaner: clean
$(MAKE) -C compcert clean
.PHONY: all proof driver plugin sanitize test clean compcert cleaner