-
Notifications
You must be signed in to change notification settings - Fork 86
/
build-sequence
198 lines (174 loc) · 4.56 KB
/
build-sequence
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
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
## The regression test runs through this list of directories.
# download the latest cake binary
developers
developers/bin
misc
# build many things in parallel at the start
compiler/proofs
compiler/bootstrap/translation
# semantics and metatheory
semantics/ffi
semantics
semantics/proofs
semantics/alt_semantics
semantics/alt_semantics/proofs
# translator
basis/pure
translator
# characteristic formulae
compiler/parsing
characteristic
# monadic translator
translator/monadic
translator/monadic/monad_base
# basis library
basis
# compiler
compiler
compiler/inference
compiler/backend/reg_alloc
compiler/backend/gc
compiler/backend
compiler/encoders/asm
compiler/encoders/x64
compiler/encoders/arm7
compiler/encoders/arm8
compiler/encoders/arm8_asl
compiler/encoders/mips
compiler/encoders/riscv
compiler/encoders/ag32
compiler/encoders/tests
compiler/encoders/monadic_enc
compiler/backend/x64
compiler/backend/arm7
compiler/backend/arm8
compiler/backend/mips
compiler/backend/riscv
compiler/backend/ag32
compiler/backend/pattern_matching
compiler/parsing/ocaml
compiler/printing
# compiler verification
compiler/parsing/proofs
compiler/inference/proofs
compiler/backend/semantics
compiler/backend/reg_alloc/proofs
compiler/backend/proofs
compiler/backend/serialiser
compiler/encoders/x64/proofs
compiler/encoders/arm7/proofs
compiler/encoders/arm8/proofs
compiler/encoders/arm8_asl/proofs
compiler/encoders/mips/proofs
compiler/encoders/riscv/proofs
compiler/encoders/ag32/proofs
compiler/backend/x64/proofs
compiler/backend/arm7/proofs
compiler/backend/arm8/proofs
compiler/backend/arm8_asl
compiler/backend/mips/proofs
compiler/backend/riscv/proofs
compiler/backend/ag32/proofs
compiler/backend/cv_compute
cv_translator
# candle
candle
candle/set-theory
candle/syntax-lib
candle/standard
candle/standard/syntax
candle/standard/semantics
candle/standard/monadic
candle/standard/ml_kernel
candle/standard/ml_kernel/lisp
candle/overloading
candle/overloading/syntax
candle/overloading/semantics
candle/overloading/monadic
candle/overloading/ml_kernel
candle/overloading/ml_checker
candle/prover
candle/prover/compute
# pancake
pancake
pancake/semantics
pancake/parser
pancake/proofs
pancake/ta_progs
# dafny compiler
compiler/dafny
compiler/dafny/translation
compiler/dafny/compilation
compiler/dafny/semantics
# examples and tests
characteristic/examples
tutorial/solutions
translator/monadic/examples
examples
examples/compilation
examples/compilation/x64
examples/compilation/x64/proofs
examples/compilation/ag32
examples/compilation/ag32/proofs
examples/lpr_checker
examples/lpr_checker/array
examples/lpr_checker/array/compilation
examples/lpr_checker/array/compilation/proofs
examples/lpr_checker/array/compilation/proofsARM8
.
examples/xlrup_checker
examples/xlrup_checker/array
examples/xlrup_checker/array/compilation
examples/xlrup_checker/array/compilation/proofs
examples/pseudo_bool
examples/pseudo_bool/cnf_encoding
examples/pseudo_bool/graph_encoding
examples/pseudo_bool/array
examples/pseudo_bool/array/compilation
examples/pseudo_bool/array/compilation/proofs
examples/pseudo_bool/array/compilation/proofsARM8
examples/opentheory
examples/opentheory/compilation
examples/opentheory/compilation/proofs
examples/opentheory/compilation/ag32
examples/opentheory/compilation/ag32/proofs
examples/sat_encodings
examples/sat_encodings/demo
examples/sat_encodings/case_studies
examples/sat_encodings/translation
examples/sat_encodings/translation/compilation
examples/deflate
examples/deflate/translation
examples/deflate/translation/compilation
examples/vipr
examples/vipr/compilation
translator/okasaki-examples
translator/other-examples
translator/other-examples/auxiliary
compiler/parsing/tests
compiler/inference/tests
compiler/printing/test
# Floating-Point optimizer
icing/flover
icing/flover/Infra
icing/flover/semantics
icing/
icing/examples
# compiler translation
compiler/repl
# compiler sexpr bootstrap
unverified/sexpr-bootstrap/x64/64:cake-unverified-x64-64.tar.gz
unverified/sexpr-bootstrap/x64/32:cake-unverified-x64-32.tar.gz
# build benchmarks and report (must come after sexp bootstrap)
compiler/benchmarks
compiler/benchmarks/cakeml_benchmarks/cakeml
compiler/benchmarks/mlton_benchmarks/cakeml
# compiler HOL bootstrap
compiler/bootstrap/compilation/x64/64:cake-x64-64.tar.gz
compiler/bootstrap/compilation/x64/64/proofs
compiler/bootstrap/compilation/x64/32:cake-x64-32.tar.gz
compiler/bootstrap/compilation/x64/32/proofs
compiler/bootstrap/compilation/arm8/64:cake-arm8-64.tar.gz
compiler/bootstrap/compilation/arm8/64/proofs
compiler/bootstrap/compilation/ag32/32
compiler/bootstrap/compilation/ag32/32/proofs