forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
build-sequence
171 lines (149 loc) · 3.93 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
## The regression test runs through this list of directories.
# download the latest cake binary
developers
developers/bin
# 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
# basis library
basis
# 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/backend/x64
compiler/backend/arm7
compiler/backend/arm8
compiler/backend/mips
compiler/backend/riscv
compiler/backend/ag32
# 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/set-theory
candle/syntax-lib
candle/standard/syntax
candle/standard/semantics
candle/standard/monadic
candle/standard/ml_kernel
candle/overloading/syntax
candle/overloading/semantics
candle/overloading/monadic
candle/overloading/ml_kernel
candle/overloading/ml_checker
candle/prover
# pancake
pancake
pancake/ffi
pancake/semantics
pancake/parser
pancake/proofs
# examples and tests
characteristic/examples
tutorial/solutions
translator/monadic/examples
examples
examples/compilation/x64
examples/compilation/x64/proofs
examples/compilation/ag32
examples/compilation/ag32/proofs
examples/compilation/to_word
# examples/cost
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
examples/opentheory/compilation
examples/opentheory/compilation/proofs
examples/opentheory/compilation/ag32
examples/opentheory/compilation/ag32/proofs
examples/sat_encodings
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
compiler/parsing/tests
compiler/inference/tests
compiler/printing/test
# Floating-Point optimizer
icing/flover
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 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/ag32/32
compiler/bootstrap/compilation/ag32/32/proofs