/
Makefile
169 lines (115 loc) · 4.07 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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
default_target: all
.PHONY: update_all clone_all coqutil riscv-coq bedrock2_noex bedrock2_ex LiveVerif_noex LiveVerif_ex LiveVerifEx64 compiler_noex compiler_ex kami processor end2end all clean_coqutil clean_riscv-coq clean_bedrock2 clean_LiveVerif clean_LiveVerifEx64 clean_compiler clean_kami clean_processor clean_end2end clean_manglenames clean install_coqutil install_kami install_riscv-coq install_bedrock2 install_bedrock2_ex install_bedrock2_noex install_LiveVerif install_LiveVerifEx64 install_LiveVerif_ex install_LiveVerif_noex install_compiler install_processor install_end2end install
clone_all:
git submodule update --init --recursive
update_all:
git submodule update --recursive
REL_PATH_OF_THIS_MAKEFILE:=$(lastword $(MAKEFILE_LIST))
ABS_ROOT_DIR:=$(abspath $(dir $(REL_PATH_OF_THIS_MAKEFILE)))
# use cygpath -m because Coq on Windows cannot handle cygwin paths
ABS_ROOT_DIR:=$(shell cygpath -m '$(ABS_ROOT_DIR)' 2>/dev/null || echo '$(ABS_ROOT_DIR)')
DEPS_DIR ?= $(ABS_ROOT_DIR)/deps
export DEPS_DIR
ifeq ($(TRY_MANGLE_NAMES),1)
COQC := $(ABS_ROOT_DIR)/coqc-try-mangle-names.sh
export COQC
endif
EXTERNAL_DEPENDENCIES?=
EXTERNAL_COQUTIL?=
EXTERNAL_RISCV_COQ?=
EXTERNAL_KAMI?=
ifneq ($(EXTERNAL_DEPENDENCIES),1)
ifneq ($(EXTERNAL_COQUTIL),1)
bedrock2_noex: coqutil
riscv-coq: coqutil
install: install_coqutil
endif
ifneq ($(EXTERNAL_RISCV_COQ),1)
kami: riscv-coq
compiler_noex: riscv-coq
processor: riscv-coq
install: install_riscv-coq
endif
ifneq ($(EXTERNAL_KAMI),1)
processor: kami
install: install_kami
endif
compiler_noex: bedrock2_noex
compiler_ex: bedrock2_ex
end2end: compiler_ex bedrock2_ex processor
endif
clean_manglenames:
find . -type f -name '*.manglenames' -delete
coqutil:
$(MAKE) -C $(DEPS_DIR)/coqutil
clean_coqutil:
$(MAKE) -C $(DEPS_DIR)/coqutil clean
install_coqutil:
$(MAKE) -C $(DEPS_DIR)/coqutil install
kami:
$(MAKE) -C $(DEPS_DIR)/kami
clean_kami:
$(MAKE) -C $(DEPS_DIR)/kami clean
install_kami:
$(MAKE) -C $(DEPS_DIR)/kami install
riscv-coq:
$(MAKE) -C $(DEPS_DIR)/riscv-coq all
clean_riscv-coq:
$(MAKE) -C $(DEPS_DIR)/riscv-coq clean
install_riscv-coq:
$(MAKE) -C $(DEPS_DIR)/riscv-coq install
bedrock2_noex:
$(MAKE) -C $(ABS_ROOT_DIR)/bedrock2 noex
bedrock2_ex: bedrock2_noex
$(MAKE) -C $(ABS_ROOT_DIR)/bedrock2
clean_bedrock2:
$(MAKE) -C $(ABS_ROOT_DIR)/bedrock2 clean
install_bedrock2:
$(MAKE) -C $(ABS_ROOT_DIR)/bedrock2 install
install_bedrock2_noex:
$(MAKE) -C $(ABS_ROOT_DIR)/bedrock2 install_noex
install_bedrock2_ex:
$(MAKE) -C $(ABS_ROOT_DIR)/bedrock2 install_ex
LiveVerif_noex: bedrock2_noex
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif noex
LiveVerif_ex: LiveVerif_noex
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif
clean_LiveVerif:
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif clean
install_LiveVerif:
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif install
install_LiveVerif_noex:
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif install_noex
LiveVerifEx64: LiveVerif_noex
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerifEx64
clean_LiveVerifEx64:
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerifEx64 clean
install_LiveVerifEx64:
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerifEx64 install
install_LiveVerif_ex:
$(MAKE) -C $(ABS_ROOT_DIR)/LiveVerif install_ex
compiler_noex:
$(MAKE) -C $(ABS_ROOT_DIR)/compiler noex
compiler_ex: compiler_noex
$(MAKE) -C $(ABS_ROOT_DIR)/compiler
clean_compiler:
$(MAKE) -C $(ABS_ROOT_DIR)/compiler clean
install_compiler:
$(MAKE) -C $(ABS_ROOT_DIR)/compiler install
processor:
$(MAKE) -C $(ABS_ROOT_DIR)/processor
clean_processor:
$(MAKE) -C $(ABS_ROOT_DIR)/processor clean
install_processor:
$(MAKE) -C $(ABS_ROOT_DIR)/processor install
end2end:
$(MAKE) -C $(ABS_ROOT_DIR)/end2end
clean_end2end:
$(MAKE) -C $(ABS_ROOT_DIR)/end2end clean
install_end2end:
$(MAKE) -C $(ABS_ROOT_DIR)/end2end install
all: bedrock2_ex LiveVerif_ex LiveVerifEx64 compiler_ex processor end2end
clean: clean_bedrock2 clean_LiveVerif clean_LiveVerifEx64 clean_compiler clean_processor clean_end2end
clean_deps: clean_coqutil clean_kami clean_riscv-coq
clean_all: clean_deps clean
install: install_bedrock2 install_LiveVerif install_LiveVerifEx64 install_compiler install_processor install_end2end