-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathMakefile
98 lines (84 loc) · 3 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
COQMODULE := compcomp
# COQTHEORIES := $(wildcard */*.v) #*/*.v
COQTHEORIES := $(shell find . -iname '*.v')
.PHONY: all proof proof-quick graph
all:
$(MAKE) proof
graph:
sh make_graph.sh
### Quick
# proof-quick: Makefile.coq $(COQTHEORIES)
# $(MAKE) -f Makefile.coq quick
proof-quick: Makefile.coq $(COQTHEORIES)
$(MAKE) -f Makefile.coq $(patsubst %.v,%.vio,$(COQTHEORIES))
proof: Makefile.coq $(COQTHEORIES)
$(MAKE) -f Makefile.coq $(patsubst %.v,%.vo,$(COQTHEORIES))
Makefile.coq: Makefile $(COQTHEORIES)
(echo "-R ../lib compcert.lib"; \
echo "-R ../common compcert.common"; \
echo "-R ../x86 compcert.x86"; \
echo "-R ../x86_64 compcert.x86_64"; \
echo "-R ../backend compcert.backend"; \
echo "-R ../cfrontend compcert.cfrontend"; \
echo "-R ../driver compcert.driver"; \
echo "-R ../flocq compcert.flocq"; \
echo "-R ../exportclight compcert.exportclight"; \
echo "-R ../cparser compcert.cparser"; \
echo "-R ../demo compcert.demo"; \
\
echo "-R lib $(COQMODULE)"; \
echo "-R common $(COQMODULE)"; \
echo "-R x86 $(COQMODULE)"; \
echo "-R x86_64 $(COQMODULE)"; \
echo "-R backend $(COQMODULE)"; \
echo "-R cfrontend $(COQMODULE)"; \
echo "-R driver $(COQMODULE)"; \
echo "-R bound $(COQMODULE)"; \
\
echo "-R compose $(COQMODULE)"; \
echo "-R proof $(COQMODULE)"; \
echo "-R demo $(COQMODULE)"; \
echo "-R selfsim $(COQMODULE)"; \
echo $(COQTHEORIES)) > _CoqProject
coq_makefile -f _CoqProject -o Makefile.coq
### All
# NORMAL_BULID_DIR=.normal_build
# all: Makefile.coq-rsync
# $(MAKE) -f Makefile.coq-rsync all
# all-rsync:
# rsync -av --copy-links --delete \
# --exclude "$(NORMAL_BULID_DIR)" --exclude '.git/*' \
# --include '*/' \
# --filter=':- .gitignore' \
# './' "$(NORMAL_BULID_DIR)/"
# $(MAKE) -C $(NORMAL_BULID_DIR) all
# rsync -av \
# --include '*/' --include "ccomp" --include "compcert.ini" --include "*.ml" --include "*.mli" \
# --exclude '*' \
# "$(NORMAL_BULID_DIR)/" './'
# Makefile.coq-rsync: Makefile $(COQTHEORIES)
# (echo "-R ../../lib compcert.lib"; \
# echo "-R ../../common compcert.common"; \
# echo "-R ../../x86 compcert.x86"; \
# echo "-R ../../x86_64 compcert.x86_64"; \
# echo "-R ../../backend compcert.backend"; \
# echo "-R ../../cfrontend compcert.cfrontend"; \
# echo "-R ../../driver compcert.driver"; \
# echo "-R ../../flocq compcert.flocq"; \
# echo "-R ../../exportclight compcert.exportclight"; \
# echo "-R ../../cparser compcert.cparser"; \
# echo $(COQTHEORIES)) > _CoqProject
# coq_makefile -f _CoqProject -o Makefile.coq-rsync
###
# %.vo: Makefile.coq
# $(MAKE) -f Makefile.coq "$@"
# %.vio: Makefile.coq
# $(MAKE) -f Makefile.coq "$@"
clean:
$(MAKE) -f Makefile.coq clean || true
find . -name "*.vio" -type f -delete
find . -name "*.v.d" -type f -delete
find . -name "*.vo" -type f -delete
find . -name "*.glob" -type f -delete
# $(MAKE) -f Makefile.coq-rsync clean || true
rm -f _CoqProject Makefile.coq Makefile.coq.conf #Makefile.coq-rsync Makefile.coq-rsync.conf