OverviewCakeML:d799d23caefc9c1971792072350c9dd7c1779c53
Update COPYING
HOL:02777f989ba557fe906094a01dd6a18ec7fb2e94
emacs-mode: fix indentation bug identified in c3e0ecb4ce1
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
Claimed job
Building HOL
Starting developers
Finished developers 4s 93MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 236MB
Starting semantics
Finished semantics 1m34s 980MB
Starting semantics/proofs
Finished semantics/proofs 3m36s 868MB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 317MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m17s 776MB
Starting basis/pure
Finished basis/pure 3m11s 868MB
Starting translator
Finished translator 2m48s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m14s 2GB
Starting characteristic
Finished characteristic 6m15s 2GB
Starting translator/monadic
Finished translator/monadic 1m42s 1GB
Starting basis
Finished basis 46m59s 11GB
Starting compiler/inference
Finished compiler/inference 1m13s 980MB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m08s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m48s 2GB
Starting compiler/backend
Finished compiler/backend 5m04s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 22s 660MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m06s 991MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m11s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 39s 965MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m37s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m49s 899MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 594MB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 21s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 19s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 20s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m13s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m54s 860MB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m36s 966MB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 33m23s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m47s 988MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 58m44s 13GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 10m30s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 14m13s 6GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 7m07s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 10m52s 1GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 9m41s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m49s 719MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 21s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 23s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 20s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 21s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 22s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 13m40s 2GB
Starting compiler/proofs
Finished compiler/proofs 1m57s 3GB
Starting candle/set-theory
Finished candle/set-theory 29s 883MB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 705MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m55s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m47s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m50s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m54s 5GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m22s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 13m06s 2GB
Starting characteristic/examples
Finished characteristic/examples 1m19s 2GB
Starting tutorial/solutions
Finished tutorial/solutions 15m52s 8GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m21s 2GB
Starting examples
Finished examples 9m00s 4GB
Starting examples/compilation/x64
FAILED: examples/compilation/x64
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
/home/cake/oven/regression/cakeml-1483/developers/readme_gen catCompileScript.sml diffCompileScript.sml echoCompileScript.sml grepCompileScript.sml helloCompileScript.sml helloErrCompileScript.sml iocatCompileScript.sml patchCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "catCompile">>
to_flat eval: runtime: 6.7s, gctime: 0.35608s, systime: 0.20071s.
to_flat real: 6.9s
to_flat size: 72691
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.37713s, gctime: 0.06009s, systime: 0.01796s.
to_clos real: 0.39575s
to_clos size: 42660
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 4.4s, gctime: 0.14563s, systime: 0.01899s.
to_bvl real: 4.5s
to_bvl size: 75939
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 36.0s, gctime: 0.21992s, systime: 0.02097s.
to_bvi real: 36.1s
to_bvi size: 80359
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 10.6s, gctime: 0.44684s, systime: 0.03798s.
to_data real: 10.7s
to_data size: 128946
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 14.9s, gctime: 0.33971s, systime: 0.02799s.
data_to_word real: 14.9s
data_to_word size: 322925
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 1m09s, gctime: 2.3s, systime: 0.25786s.
inst,ssa,two-reg (par) real: 31.5s
inst,ssa,two-reg (par) size: 1286204
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 7.9s, gctime: 0.89199s, systime: 0.09379s.
get_clash (par) real: 3.8s
get_clash (par) size: 1996027
external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75 coalesceable: 61 coalesced: 53
1 moves: 24 coalesceable: 22 coalesced: 20
2 moves: 90 coalesceable: 68 coalesced: 53
3 moves: 25 coalesceable: 19 coalesced: 17
4 moves: 16 coalesceable: 15 coalesced: 12
5 moves: 148 coalesceable: 116 coalesced: 110
6 moves: 7 coalesceable: 7 coalesced: 7
7 moves: 7 coalesceable: 7 coalesced: 7
8 moves: 7 coalesceable: 7 coalesced: 7
9 moves: 7 coalesceable: 7 coalesced: 7
10 moves: 7 coalesceable: 7 coalesced: 7
11 moves: 19 coalesceable: 17 coalesced: 12
12 moves: 47 coalesceable: 41 coalesced: 37
13 moves: 31 coalesceable: 20 coalesced: 17
14 moves: 58 coalesceable: 48 coalesced: 42
15 moves: 0 coalesceable: 0 coalesced: 0
16 moves: 10 coalesceable: 8 coalesced: 5
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 21 coalesceable: 20 coalesced: 20
19 moves: 22 coalesceable: 21 coalesced: 20
20 moves: 19 coalesceable: 15 coalesced: 15
21 moves: 35 coalesceable: 29 coalesced: 25
22 moves: 40 coalesceable: 34 coalesced: 33
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 19 coalesceable: 17 coalesced: 15
25 moves: 42 coalesceable: 38 coalesced: 29
26 moves: 20 coalesceable: 20 coalesced: 14
27 moves: 20 coalesceable: 20 coalesced: 10
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 316 coalesceable: 269 coalesced: 269
31 moves: 26 coalesceable: 23 coalesced: 23
32 moves: 24 coalesceable: 23 coalesced: 23
33 moves: 16 coalesceable: 15 coalesced: 15
34 moves: 22 coalesceable: 19 coalesced: 19
35 moves: 90 coalesceable: 81 coalesced: 81
36 moves: 85 coalesceable: 82 coalesced: 82
37 moves: 65 coalesceable: 62 coalesced: 62
38 moves: 88 coalesceable: 85 coalesced: 85
39 moves: 29 coalesceable: 26 coalesced: 26
40 moves: 48 coalesceable: 45 coalesced: 45
41 moves: 7 coalesceable: 6 coalesced: 6
42 moves: 22 coalesceable: 19 coalesced: 19
43 moves: 12 coalesceable: 11 coalesced: 11
44 moves: 21 coalesceable: 18 coalesced: 18
45 moves: 51 coalesceable: 48 coalesced: 48
46 moves: 8 coalesceable: 7 coalesced: 7
47 moves: 11 coalesceable: 10 coalesced: 10
48 moves: 22 coalesceable: 19 coalesced: 19
49 moves: 26 coalesceable: 23 coalesced: 23
50 moves: 15 coalesceable: 14 coalesced: 14
51 moves: 20 coalesceable: 17 coalesced: 17
52 moves: 24 coalesceable: 21 coalesced: 21
53 moves: 190 coalesceable: 117 coalesced: 103
54 moves: 92 coalesceable: 65 coalesced: 51
55 moves: 41 coalesceable: 26 coalesced: 25
56 moves: 35 coalesceable: 26 coalesced: 21
57 moves: 56 coalesceable: 42 coalesced: 36
58 moves: 71 coalesceable: 46 coalesced: 40
59 moves: 48 coalesceable: 37 coalesced: 32
60 moves: 71 coalesceable: 46 coalesced: 38
61 moves: 927 coalesceable: 603 coalesced: 410
62 moves: 1088 coalesceable: 687 coalesced: 404
63 moves: 1169 coalesceable: 725 coalesced: 434
64 moves: 1254 coalesceable: 765 coalesced: 434
65 moves: 1343 coalesceable: 807 coalesced: 407
66 moves: 1436 coalesceable: 851 coalesced: 420
67 moves: 1533 coalesceable: 897 coalesced: 459
68 moves: 1634 coalesceable: 943 coalesced: 482
69 moves: 1739 coalesceable: 989 coalesced: 504
70 moves: 1848 coalesceable: 1035 coalesced: 506
71 moves: 17 coalesceable: 15 coalesced: 15
72 moves: 19 coalesceable: 17 coalesced: 17
73 moves: 21 coalesceable: 18 coalesced: 17
74 moves: 21 coalesceable: 19 coalesced: 19
75 moves: 23 coalesceable: 20 coalesced: 19
76 moves: 25 coalesceable: 21 coalesced: 20
77 moves: 23 coalesceable: 21 coalesced: 21
78 moves: 25 coalesceable: 22 coalesced: 21
79 moves: 27 coalesceable: 23 coalesced: 22
80 moves: 29 coalesceable: 24 coalesced: 23
81 moves: 25 coalesceable: 23 coalesced: 19
82 moves: 27 coalesceable: 24 coalesced: 20
83 moves: 29 coalesceable: 25 coalesced: 21
84 moves: 31 coalesceable: 26 coalesced: 22
85 moves: 33 coalesceable: 27 coalesced: 23
86 moves: 27 coalesceable: 24 coalesced: 21
87 moves: 29 coalesceable: 25 coalesced: 22
88 moves: 31 coalesceable: 26 coalesced: 23
89 moves: 33 coalesceable: 27 coalesced: 24
90 moves: 35 coalesceable: 28 coalesced: 25
91 moves: 37 coalesceable: 29 coalesced: 26
92 moves: 29 coalesceable: 25 coalesced: 16
93 moves: 31 coalesceable: 26 coalesced: 18
94 moves: 33 coalesceable: 27 coalesced: 23
95 moves: 35 coalesceable: 28 coalesced: 21
96 moves: 37 coalesceable: 29 coalesced: 22
97 moves: 39 coalesceable: 30 coalesced: 23
98 moves: 41 coalesceable: 31 coalesced: 24
99 moves: 31 coalesceable: 25 coalesced: 12
100 moves: 33 coalesceable: 27 coalesced: 9
101 moves: 35 coalesceable: 28 coalesced: 16
102 moves: 37 coalesceable: 29 coalesced: 23
103 moves: 39 coalesceable: 30 coalesced: 23
104 moves: 41 coalesceable: 31 coalesced: 21
105 moves: 43 coalesceable: 32 coalesced: 22
106 moves: 45 coalesceable: 33 coalesced: 25
107 moves: 33 coalesceable: 25 coalesced: 14
108 moves: 35 coalesceable: 27 coalesced: 10
109 moves: 37 coalesceable: 29 coalesced: 11
110 moves: 39 coalesceable: 30 coalesced: 14
111 moves: 41 coalesceable: 31 coalesced: 21
112 moves: 43 coalesceable: 32 coalesced: 23
113 moves: 45 coalesceable: 33 coalesced: 23
114 moves: 47 coalesceable: 34 coalesced: 23
115 moves: 49 coalesceable: 35 coalesced: 25
116 moves: 62 coalesceable: 11 coalesced: 7
117 moves: 940 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 11 coalesced: 11
119 moves: 17 coalesceable: 11 coalesced: 11
120 moves: 17 coalesceable: 11 coalesced: 11
121 moves: 17 coalesceable: 11 coalesced: 11
122 moves: 17 coalesceable: 11 coalesced: 11
123 moves: 17 coalesceable: 11 coalesced: 11
124 moves: 17 coalesceable: 11 coalesced: 11
125 moves: 17 coalesceable: 11 coalesced: 11
126 moves: 17 coalesceable: 11 coalesced: 11
127 moves: 17 coalesceable: 11 coalesced: 11
128 moves: 17 coalesceable: 11 coalesced: 11
129 moves: 17 coalesceable: 11 coalesced: 11
130 moves: 17 coalesceable: 11 coalesced: 11
131 moves: 17 coalesceable: 11 coalesced: 11
132 moves: 17 coalesceable: 11 coalesced: 11
133 moves: 17 coalesceable: 11 coalesced: 11
134 moves: 17 coalesceable: 11 coalesced: 11
135 moves: 17 coalesceable: 11 coalesced: 11
136 moves: 4375 coalesceable: 2573 coalesced: 2573
137 moves: 17 coalesceable: 11 coalesced: 11
138 moves: 17 coalesceable: 11 coalesced: 11
139 moves: 17 coalesceable: 11 coalesced: 11
140 moves: 17 coalesceable: 11 coalesced: 11
141 moves: 17 coalesceable: 11 coalesced: 11
142 moves: 17 coalesceable: 11 coalesced: 11
143 moves: 17 coalesceable: 11 coalesced: 11
144 moves: 17 coalesceable: 11 coalesced: 11
145 moves: 17 coalesceable: 11 coalesced: 11
146 moves: 17 coalesceable: 11 coalesced: 11
147 moves: 17 coalesceable: 11 coalesced: 11
148 moves: 17 coalesceable: 11 coalesced: 11
149 moves: 17 coalesceable: 11 coalesced: 11
150 moves: 17 coalesceable: 11 coalesced: 11
151 moves: 17 coalesceable: 11 coalesced: 11
152 moves: 17 coalesceable: 11 coalesced: 11
153 moves: 17 coalesceable: 11 coalesced: 11
154 moves: 10 coalesceable: 6 coalesced: 6
155 moves: 60 coalesceable: 41 coalesced: 40
156 moves: 17 coalesceable: 11 coalesced: 11
157 moves: 17 coalesceable: 11 coalesced: 11
158 moves: 17 coalesceable: 11 coalesced: 11
159 moves: 17 coalesceable: 11 coalesced: 11
160 moves: 17 coalesceable: 11 coalesced: 11
161 moves: 17 coalesceable: 11 coalesced: 11
162 moves: 17 coalesceable: 11 coalesced: 11
163 moves: 17 coalesceable: 11 coalesced: 11
164 moves: 17 coalesceable: 11 coalesced: 11
165 moves: 17 coalesceable: 11 coalesced: 11
166 moves: 2 coalesceable: 2 coalesced: 2
167 moves: 17 coalesceable: 11 coalesced: 11
168 moves: 17 coalesceable: 11 coalesced: 11
169 moves: 17 coalesceable: 11 coalesced: 11
170 moves: 5 coalesceable: 3 coalesced: 3
171 moves: 6 coalesceable: 6 coalesced: 6
172 moves: 29 coalesceable: 19 coalesced: 13
173 moves: 4 coalesceable: 4 coalesced: 4
174 moves: 7 coalesceable: 7 coalesced: 7
175 moves: 4 coalesceable: 4 coalesced: 4
176 moves: 9 coalesceable: 9 coalesced: 8
177 moves: 8 coalesceable: 8 coalesced: 8
178 moves: 124 coalesceable: 72 coalesced: 58
179 moves: 6 coalesceable: 6 coalesced: 6
180 moves: 62 coalesceable: 31 coalesced: 29
181 moves: 4 coalesceable: 4 coalesced: 4
182 moves: 48 coalesceable: 23 coalesced: 21
183 moves: 6 coalesceable: 6 coalesced: 6
184 moves: 23 coalesceable: 15 coalesced: 11
185 moves: 6 coalesceable: 6 coalesced: 6
186 moves: 23 coalesceable: 15 coalesced: 11
187 moves: 6 coalesceable: 6 coalesced: 6
188 moves: 30 coalesceable: 19 coalesced: 16
189 moves: 6 coalesceable: 6 coalesced: 6
190 moves: 29 coalesceable: 21 coalesced: 17
191 moves: 6 coalesceable: 6 coalesced: 6
192 moves: 24 coalesceable: 16 coalesced: 13
193 moves: 6 coalesceable: 6 coalesced: 6
194 moves: 24 coalesceable: 16 coalesced: 13
195 moves: 6 coalesceable: 6 coalesced: 6
196 moves: 30 coalesceable: 22 coalesced: 19
197 moves: 6 coalesceable: 6 coalesced: 6
198 moves: 60 coalesceable: 44 coalesced: 41
199 moves: 6 coalesceable: 6 coalesced: 6
200 moves: 62 coalesceable: 31 coalesced: 29
201 moves: 4 coalesceable: 4 coalesced: 4
202 moves: 3 coalesceable: 3 coalesced: 3
203 moves: 4 coalesceable: 4 coalesced: 4
204 moves: 43 coalesceable: 29 coalesced: 25
205 moves: 4 coalesceable: 4 coalesced: 4
206 moves: 3 coalesceable: 3 coalesced: 3
207 moves: 4 coalesceable: 4 coalesced: 4
208 moves: 18 coalesceable: 16 coalesced: 16
209 moves: 4 coalesceable: 4 coalesced: 4
210 moves: 25 coalesceable: 18 coalesced: 16
211 moves: 4 coalesceable: 4 coalesced: 4
212 moves: 3 coalesceable: 3 coalesced: 3
213 moves: 6 coalesceable: 6 coalesced: 6
214 moves: 36 coalesceable: 23 coalesced: 17
215 moves: 6 coalesceable: 6 coalesced: 6
216 moves: 21 coalesceable: 19 coalesced: 19
217 moves: 8 coalesceable: 8 coalesced: 8
218 moves: 22 coalesceable: 20 coalesced: 20
219 moves: 12 coalesceable: 12 coalesced: 12
220 moves: 218 coalesceable: 134 coalesced: 94
221 moves: 8 coalesceable: 8 coalesced: 8
222 moves: 124 coalesceable: 72 coalesced: 58
223 moves: 4 coalesceable: 4 coalesced: 4
224 moves: 77 coalesceable: 56 coalesced: 53
225 moves: 6 coalesceable: 6 coalesced: 6
226 moves: 110 coalesceable: 79 coalesced: 69
227 moves: 8 coalesceable: 8 coalesced: 8
228 moves: 407 coalesceable: 208 coalesced: 175
229 moves: 4 coalesceable: 4 coalesced: 4
230 moves: 56 coalesceable: 33 coalesced: 30
231 moves: 4 coalesceable: 4 coalesced: 4
232 moves: 8 coalesceable: 6 coalesced: 6
233 moves: 8 coalesceable: 8 coalesced: 8
234 moves: 163 coalesceable: 110 coalesced: 96
235 moves: 6 coalesceable: 6 coalesced: 6
236 moves: 114 coalesceable: 80 coalesced: 72
237 moves: 4 coalesceable: 4 coalesced: 4
238 moves: 6 coalesceable: 6 coalesced: 6
239 moves: 4 coalesceable: 4 coalesced: 4
240 moves: 6 coalesceable: 6 coalesced: 6
241 moves: 8 coalesceable: 8 coalesced: 8
242 moves: 128 coalesceable: 77 coalesced: 70
243 moves: 8 coalesceable: 8 coalesced: 8
244 moves: 111 coalesceable: 66 coalesced: 51
245 moves: 6 coalesceable: 6 coalesced: 6
246 moves: 50 coalesceable: 38 coalesced: 35
247 moves: 6 coalesceable: 6 coalesced: 6
248 moves: 427 coalesceable: 263 coalesced: 198
249 moves: 4 coalesceable: 4 coalesced: 4
250 moves: 5 coalesceable: 5 coalesced: 5
251 moves: 4 coalesceable: 4 coalesced: 4
252 moves: 272 coalesceable: 139 coalesced: 131
253 moves: 4 coalesceable: 4 coalesced: 4
254 moves: 69 coalesceable: 54 coalesced: 54
255 moves: 6 coalesceable: 6 coalesced: 6
256 moves: 78 coalesceable: 59 coalesced: 56
257 moves: 4 coalesceable: 4 coalesced: 4
258 moves: 21 coalesceable: 18 coalesced: 16
259 moves: 4 coalesceable: 4 coalesced: 4
260 moves: 15 coalesceable: 12 coalesced: 12
261 moves: 25 coalesceable: 21 coalesced: 21
262 moves: 24 coalesceable: 15 coalesced: 15
263 moves: 4 coalesceable: 4 coalesced: 4
264 moves: 34 coalesceable: 19 coalesced: 17
265 moves: 4 coalesceable: 4 coalesced: 4
266 moves: 16 coalesceable: 11 coalesced: 10
267 moves: 4 coalesceable: 4 coalesced: 4
268 moves: 11 coalesceable: 7 coalesced: 7
runtime: 9.2s, gctime: 0.12233s, systime: 0.01196s.
external oracle real: 9.2s
external oracle size: 146748
apply colour (par) eval: runtime: 1m28s, gctime: 6.6s, systime: 0.67242s.
apply colour (par) real: 49.8s
apply colour (par) size: 647308
check colour eval: runtime: 1.3s, gctime: 0.12723s, systime: 0.01897s.
check colour real: 1.3s
check colour size: 647578
word_to_stack eval: runtime: 1m02s, gctime: 1.9s, systime: 0.26337s.
word_to_stack real: 1m02s
word_to_stack size: 527185
stack_rawcall eval: runtime: 40.1s, gctime: 4.2s, systime: 0.26360s.
stack_rawcall real: 40.4s
stack_rawcall size: 520032
stack_alloc (par) eval: runtime: 50.6s, gctime: 0.85258s, systime: 0.11071s.
stack_alloc (par) real: 22.9s
stack_alloc (par) size: 521980
expand stack_remove_def eval: runtime: 0.03506s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.03513s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 1m14s, gctime: 8.1s, systime: 0.91348s.
stack_remove (par) real: 42.3s
stack_remove (par) size: 889970
stack_names (par) eval: runtime: 35.4s, gctime: 0.67345s, systime: 0.07584s.
stack_names (par) real: 16.5s
stack_names (par) size: 918563
stack_to_lab (par) eval: runtime: 1m12s, gctime: 1.3s, systime: 0.13379s.
stack_to_lab (par) real: 33.2s
stack_to_lab (par) size: 1119677
lab_to_target eval: runtime: 3m33s, gctime: 10.1s, systime: 0.89597s.
lab_to_target real: 3m34s
lab_to_target size: 1801640
export: runtime: 0.47625s, gctime: 0.00000s, systime: 0.15379s.
Saved theorem _____ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 13m40s to build
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "diffCompile">>
to_flat eval: runtime: 7.6s, gctime: 0.46123s, systime: 0.09794s.
to_flat real: 7.7s
to_flat size: 120491
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.79011s, gctime: 0.09699s, systime: 0.00500s.
to_clos real: 0.79626s
to_clos size: 64819
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 6.1s, gctime: 0.23551s, systime: 0.02495s.
to_bvl real: 6.1s
to_bvl size: 120565
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 45.0s, gctime: 0.44740s, systime: 0.03587s.
to_bvi real: 45.1s
to_bvi size: 118173
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 12.8s, gctime: 0.53005s, systime: 0.04496s.
to_data real: 12.9s
to_data size: 189749
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 19.5s, gctime: 0.61796s, systime: 0.04490s.
data_to_word real: 19.6s
data_to_word size: 432035
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m02s, gctime: 8.4s, systime: 0.81601s.
inst,ssa,two-reg (par) real: 41.9s
inst,ssa,two-reg (par) size: 1675692
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 14.0s, gctime: 1.3s, systime: 0.11683s.
get_clash (par) real: 4.6s
get_clash (par) size: 2632093
external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75 coalesceable: 61 coalesced: 53
1 moves: 24 coalesceable: 22 coalesced: 20
2 moves: 90 coalesceable: 68 coalesced: 53
3 moves: 25 coalesceable: 19 coalesced: 17
4 moves: 16 coalesceable: 15 coalesced: 12
5 moves: 148 coalesceable: 116 coalesced: 110
6 moves: 7 coalesceable: 7 coalesced: 7
7 moves: 7 coalesceable: 7 coalesced: 7
8 moves: 7 coalesceable: 7 coalesced: 7
9 moves: 7 coalesceable: 7 coalesced: 7
10 moves: 7 coalesceable: 7 coalesced: 7
11 moves: 19 coalesceable: 17 coalesced: 12
12 moves: 47 coalesceable: 41 coalesced: 37
13 moves: 31 coalesceable: 20 coalesced: 17
14 moves: 58 coalesceable: 48 coalesced: 42
15 moves: 0 coalesceable: 0 coalesced: 0
16 moves: 10 coalesceable: 8 coalesced: 5
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 21 coalesceable: 20 coalesced: 20
19 moves: 22 coalesceable: 21 coalesced: 20
20 moves: 19 coalesceable: 15 coalesced: 15
21 moves: 35 coalesceable: 29 coalesced: 25
22 moves: 40 coalesceable: 34 coalesced: 33
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 19 coalesceable: 17 coalesced: 15
25 moves: 42 coalesceable: 38 coalesced: 29
26 moves: 20 coalesceable: 20 coalesced: 14
27 moves: 20 coalesceable: 20 coalesced: 10
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 316 coalesceable: 269 coalesced: 269
31 moves: 26 coalesceable: 23 coalesced: 23
32 moves: 24 coalesceable: 23 coalesced: 23
33 moves: 16 coalesceable: 15 coalesced: 15
34 moves: 22 coalesceable: 19 coalesced: 19
35 moves: 90 coalesceable: 81 coalesced: 81
36 moves: 85 coalesceable: 82 coalesced: 82
37 moves: 65 coalesceable: 62 coalesced: 62
38 moves: 88 coalesceable: 85 coalesced: 85
39 moves: 29 coalesceable: 26 coalesced: 26
40 moves: 48 coalesceable: 45 coalesced: 45
41 moves: 7 coalesceable: 6 coalesced: 6
42 moves: 22 coalesceable: 19 coalesced: 19
43 moves: 12 coalesceable: 11 coalesced: 11
44 moves: 21 coalesceable: 18 coalesced: 18
45 moves: 51 coalesceable: 48 coalesced: 48
46 moves: 8 coalesceable: 7 coalesced: 7
47 moves: 11 coalesceable: 10 coalesced: 10
48 moves: 22 coalesceable: 19 coalesced: 19
49 moves: 26 coalesceable: 23 coalesced: 23
50 moves: 15 coalesceable: 14 coalesced: 14
51 moves: 20 coalesceable: 17 coalesced: 17
52 moves: 24 coalesceable: 21 coalesced: 21
53 moves: 190 coalesceable: 117 coalesced: 103
54 moves: 92 coalesceable: 65 coalesced: 51
55 moves: 41 coalesceable: 26 coalesced: 25
56 moves: 35 coalesceable: 26 coalesced: 21
57 moves: 56 coalesceable: 42 coalesced: 36
58 moves: 71 coalesceable: 46 coalesced: 40
59 moves: 48 coalesceable: 37 coalesced: 32
60 moves: 71 coalesceable: 46 coalesced: 38
61 moves: 927 coalesceable: 603 coalesced: 410
62 moves: 1088 coalesceable: 687 coalesced: 404
63 moves: 1169 coalesceable: 725 coalesced: 434
64 moves: 1254 coalesceable: 765 coalesced: 434
65 moves: 1343 coalesceable: 807 coalesced: 407
66 moves: 1436 coalesceable: 851 coalesced: 420
67 moves: 1533 coalesceable: 897 coalesced: 459
68 moves: 1634 coalesceable: 943 coalesced: 482
69 moves: 1739 coalesceable: 989 coalesced: 504
70 moves: 1848 coalesceable: 1035 coalesced: 506
71 moves: 17 coalesceable: 15 coalesced: 15
72 moves: 19 coalesceable: 17 coalesced: 17
73 moves: 21 coalesceable: 18 coalesced: 17
74 moves: 21 coalesceable: 19 coalesced: 19
75 moves: 23 coalesceable: 20 coalesced: 19
76 moves: 25 coalesceable: 21 coalesced: 20
77 moves: 23 coalesceable: 21 coalesced: 21
78 moves: 25 coalesceable: 22 coalesced: 21
79 moves: 27 coalesceable: 23 coalesced: 22
80 moves: 29 coalesceable: 24 coalesced: 23
81 moves: 25 coalesceable: 23 coalesced: 19
82 moves: 27 coalesceable: 24 coalesced: 20
83 moves: 29 coalesceable: 25 coalesced: 21
84 moves: 31 coalesceable: 26 coalesced: 22
85 moves: 33 coalesceable: 27 coalesced: 23
86 moves: 27 coalesceable: 24 coalesced: 21
87 moves: 29 coalesceable: 25 coalesced: 22
88 moves: 31 coalesceable: 26 coalesced: 23
89 moves: 33 coalesceable: 27 coalesced: 24
90 moves: 35 coalesceable: 28 coalesced: 25
91 moves: 37 coalesceable: 29 coalesced: 26
92 moves: 29 coalesceable: 25 coalesced: 16
93 moves: 31 coalesceable: 26 coalesced: 18
94 moves: 33 coalesceable: 27 coalesced: 23
95 moves: 35 coalesceable: 28 coalesced: 21
96 moves: 37 coalesceable: 29 coalesced: 22
97 moves: 39 coalesceable: 30 coalesced: 23
98 moves: 41 coalesceable: 31 coalesced: 24
99 moves: 31 coalesceable: 25 coalesced: 12
100 moves: 33 coalesceable: 27 coalesced: 9
101 moves: 35 coalesceable: 28 coalesced: 16
102 moves: 37 coalesceable: 29 coalesced: 23
103 moves: 39 coalesceable: 30 coalesced: 23
104 moves: 41 coalesceable: 31 coalesced: 21
105 moves: 43 coalesceable: 32 coalesced: 22
106 moves: 45 coalesceable: 33 coalesced: 25
107 moves: 33 coalesceable: 25 coalesced: 14
108 moves: 35 coalesceable: 27 coalesced: 10
109 moves: 37 coalesceable: 29 coalesced: 11
110 moves: 39 coalesceable: 30 coalesced: 14
111 moves: 41 coalesceable: 31 coalesced: 21
112 moves: 43 coalesceable: 32 coalesced: 23
113 moves: 45 coalesceable: 33 coalesced: 23
114 moves: 47 coalesceable: 34 coalesced: 23
115 moves: 49 coalesceable: 35 coalesced: 25
116 moves: 62 coalesceable: 11 coalesced: 7
117 moves: 972 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 11 coalesced: 11
119 moves: 17 coalesceable: 11 coalesced: 11
120 moves: 17 coalesceable: 11 coalesced: 11
121 moves: 17 coalesceable: 11 coalesced: 11
122 moves: 17 coalesceable: 11 coalesced: 11
123 moves: 17 coalesceable: 11 coalesced: 11
124 moves: 17 coalesceable: 11 coalesced: 11
125 moves: 17 coalesceable: 11 coalesced: 11
126 moves: 17 coalesceable: 11 coalesced: 11
127 moves: 17 coalesceable: 11 coalesced: 11
128 moves: 17 coalesceable: 11 coalesced: 11
129 moves: 17 coalesceable: 11 coalesced: 11
130 moves: 17 coalesceable: 11 coalesced: 11
131 moves: 17 coalesceable: 11 coalesced: 11
132 moves: 17 coalesceable: 11 coalesced: 11
133 moves: 17 coalesceable: 11 coalesced: 11
134 moves: 17 coalesceable: 11 coalesced: 11
135 moves: 17 coalesceable: 11 coalesced: 11
136 moves: 17 coalesceable: 11 coalesced: 11
137 moves: 17 coalesceable: 11 coalesced: 11
138 moves: 17 coalesceable: 11 coalesced: 11
139 moves: 17 coalesceable: 11 coalesced: 11
140 moves: 17 coalesceable: 11 coalesced: 11
141 moves: 17 coalesceable: 11 coalesced: 11
142 moves: 17 coalesceable: 11 coalesced: 11
143 moves: 17 coalesceable: 11 coalesced: 11
144 moves: 17 coalesceable: 11 coalesced: 11
145 moves: 17 coalesceable: 11 coalesced: 11
146 moves: 17 coalesceable: 11 coalesced: 11
147 moves: 17 coalesceable: 11 coalesced: 11
148 moves: 17 coalesceable: 11 coalesced: 11
149 moves: 17 coalesceable: 11 coalesced: 11
150 moves: 4375 coalesceable: 2573 coalesced: 2573
151 moves: 17 coalesceable: 11 coalesced: 11
152 moves: 17 coalesceable: 11 coalesced: 11
153 moves: 17 coalesceable: 11 coalesced: 11
154 moves: 17 coalesceable: 11 coalesced: 11
155 moves: 17 coalesceable: 11 coalesced: 11
156 moves: 17 coalesceable: 11 coalesced: 11
157 moves: 17 coalesceable: 11 coalesced: 11
158 moves: 17 coalesceable: 11 coalesced: 11
159 moves: 17 coalesceable: 11 coalesced: 11
160 moves: 17 coalesceable: 11 coalesced: 11
161 moves: 17 coalesceable: 11 coalesced: 11
162 moves: 17 coalesceable: 11 coalesced: 11
163 moves: 17 coalesceable: 11 coalesced: 11
164 moves: 17 coalesceable: 11 coalesced: 11
165 moves: 17 coalesceable: 11 coalesced: 11
166 moves: 17 coalesceable: 11 coalesced: 11
167 moves: 17 coalesceable: 11 coalesced: 11
168 moves: 17 coalesceable: 11 coalesced: 11
169 moves: 10 coalesceable: 6 coalesced: 6
170 moves: 60 coalesceable: 41 coalesced: 40
171 moves: 60 coalesceable: 41 coalesced: 40
172 moves: 17 coalesceable: 11 coalesced: 11
173 moves: 17 coalesceable: 11 coalesced: 11
174 moves: 17 coalesceable: 11 coalesced: 11
175 moves: 17 coalesceable: 11 coalesced: 11
176 moves: 17 coalesceable: 11 coalesced: 11
177 moves: 17 coalesceable: 11 coalesced: 11
178 moves: 17 coalesceable: 11 coalesced: 11
179 moves: 17 coalesceable: 11 coalesced: 11
180 moves: 17 coalesceable: 11 coalesced: 11
181 moves: 17 coalesceable: 11 coalesced: 11
182 moves: 17 coalesceable: 11 coalesced: 11
183 moves: 17 coalesceable: 11 coalesced: 11
184 moves: 17 coalesceable: 11 coalesced: 11
185 moves: 2 coalesceable: 2 coalesced: 2
186 moves: 17 coalesceable: 11 coalesced: 11
187 moves: 17 coalesceable: 11 coalesced: 11
188 moves: 17 coalesceable: 11 coalesced: 11
189 moves: 17 coalesceable: 11 coalesced: 11
190 moves: 17 coalesceable: 11 coalesced: 11
191 moves: 17 coalesceable: 11 coalesced: 11
192 moves: 17 coalesceable: 11 coalesced: 11
193 moves: 17 coalesceable: 11 coalesced: 11
194 moves: 17 coalesceable: 11 coalesced: 11
195 moves: 17 coalesceable: 11 coalesced: 11
196 moves: 17 coalesceable: 11 coalesced: 11
197 moves: 17 coalesceable: 11 coalesced: 11
198 moves: 17 coalesceable: 11 coalesced: 11
199 moves: 17 coalesceable: 11 coalesced: 11
200 moves: 17 coalesceable: 11 coalesced: 11
201 moves: 17 coalesceable: 11 coalesced: 11
202 moves: 17 coalesceable: 11 coalesced: 11
203 moves: 114 coalesceable: 84 coalesced: 84
204 moves: 17 coalesceable: 11 coalesced: 11
205 moves: 17 coalesceable: 11 coalesced: 11
206 moves: 5 coalesceable: 3 coalesced: 3
207 moves: 4 coalesceable: 4 coalesced: 4
208 moves: 6 coalesceable: 6 coalesced: 6
209 moves: 4 coalesceable: 4 coalesced: 4
210 moves: 6 coalesceable: 6 coalesced: 6
211 moves: 6 coalesceable: 6 coalesced: 6
212 moves: 29 coalesceable: 19 coalesced: 13
213 moves: 6 coalesceable: 6 coalesced: 6
214 moves: 32 coalesceable: 23 coalesced: 18
215 moves: 4 coalesceable: 4 coalesced: 4
216 moves: 5 coalesceable: 5 coalesced: 3
217 moves: 6 coalesceable: 6 coalesced: 6
218 moves: 36 coalesceable: 25 coalesced: 24
219 moves: 4 coalesceable: 4 coalesced: 4
220 moves: 5 coalesceable: 5 coalesced: 3
221 moves: 4 coalesceable: 4 coalesced: 4
222 moves: 7 coalesceable: 7 coalesced: 7
223 moves: 4 coalesceable: 4 coalesced: 4
224 moves: 7 coalesceable: 7 coalesced: 7
225 moves: 4 coalesceable: 4 coalesced: 4
226 moves: 45 coalesceable: 35 coalesced: 33
227 moves: 6 coalesceable: 6 coalesced: 6
228 moves: 86 coalesceable: 57 coalesced: 51
229 moves: 6 coalesceable: 6 coalesced: 6
230 moves: 76 coalesceable: 47 coalesced: 43
231 moves: 4 coalesceable: 4 coalesced: 4
232 moves: 9 coalesceable: 9 coalesced: 8
233 moves: 8 coalesceable: 8 coalesced: 8
234 moves: 124 coalesceable: 72 coalesced: 58
235 moves: 6 coalesceable: 6 coalesced: 6
236 moves: 62 coalesceable: 31 coalesced: 29
237 moves: 4 coalesceable: 4 coalesced: 4
238 moves: 48 coalesceable: 23 coalesced: 21
239 moves: 6 coalesceable: 6 coalesced: 6
240 moves: 23 coalesceable: 15 coalesced: 11
241 moves: 6 coalesceable: 6 coalesced: 6
242 moves: 23 coalesceable: 15 coalesced: 11
243 moves: 6 coalesceable: 6 coalesced: 6
244 moves: 30 coalesceable: 19 coalesced: 16
245 moves: 6 coalesceable: 6 coalesced: 6
246 moves: 29 coalesceable: 21 coalesced: 17
247 moves: 6 coalesceable: 6 coalesced: 6
248 moves: 24 coalesceable: 16 coalesced: 13
249 moves: 6 coalesceable: 6 coalesced: 6
250 moves: 24 coalesceable: 16 coalesced: 13
251 moves: 6 coalesceable: 6 coalesced: 6
252 moves: 30 coalesceable: 22 coalesced: 19
253 moves: 6 coalesceable: 6 coalesced: 6
254 moves: 60 coalesceable: 44 coalesced: 41
255 moves: 6 coalesceable: 6 coalesced: 6
256 moves: 62 coalesceable: 31 coalesced: 29
257 moves: 6 coalesceable: 6 coalesced: 6
258 moves: 79 coalesceable: 52 coalesced: 46
259 moves: 4 coalesceable: 4 coalesced: 4
260 moves: 162 coalesceable: 108 coalesced: 98
261 moves: 8 coalesceable: 8 coalesced: 8
262 moves: 284 coalesceable: 173 coalesced: 140
263 moves: 8 coalesceable: 8 coalesced: 8
264 moves: 119 coalesceable: 79 coalesced: 60
265 moves: 4 coalesceable: 4 coalesced: 4
266 moves: 423 coalesceable: 264 coalesced: 209
267 moves: 4 coalesceable: 4 coalesced: 4
268 moves: 3 coalesceable: 3 coalesced: 3
269 moves: 4 coalesceable: 4 coalesced: 4
270 moves: 43 coalesceable: 29 coalesced: 25
271 moves: 4 coalesceable: 4 coalesced: 4
272 moves: 25 coalesceable: 18 coalesced: 16
273 moves: 4 coalesceable: 4 coalesced: 4
274 moves: 3 coalesceable: 3 coalesced: 3
275 moves: 6 coalesceable: 6 coalesced: 6
276 moves: 36 coalesceable: 23 coalesced: 17
277 moves: 6 coalesceable: 6 coalesced: 6
278 moves: 21 coalesceable: 19 coalesced: 19
279 moves: 4 coalesceable: 4 coalesced: 4
280 moves: 9 coalesceable: 9 coalesced: 8
281 moves: 8 coalesceable: 8 coalesced: 8
282 moves: 22 coalesceable: 20 coalesced: 20
283 moves: 12 coalesceable: 12 coalesced: 12
284 moves: 218 coalesceable: 134 coalesced: 94
285 moves: 12 coalesceable: 12 coalesced: 12
286 moves: 218 coalesceable: 134 coalesced: 94
287 moves: 8 coalesceable: 8 coalesced: 8
288 moves: 124 coalesceable: 72 coalesced: 58
289 moves: 4 coalesceable: 4 coalesced: 4
290 moves: 77 coalesceable: 56 coalesced: 53
291 moves: 6 coalesceable: 6 coalesced: 6
292 moves: 110 coalesceable: 79 coalesced: 69
293 moves: 8 coalesceable: 8 coalesced: 8
294 moves: 407 coalesceable: 208 coalesced: 175
295 moves: 4 coalesceable: 4 coalesced: 4
296 moves: 56 coalesceable: 33 coalesced: 30
297 moves: 4 coalesceable: 4 coalesced: 4
298 moves: 8 coalesceable: 6 coalesced: 6
299 moves: 8 coalesceable: 8 coalesced: 8
300 moves: 163 coalesceable: 110 coalesced: 96
301 moves: 6 coalesceable: 6 coalesced: 6
302 moves: 114 coalesceable: 80 coalesced: 72
303 moves: 4 coalesceable: 4 coalesced: 4
304 moves: 6 coalesceable: 6 coalesced: 6
305 moves: 4 coalesceable: 4 coalesced: 4
306 moves: 6 coalesceable: 6 coalesced: 6
307 moves: 8 coalesceable: 8 coalesced: 8
308 moves: 128 coalesceable: 77 coalesced: 70
309 moves: 8 coalesceable: 8 coalesced: 8
310 moves: 111 coalesceable: 66 coalesced: 51
311 moves: 6 coalesceable: 6 coalesced: 6
312 moves: 427 coalesceable: 263 coalesced: 198
313 moves: 4 coalesceable: 4 coalesced: 4
314 moves: 5 coalesceable: 5 coalesced: 5
315 moves: 4 coalesceable: 4 coalesced: 4
316 moves: 17 coalesceable: 12 coalesced: 11
317 moves: 4 coalesceable: 4 coalesced: 4
318 moves: 272 coalesceable: 139 coalesced: 131
319 moves: 4 coalesceable: 4 coalesced: 4
320 moves: 69 coalesceable: 54 coalesced: 54
321 moves: 6 coalesceable: 6 coalesced: 6
322 moves: 78 coalesceable: 59 coalesced: 56
323 moves: 4 coalesceable: 4 coalesced: 4
324 moves: 21 coalesceable: 18 coalesced: 16
325 moves: 4 coalesceable: 4 coalesced: 4
326 moves: 164 coalesceable: 106 coalesced: 89
327 moves: 224 coalesceable: 137 coalesced: 113
328 moves: 217 coalesceable: 133 coalesced: 108
329 moves: 4 coalesceable: 4 coalesced: 4
330 moves: 45 coalesceable: 26 coalesced: 24
331 moves: 4 coalesceable: 4 coalesced: 4
332 moves: 42 coalesceable: 23 coalesced: 22
333 moves: 4 coalesceable: 4 coalesced: 4
334 moves: 15 coalesceable: 12 coalesced: 12
335 moves: 36 coalesceable: 18 coalesced: 18
336 moves: 6 coalesceable: 6 coalesced: 6
337 moves: 95 coalesceable: 59 coalesced: 59
338 moves: 12 coalesceable: 12 coalesced: 12
339 moves: 362 coalesceable: 166 coalesced: 106
340 moves: 8 coalesceable: 8 coalesced: 8
341 moves: 98 coalesceable: 66 coalesced: 52
342 moves: 6 coalesceable: 6 coalesced: 6
343 moves: 84 coalesceable: 52 coalesced: 43
344 moves: 6 coalesceable: 6 coalesced: 6
345 moves: 55 coalesceable: 28 coalesced: 23
346 moves: 6 coalesceable: 6 coalesced: 6
347 moves: 90 coalesceable: 61 coalesced: 58
348 moves: 8 coalesceable: 8 coalesced: 8
349 moves: 157 coalesceable: 106 coalesced: 88
350 moves: 6 coalesceable: 6 coalesced: 6
351 moves: 99 coalesceable: 62 coalesced: 56
352 moves: 6 coalesceable: 6 coalesced: 6
353 moves: 275 coalesceable: 122 coalesced: 107
354 moves: 6 coalesceable: 6 coalesced: 6
355 moves: 7 coalesceable: 7 coalesced: 7
356 moves: 10 coalesceable: 10 coalesced: 10
357 moves: 375 coalesceable: 141 coalesced: 119
358 moves: 6 coalesceable: 6 coalesced: 6
359 moves: 35 coalesceable: 25 coalesced: 20
360 moves: 10 coalesceable: 10 coalesced: 10
361 moves: 1001 coalesceable: 448 coalesced: 387
362 moves: 6 coalesceable: 6 coalesced: 6
363 moves: 162 coalesceable: 92 coalesced: 88
364 moves: 33 coalesceable: 25 coalesced: 23
365 moves: 33 coalesceable: 25 coalesced: 23
366 moves: 12 coalesceable: 12 coalesced: 12
367 moves: 2015 coalesceable: 1063 coalesced: 797
368 moves: 6 coalesceable: 6 coalesced: 6
369 moves: 690 coalesceable: 353 coalesced: 200
370 moves: 4 coalesceable: 4 coalesced: 4
371 moves: 266 coalesceable: 170 coalesced: 166
372 moves: 6 coalesceable: 6 coalesced: 6
373 moves: 570 coalesceable: 359 coalesced: 352
374 moves: 4 coalesceable: 4 coalesced: 4
375 moves: 47 coalesceable: 39 coalesced: 39
runtime: 9.1s, gctime: 0.14109s, systime: 0.02193s.
external oracle real: 9.2s
external oracle size: 198691
apply colour (par) eval: runtime: 2m29s, gctime: 7.8s, systime: 0.98985s.
apply colour (par) real: 56.8s
apply colour (par) size: 849607
check colour eval: runtime: 3.1s, gctime: 0.42791s, systime: 0.07092s.
check colour real: 3.2s
check colour size: 849984
word_to_stack eval: runtime: 1m31s, gctime: 7.7s, systime: 1.1s.
word_to_stack real: 1m32s
word_to_stack size: 673984
stack_rawcall eval: runtime: 46.9s, gctime: 0.54946s, systime: 0.06479s.
stack_rawcall real: 47.0s
stack_rawcall size: 665204
stack_alloc (par) eval: runtime: 1m14s, gctime: 0.73894s, systime: 0.10783s.
stack_alloc (par) real: 24.5s
stack_alloc (par) size: 669170
expand stack_remove_def eval: runtime: 0.03394s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.03401s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 1m41s, gctime: 0.97235s, systime: 0.14349s.
stack_remove (par) real: 37.8s
stack_remove (par) size: 1120033
stack_names (par) eval: runtime: 51.7s, gctime: 0.85036s, systime: 0.09976s.
stack_names (par) real: 17.2s
stack_names (par) size: 1156806
stack_to_lab (par) eval: runtime: 1m47s, gctime: 1.7s, systime: 0.17274s.
stack_to_lab (par) real: 35.0s
stack_to_lab (par) size: 1425269
lab_to_target eval: runtime: 4m38s, gctime: 19.3s, systime: 1.8s.
lab_to_target real: 4m41s
lab_to_target size: 2313542
export: runtime: 0.48799s, gctime: 0.00000s, systime: 0.00199s.
Saved theorem _____ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 19m28s to build
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "echoCompile">>
to_flat eval: runtime: 6.5s, gctime: 0.27650s, systime: 0.11785s.
to_flat real: 6.6s
to_flat size: 67572
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.33475s, gctime: 0.06708s, systime: 0.00301s.
to_clos real: 0.33839s
to_clos size: 40080
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 4.1s, gctime: 0.14212s, systime: 0.01803s.
to_bvl real: 4.1s
to_bvl size: 67165
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 34.6s, gctime: 0.38284s, systime: 0.03406s.
to_bvi real: 34.6s
to_bvi size: 72907
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 10.3s, gctime: 0.51623s, systime: 0.04694s.
to_data real: 10.4s
to_data size: 121432
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 14.6s, gctime: 0.59158s, systime: 0.04486s.
data_to_word real: 14.7s
data_to_word size: 311616
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 1m05s, gctime: 2.7s, systime: 0.31045s.
inst,ssa,two-reg (par) real: 31.8s
inst,ssa,two-reg (par) size: 1252479
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 7.6s, gctime: 1.1s, systime: 0.09988s.
get_clash (par) real: 3.9s
get_clash (par) size: 1948615
external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75 coalesceable: 61 coalesced: 53
1 moves: 24 coalesceable: 22 coalesced: 20
2 moves: 90 coalesceable: 68 coalesced: 53
3 moves: 25 coalesceable: 19 coalesced: 17
4 moves: 16 coalesceable: 15 coalesced: 12
5 moves: 148 coalesceable: 116 coalesced: 110
6 moves: 7 coalesceable: 7 coalesced: 7
7 moves: 7 coalesceable: 7 coalesced: 7
8 moves: 7 coalesceable: 7 coalesced: 7
9 moves: 7 coalesceable: 7 coalesced: 7
10 moves: 7 coalesceable: 7 coalesced: 7
11 moves: 19 coalesceable: 17 coalesced: 12
12 moves: 47 coalesceable: 41 coalesced: 37
13 moves: 31 coalesceable: 20 coalesced: 17
14 moves: 58 coalesceable: 48 coalesced: 42
15 moves: 0 coalesceable: 0 coalesced: 0
16 moves: 10 coalesceable: 8 coalesced: 5
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 21 coalesceable: 20 coalesced: 20
19 moves: 22 coalesceable: 21 coalesced: 20
20 moves: 19 coalesceable: 15 coalesced: 15
21 moves: 35 coalesceable: 29 coalesced: 25
22 moves: 40 coalesceable: 34 coalesced: 33
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 19 coalesceable: 17 coalesced: 15
25 moves: 42 coalesceable: 38 coalesced: 29
26 moves: 20 coalesceable: 20 coalesced: 14
27 moves: 20 coalesceable: 20 coalesced: 10
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 316 coalesceable: 269 coalesced: 269
31 moves: 26 coalesceable: 23 coalesced: 23
32 moves: 24 coalesceable: 23 coalesced: 23
33 moves: 16 coalesceable: 15 coalesced: 15
34 moves: 22 coalesceable: 19 coalesced: 19
35 moves: 90 coalesceable: 81 coalesced: 81
36 moves: 85 coalesceable: 82 coalesced: 82
37 moves: 65 coalesceable: 62 coalesced: 62
38 moves: 88 coalesceable: 85 coalesced: 85
39 moves: 29 coalesceable: 26 coalesced: 26
40 moves: 48 coalesceable: 45 coalesced: 45
41 moves: 7 coalesceable: 6 coalesced: 6
42 moves: 22 coalesceable: 19 coalesced: 19
43 moves: 12 coalesceable: 11 coalesced: 11
44 moves: 21 coalesceable: 18 coalesced: 18
45 moves: 51 coalesceable: 48 coalesced: 48
46 moves: 8 coalesceable: 7 coalesced: 7
47 moves: 11 coalesceable: 10 coalesced: 10
48 moves: 22 coalesceable: 19 coalesced: 19
49 moves: 26 coalesceable: 23 coalesced: 23
50 moves: 15 coalesceable: 14 coalesced: 14
51 moves: 20 coalesceable: 17 coalesced: 17
52 moves: 24 coalesceable: 21 coalesced: 21
53 moves: 190 coalesceable: 117 coalesced: 103
54 moves: 92 coalesceable: 65 coalesced: 51
55 moves: 41 coalesceable: 26 coalesced: 25
56 moves: 35 coalesceable: 26 coalesced: 21
57 moves: 56 coalesceable: 42 coalesced: 36
58 moves: 71 coalesceable: 46 coalesced: 40
59 moves: 48 coalesceable: 37 coalesced: 32
60 moves: 71 coalesceable: 46 coalesced: 38
61 moves: 927 coalesceable: 603 coalesced: 410
62 moves: 1088 coalesceable: 687 coalesced: 404
63 moves: 1169 coalesceable: 725 coalesced: 434
64 moves: 1254 coalesceable: 765 coalesced: 434
65 moves: 1343 coalesceable: 807 coalesced: 407
66 moves: 1436 coalesceable: 851 coalesced: 420
67 moves: 1533 coalesceable: 897 coalesced: 459
68 moves: 1634 coalesceable: 943 coalesced: 482
69 moves: 1739 coalesceable: 989 coalesced: 504
70 moves: 1848 coalesceable: 1035 coalesced: 506
71 moves: 17 coalesceable: 15 coalesced: 15
72 moves: 19 coalesceable: 17 coalesced: 17
73 moves: 21 coalesceable: 18 coalesced: 17
74 moves: 21 coalesceable: 19 coalesced: 19
75 moves: 23 coalesceable: 20 coalesced: 19
76 moves: 25 coalesceable: 21 coalesced: 20
77 moves: 23 coalesceable: 21 coalesced: 21
78 moves: 25 coalesceable: 22 coalesced: 21
79 moves: 27 coalesceable: 23 coalesced: 22
80 moves: 29 coalesceable: 24 coalesced: 23
81 moves: 25 coalesceable: 23 coalesced: 19
82 moves: 27 coalesceable: 24 coalesced: 20
83 moves: 29 coalesceable: 25 coalesced: 21
84 moves: 31 coalesceable: 26 coalesced: 22
85 moves: 33 coalesceable: 27 coalesced: 23
86 moves: 27 coalesceable: 24 coalesced: 21
87 moves: 29 coalesceable: 25 coalesced: 22
88 moves: 31 coalesceable: 26 coalesced: 23
89 moves: 33 coalesceable: 27 coalesced: 24
90 moves: 35 coalesceable: 28 coalesced: 25
91 moves: 37 coalesceable: 29 coalesced: 26
92 moves: 29 coalesceable: 25 coalesced: 16
93 moves: 31 coalesceable: 26 coalesced: 18
94 moves: 33 coalesceable: 27 coalesced: 23
95 moves: 35 coalesceable: 28 coalesced: 21
96 moves: 37 coalesceable: 29 coalesced: 22
97 moves: 39 coalesceable: 30 coalesced: 23
98 moves: 41 coalesceable: 31 coalesced: 24
99 moves: 31 coalesceable: 25 coalesced: 12
100 moves: 33 coalesceable: 27 coalesced: 9
101 moves: 35 coalesceable: 28 coalesced: 16
102 moves: 37 coalesceable: 29 coalesced: 23
103 moves: 39 coalesceable: 30 coalesced: 23
104 moves: 41 coalesceable: 31 coalesced: 21
105 moves: 43 coalesceable: 32 coalesced: 22
106 moves: 45 coalesceable: 33 coalesced: 25
107 moves: 33 coalesceable: 25 coalesced: 14
108 moves: 35 coalesceable: 27 coalesced: 10
109 moves: 37 coalesceable: 29 coalesced: 11
110 moves: 39 coalesceable: 30 coalesced: 14
111 moves: 41 coalesceable: 31 coalesced: 21
112 moves: 43 coalesceable: 32 coalesced: 23
113 moves: 45 coalesceable: 33 coalesced: 23
114 moves: 47 coalesceable: 34 coalesced: 23
115 moves: 49 coalesceable: 35 coalesced: 25
116 moves: 62 coalesceable: 11 coalesced: 7
117 moves: 934 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 11 coalesced: 11
119 moves: 17 coalesceable: 11 coalesced: 11
120 moves: 17 coalesceable: 11 coalesced: 11
121 moves: 17 coalesceable: 11 coalesced: 11
122 moves: 17 coalesceable: 11 coalesced: 11
123 moves: 17 coalesceable: 11 coalesced: 11
124 moves: 17 coalesceable: 11 coalesced: 11
125 moves: 17 coalesceable: 11 coalesced: 11
126 moves: 17 coalesceable: 11 coalesced: 11
127 moves: 17 coalesceable: 11 coalesced: 11
128 moves: 17 coalesceable: 11 coalesced: 11
129 moves: 17 coalesceable: 11 coalesced: 11
130 moves: 17 coalesceable: 11 coalesced: 11
131 moves: 17 coalesceable: 11 coalesced: 11
132 moves: 17 coalesceable: 11 coalesced: 11
133 moves: 4375 coalesceable: 2573 coalesced: 2573
134 moves: 17 coalesceable: 11 coalesced: 11
135 moves: 17 coalesceable: 11 coalesced: 11
136 moves: 17 coalesceable: 11 coalesced: 11
137 moves: 17 coalesceable: 11 coalesced: 11
138 moves: 17 coalesceable: 11 coalesced: 11
139 moves: 17 coalesceable: 11 coalesced: 11
140 moves: 17 coalesceable: 11 coalesced: 11
141 moves: 17 coalesceable: 11 coalesced: 11
142 moves: 17 coalesceable: 11 coalesced: 11
143 moves: 17 coalesceable: 11 coalesced: 11
144 moves: 17 coalesceable: 11 coalesced: 11
145 moves: 17 coalesceable: 11 coalesced: 11
146 moves: 17 coalesceable: 11 coalesced: 11
147 moves: 17 coalesceable: 11 coalesced: 11
148 moves: 17 coalesceable: 11 coalesced: 11
149 moves: 10 coalesceable: 6 coalesced: 6
150 moves: 60 coalesceable: 41 coalesced: 40
151 moves: 17 coalesceable: 11 coalesced: 11
152 moves: 17 coalesceable: 11 coalesced: 11
153 moves: 17 coalesceable: 11 coalesced: 11
154 moves: 17 coalesceable: 11 coalesced: 11
155 moves: 17 coalesceable: 11 coalesced: 11
156 moves: 2 coalesceable: 2 coalesced: 2
157 moves: 17 coalesceable: 11 coalesced: 11
158 moves: 5 coalesceable: 3 coalesced: 3
159 moves: 6 coalesceable: 6 coalesced: 6
160 moves: 29 coalesceable: 19 coalesced: 13
161 moves: 4 coalesceable: 4 coalesced: 4
162 moves: 7 coalesceable: 7 coalesced: 7
163 moves: 4 coalesceable: 4 coalesced: 4
164 moves: 9 coalesceable: 9 coalesced: 8
165 moves: 8 coalesceable: 8 coalesced: 8
166 moves: 124 coalesceable: 72 coalesced: 58
167 moves: 6 coalesceable: 6 coalesced: 6
168 moves: 62 coalesceable: 31 coalesced: 29
169 moves: 8 coalesceable: 8 coalesced: 8
170 moves: 180 coalesceable: 93 coalesced: 89
171 moves: 6 coalesceable: 6 coalesced: 6
172 moves: 7 coalesceable: 7 coalesced: 4
173 moves: 6 coalesceable: 6 coalesced: 6
174 moves: 23 coalesceable: 15 coalesced: 11
175 moves: 6 coalesceable: 6 coalesced: 6
176 moves: 23 coalesceable: 15 coalesced: 11
177 moves: 6 coalesceable: 6 coalesced: 6
178 moves: 30 coalesceable: 19 coalesced: 16
179 moves: 6 coalesceable: 6 coalesced: 6
180 moves: 29 coalesceable: 21 coalesced: 17
181 moves: 6 coalesceable: 6 coalesced: 6
182 moves: 24 coalesceable: 16 coalesced: 13
183 moves: 6 coalesceable: 6 coalesced: 6
184 moves: 24 coalesceable: 16 coalesced: 13
185 moves: 6 coalesceable: 6 coalesced: 6
186 moves: 30 coalesceable: 22 coalesced: 19
187 moves: 4 coalesceable: 4 coalesced: 4
188 moves: 3 coalesceable: 3 coalesced: 3
189 moves: 4 coalesceable: 4 coalesced: 4
190 moves: 25 coalesceable: 18 coalesced: 16
191 moves: 4 coalesceable: 4 coalesced: 4
192 moves: 3 coalesceable: 3 coalesced: 3
193 moves: 6 coalesceable: 6 coalesced: 6
194 moves: 36 coalesceable: 23 coalesced: 17
195 moves: 6 coalesceable: 6 coalesced: 6
196 moves: 21 coalesceable: 19 coalesced: 19
197 moves: 8 coalesceable: 8 coalesced: 8
198 moves: 22 coalesceable: 20 coalesced: 20
199 moves: 12 coalesceable: 12 coalesced: 12
200 moves: 218 coalesceable: 134 coalesced: 94
201 moves: 8 coalesceable: 8 coalesced: 8
202 moves: 124 coalesceable: 72 coalesced: 58
203 moves: 4 coalesceable: 4 coalesced: 4
204 moves: 77 coalesceable: 56 coalesced: 53
205 moves: 6 coalesceable: 6 coalesced: 6
206 moves: 110 coalesceable: 79 coalesced: 69
207 moves: 8 coalesceable: 8 coalesced: 8
208 moves: 407 coalesceable: 208 coalesced: 175
209 moves: 4 coalesceable: 4 coalesced: 4
210 moves: 56 coalesceable: 33 coalesced: 30
211 moves: 4 coalesceable: 4 coalesced: 4
212 moves: 8 coalesceable: 6 coalesced: 6
213 moves: 8 coalesceable: 8 coalesced: 8
214 moves: 163 coalesceable: 110 coalesced: 96
215 moves: 6 coalesceable: 6 coalesced: 6
216 moves: 114 coalesceable: 80 coalesced: 72
217 moves: 4 coalesceable: 4 coalesced: 4
218 moves: 6 coalesceable: 6 coalesced: 6
219 moves: 8 coalesceable: 8 coalesced: 8
220 moves: 128 coalesceable: 77 coalesced: 70
221 moves: 8 coalesceable: 8 coalesced: 8
222 moves: 111 coalesceable: 66 coalesced: 51
223 moves: 6 coalesceable: 6 coalesced: 6
224 moves: 50 coalesceable: 38 coalesced: 35
225 moves: 6 coalesceable: 6 coalesced: 6
226 moves: 427 coalesceable: 263 coalesced: 198
227 moves: 4 coalesceable: 4 coalesced: 4
228 moves: 5 coalesceable: 5 coalesced: 5
229 moves: 4 coalesceable: 4 coalesced: 4
230 moves: 36 coalesceable: 21 coalesced: 19
runtime: 9.5s, gctime: 0.13874s, systime: 0.01593s.
external oracle real: 9.5s
external oracle size: 141827
apply colour (par) eval: runtime: 1m23s, gctime: 7.3s, systime: 0.81411s.
apply colour (par) real: 50.6s
apply colour (par) size: 625527
check colour eval: runtime: 1.1s, gctime: 0.10143s, systime: 0.01400s.
check colour real: 1.2s
check colour size: 625759
word_to_stack eval: runtime: 1m01s, gctime: 1.7s, systime: 0.24052s.
word_to_stack real: 1m01s
word_to_stack size: 511058
stack_rawcall eval: runtime: 36.0s, gctime: 1.0s, systime: 0.17168s.
stack_rawcall real: 36.2s
stack_rawcall size: 504423
stack_alloc (par) eval: runtime: 47.9s, gctime: 0.62748s, systime: 0.22042s.
stack_alloc (par) real: 22.6s
stack_alloc (par) size: 506070
expand stack_remove_def eval: runtime: 0.03374s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.03381s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 1m04s, gctime: 1.9s, systime: 0.30841s.
stack_remove (par) real: 35.6s
stack_remove (par) size: 864239
stack_names (par) eval: runtime: 36.7s, gctime: 3.8s, systime: 0.65145s.
stack_names (par) real: 19.4s
stack_names (par) size: 891944
stack_to_lab (par) eval: runtime: 1m08s, gctime: 1.2s, systime: 0.12481s.
stack_to_lab (par) real: 32.0s
stack_to_lab (par) size: 1085176
lab_to_target eval: runtime: 3m20s, gctime: 5.0s, systime: 0.57978s.
lab_to_target real: 3m21s
lab_to_target size: 1742975
export: runtime: 0.46518s, gctime: 0.05054s, systime: 0.03695s.
Saved theorem _____ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 13m03s to build
cc cat.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o -o cake_cat
cc diff.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o -o cake_diff
cc echo.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o -o cake_echo
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "grepCompile">>
to_flat eval: runtime: 14.7s, gctime: 0.67592s, systime: 0.16266s.
to_flat real: 14.9s
to_flat size: 316098
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 2.6s, gctime: 0.23480s, systime: 0.02397s.
to_clos real: 2.6s
to_clos size: 150578
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 14.8s, gctime: 0.55652s, systime: 0.03485s.
to_bvl real: 14.8s
to_bvl size: 268774
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m33s, gctime: 1.2s, systime: 0.08180s.
to_bvi real: 1m33s
to_bvi size: 238174
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 27.9s, gctime: 1.6s, systime: 0.13877s.
to_data real: 28.1s
to_data size: 444515
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 1m04s, gctime: 3.2s, systime: 0.21161s.
data_to_word real: 1m04s
data_to_word size: 1269032
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 13m07s, gctime: 1m17s, systime: 10.2s.
inst,ssa,two-reg (par) real: 9m02s
inst,ssa,two-reg (par) size: 4751385
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 39.5s, gctime: 3.9s, systime: 0.43718s.
get_clash (par) real: 14.2s
get_clash (par) size: 7257967
external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75 coalesceable: 61 coalesced: 53
1 moves: 24 coalesceable: 22 coalesced: 20
2 moves: 90 coalesceable: 68 coalesced: 53
3 moves: 25 coalesceable: 19 coalesced: 17
4 moves: 16 coalesceable: 15 coalesced: 12
5 moves: 148 coalesceable: 116 coalesced: 110
6 moves: 7 coalesceable: 7 coalesced: 7
7 moves: 7 coalesceable: 7 coalesced: 7
8 moves: 7 coalesceable: 7 coalesced: 7
9 moves: 7 coalesceable: 7 coalesced: 7
10 moves: 7 coalesceable: 7 coalesced: 7
11 moves: 19 coalesceable: 17 coalesced: 12
12 moves: 47 coalesceable: 41 coalesced: 37
13 moves: 31 coalesceable: 20 coalesced: 17
14 moves: 58 coalesceable: 48 coalesced: 42
15 moves: 0 coalesceable: 0 coalesced: 0
16 moves: 10 coalesceable: 8 coalesced: 5
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 21 coalesceable: 20 coalesced: 20
19 moves: 22 coalesceable: 21 coalesced: 20
20 moves: 19 coalesceable: 15 coalesced: 15
21 moves: 35 coalesceable: 29 coalesced: 25
22 moves: 40 coalesceable: 34 coalesced: 33
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 19 coalesceable: 17 coalesced: 15
25 moves: 42 coalesceable: 38 coalesced: 29
26 moves: 20 coalesceable: 20 coalesced: 14
27 moves: 20 coalesceable: 20 coalesced: 10
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 316 coalesceable: 269 coalesced: 269
31 moves: 26 coalesceable: 23 coalesced: 23
32 moves: 24 coalesceable: 23 coalesced: 23
33 moves: 16 coalesceable: 15 coalesced: 15
34 moves: 22 coalesceable: 19 coalesced: 19
35 moves: 90 coalesceable: 81 coalesced: 81
36 moves: 85 coalesceable: 82 coalesced: 82
37 moves: 65 coalesceable: 62 coalesced: 62
38 moves: 88 coalesceable: 85 coalesced: 85
39 moves: 29 coalesceable: 26 coalesced: 26
40 moves: 48 coalesceable: 45 coalesced: 45
41 moves: 7 coalesceable: 6 coalesced: 6
42 moves: 22 coalesceable: 19 coalesced: 19
43 moves: 12 coalesceable: 11 coalesced: 11
44 moves: 21 coalesceable: 18 coalesced: 18
45 moves: 51 coalesceable: 48 coalesced: 48
46 moves: 8 coalesceable: 7 coalesced: 7
47 moves: 11 coalesceable: 10 coalesced: 10
48 moves: 22 coalesceable: 19 coalesced: 19
49 moves: 26 coalesceable: 23 coalesced: 23
50 moves: 15 coalesceable: 14 coalesced: 14
51 moves: 20 coalesceable: 17 coalesced: 17
52 moves: 24 coalesceable: 21 coalesced: 21
53 moves: 190 coalesceable: 117 coalesced: 103
54 moves: 92 coalesceable: 65 coalesced: 51
55 moves: 41 coalesceable: 26 coalesced: 25
56 moves: 35 coalesceable: 26 coalesced: 21
57 moves: 56 coalesceable: 42 coalesced: 36
58 moves: 71 coalesceable: 46 coalesced: 40
59 moves: 48 coalesceable: 37 coalesced: 32
60 moves: 71 coalesceable: 46 coalesced: 38
61 moves: 927 coalesceable: 603 coalesced: 410
62 moves: 1088 coalesceable: 687 coalesced: 404
63 moves: 1169 coalesceable: 725 coalesced: 434
64 moves: 1254 coalesceable: 765 coalesced: 434
65 moves: 1343 coalesceable: 807 coalesced: 407
66 moves: 1436 coalesceable: 851 coalesced: 420
67 moves: 1533 coalesceable: 897 coalesced: 459
68 moves: 1634 coalesceable: 943 coalesced: 482
69 moves: 1739 coalesceable: 989 coalesced: 504
70 moves: 1848 coalesceable: 1035 coalesced: 506
71 moves: 17 coalesceable: 15 coalesced: 15
72 moves: 19 coalesceable: 17 coalesced: 17
73 moves: 21 coalesceable: 18 coalesced: 17
74 moves: 21 coalesceable: 19 coalesced: 19
75 moves: 23 coalesceable: 20 coalesced: 19
76 moves: 25 coalesceable: 21 coalesced: 20
77 moves: 23 coalesceable: 21 coalesced: 21
78 moves: 25 coalesceable: 22 coalesced: 21
79 moves: 27 coalesceable: 23 coalesced: 22
80 moves: 29 coalesceable: 24 coalesced: 23
81 moves: 25 coalesceable: 23 coalesced: 19
82 moves: 27 coalesceable: 24 coalesced: 20
83 moves: 29 coalesceable: 25 coalesced: 21
84 moves: 31 coalesceable: 26 coalesced: 22
85 moves: 33 coalesceable: 27 coalesced: 23
86 moves: 27 coalesceable: 24 coalesced: 21
87 moves: 29 coalesceable: 25 coalesced: 22
88 moves: 31 coalesceable: 26 coalesced: 23
89 moves: 33 coalesceable: 27 coalesced: 24
90 moves: 35 coalesceable: 28 coalesced: 25
91 moves: 37 coalesceable: 29 coalesced: 26
92 moves: 29 coalesceable: 25 coalesced: 16
93 moves: 31 coalesceable: 26 coalesced: 18
94 moves: 33 coalesceable: 27 coalesced: 23
95 moves: 35 coalesceable: 28 coalesced: 21
96 moves: 37 coalesceable: 29 coalesced: 22
97 moves: 39 coalesceable: 30 coalesced: 23
98 moves: 41 coalesceable: 31 coalesced: 24
99 moves: 31 coalesceable: 25 coalesced: 12
100 moves: 33 coalesceable: 27 coalesced: 9
101 moves: 35 coalesceable: 28 coalesced: 16
102 moves: 37 coalesceable: 29 coalesced: 23
103 moves: 39 coalesceable: 30 coalesced: 23
104 moves: 41 coalesceable: 31 coalesced: 21
105 moves: 43 coalesceable: 32 coalesced: 22
106 moves: 45 coalesceable: 33 coalesced: 25
107 moves: 33 coalesceable: 25 coalesced: 14
108 moves: 35 coalesceable: 27 coalesced: 10
109 moves: 37 coalesceable: 29 coalesced: 11
110 moves: 39 coalesceable: 30 coalesced: 14
111 moves: 41 coalesceable: 31 coalesced: 21
112 moves: 43 coalesceable: 32 coalesced: 23
113 moves: 45 coalesceable: 33 coalesced: 23
114 moves: 47 coalesceable: 34 coalesced: 23
115 moves: 49 coalesceable: 35 coalesced: 25
116 moves: 62 coalesceable: 11 coalesced: 7
117 moves: 200 coalesceable: 2 coalesced: 2
118 moves: 1002 coalesceable: 2 coalesced: 2
119 moves: 17 coalesceable: 11 coalesced: 11
120 moves: 17 coalesceable: 11 coalesced: 11
121 moves: 17 coalesceable: 11 coalesced: 11
122 moves: 17 coalesceable: 11 coalesced: 11
123 moves: 17 coalesceable: 11 coalesced: 11
124 moves: 17 coalesceable: 11 coalesced: 11
125 moves: 17 coalesceable: 11 coalesced: 11
126 moves: 17 coalesceable: 11 coalesced: 11
127 moves: 17 coalesceable: 11 coalesced: 11
128 moves: 17 coalesceable: 11 coalesced: 11
129 moves: 17 coalesceable: 11 coalesced: 11
130 moves: 17 coalesceable: 11 coalesced: 11
131 moves: 17 coalesceable: 11 coalesced: 11
132 moves: 17 coalesceable: 11 coalesced: 11
133 moves: 17 coalesceable: 11 coalesced: 11
134 moves: 17 coalesceable: 11 coalesced: 11
135 moves: 17 coalesceable: 11 coalesced: 11
136 moves: 17 coalesceable: 11 coalesced: 11
137 moves: 17 coalesceable: 11 coalesced: 11
138 moves: 17 coalesceable: 11 coalesced: 11
139 moves: 17 coalesceable: 11 coalesced: 11
140 moves: 17 coalesceable: 11 coalesced: 11
141 moves: 17 coalesceable: 11 coalesced: 11
142 moves: 17 coalesceable: 11 coalesced: 11
143 moves: 17 coalesceable: 11 coalesced: 11
144 moves: 17 coalesceable: 11 coalesced: 11
145 moves: 17 coalesceable: 11 coalesced: 11
146 moves: 17 coalesceable: 11 coalesced: 11
147 moves: 17 coalesceable: 11 coalesced: 11
148 moves: 17 coalesceable: 11 coalesced: 11
149 moves: 17 coalesceable: 11 coalesced: 11
150 moves: 17 coalesceable: 11 coalesced: 11
151 moves: 17 coalesceable: 11 coalesced: 11
152 moves: 17 coalesceable: 11 coalesced: 11
153 moves: 17 coalesceable: 11 coalesced: 11
154 moves: 17 coalesceable: 11 coalesced: 11
155 moves: 17 coalesceable: 11 coalesced: 11
156 moves: 17 coalesceable: 11 coalesced: 11
157 moves: 17 coalesceable: 11 coalesced: 11
158 moves: 17 coalesceable: 11 coalesced: 11
159 moves: 4375 coalesceable: 2573 coalesced: 2573
160 moves: 17 coalesceable: 11 coalesced: 11
161 moves: 17 coalesceable: 11 coalesced: 11
162 moves: 17 coalesceable: 11 coalesced: 11
163 moves: 17 coalesceable: 11 coalesced: 11
164 moves: 17 coalesceable: 11 coalesced: 11
165 moves: 17 coalesceable: 11 coalesced: 11
166 moves: 17 coalesceable: 11 coalesced: 11
167 moves: 17 coalesceable: 11 coalesced: 11
168 moves: 17 coalesceable: 11 coalesced: 11
169 moves: 17 coalesceable: 11 coalesced: 11
170 moves: 17 coalesceable: 11 coalesced: 11
171 moves: 17 coalesceable: 11 coalesced: 11
172 moves: 17 coalesceable: 11 coalesced: 11
173 moves: 17 coalesceable: 11 coalesced: 11
174 moves: 17 coalesceable: 11 coalesced: 11
175 moves: 17 coalesceable: 11 coalesced: 11
176 moves: 17 coalesceable: 11 coalesced: 11
177 moves: 17 coalesceable: 11 coalesced: 11
178 moves: 10 coalesceable: 6 coalesced: 6
179 moves: 60 coalesceable: 41 coalesced: 40
180 moves: 60 coalesceable: 41 coalesced: 40
181 moves: 17 coalesceable: 11 coalesced: 11
182 moves: 17 coalesceable: 11 coalesced: 11
183 moves: 17 coalesceable: 11 coalesced: 11
184 moves: 17 coalesceable: 11 coalesced: 11
185 moves: 17 coalesceable: 11 coalesced: 11
186 moves: 17 coalesceable: 11 coalesced: 11
187 moves: 17 coalesceable: 11 coalesced: 11
188 moves: 17 coalesceable: 11 coalesced: 11
189 moves: 17 coalesceable: 11 coalesced: 11
190 moves: 17 coalesceable: 11 coalesced: 11
191 moves: 2 coalesceable: 2 coalesced: 2
192 moves: 17 coalesceable: 11 coalesced: 11
193 moves: 573 coalesceable: 374 coalesced: 314
194 moves: 2 coalesceable: 2 coalesced: 2
195 moves: 17 coalesceable: 11 coalesced: 11
196 moves: 17 coalesceable: 11 coalesced: 11
197 moves: 17 coalesceable: 11 coalesced: 11
198 moves: 17 coalesceable: 11 coalesced: 11
199 moves: 2 coalesceable: 2 coalesced: 2
200 moves: 2 coalesceable: 2 coalesced: 2
201 moves: 17 coalesceable: 11 coalesced: 11
202 moves: 17 coalesceable: 11 coalesced: 11
203 moves: 17 coalesceable: 11 coalesced: 11
204 moves: 17 coalesceable: 11 coalesced: 11
205 moves: 17 coalesceable: 11 coalesced: 11
206 moves: 17 coalesceable: 11 coalesced: 11
207 moves: 2 coalesceable: 2 coalesced: 2
208 moves: 17 coalesceable: 11 coalesced: 11
209 moves: 17 coalesceable: 11 coalesced: 11
210 moves: 17 coalesceable: 11 coalesced: 11
211 moves: 17 coalesceable: 11 coalesced: 11
212 moves: 17 coalesceable: 11 coalesced: 11
213 moves: 17 coalesceable: 11 coalesced: 11
214 moves: 17 coalesceable: 11 coalesced: 11
215 moves: 17 coalesceable: 11 coalesced: 11
216 moves: 17 coalesceable: 11 coalesced: 11
217 moves: 17 coalesceable: 11 coalesced: 11
218 moves: 17 coalesceable: 11 coalesced: 11
219 moves: 17 coalesceable: 11 coalesced: 11
220 moves: 17 coalesceable: 11 coalesced: 11
221 moves: 51 coalesceable: 31 coalesced: 31
222 moves: 17 coalesceable: 11 coalesced: 11
223 moves: 17 coalesceable: 11 coalesced: 11
224 moves: 17 coalesceable: 11 coalesced: 11
225 moves: 17 coalesceable: 11 coalesced: 11
226 moves: 17 coalesceable: 11 coalesced: 11
227 moves: 16 coalesceable: 11 coalesced: 11
228 moves: 17 coalesceable: 11 coalesced: 11
229 moves: 17 coalesceable: 11 coalesced: 11
230 moves: 24 coalesceable: 16 coalesced: 16
231 moves: 17 coalesceable: 11 coalesced: 11
232 moves: 17 coalesceable: 11 coalesced: 11
233 moves: 17 coalesceable: 11 coalesced: 11
234 moves: 17 coalesceable: 11 coalesced: 11
235 moves: 17 coalesceable: 11 coalesced: 11
236 moves: 17 coalesceable: 11 coalesced: 11
237 moves: 17 coalesceable: 11 coalesced: 11
238 moves: 17 coalesceable: 11 coalesced: 11
239 moves: 17 coalesceable: 11 coalesced: 11
240 moves: 17 coalesceable: 11 coalesced: 11
241 moves: 2312 coalesceable: 1286 coalesced: 1286
242 moves: 17 coalesceable: 11 coalesced: 11
243 moves: 17 coalesceable: 11 coalesced: 11
244 moves: 17 coalesceable: 11 coalesced: 11
245 moves: 17 coalesceable: 11 coalesced: 11
246 moves: 17 coalesceable: 11 coalesced: 11
247 moves: 74 coalesceable: 49 coalesced: 43
248 moves: 17 coalesceable: 11 coalesced: 11
249 moves: 17 coalesceable: 11 coalesced: 11
250 moves: 17 coalesceable: 11 coalesced: 11
251 moves: 17 coalesceable: 11 coalesced: 11
252 moves: 17 coalesceable: 11 coalesced: 11
253 moves: 17 coalesceable: 11 coalesced: 11
254 moves: 17 coalesceable: 11 coalesced: 11
255 moves: 17 coalesceable: 11 coalesced: 11
256 moves: 17 coalesceable: 11 coalesced: 11
257 moves: 17 coalesceable: 11 coalesced: 11
258 moves: 17 coalesceable: 11 coalesced: 11
259 moves: 17 coalesceable: 11 coalesced: 11
260 moves: 17 coalesceable: 11 coalesced: 11
261 moves: 17 coalesceable: 11 coalesced: 11
262 moves: 5885 coalesceable: 3532 coalesced: 3033
263 moves: 11474 coalesceable: 7187 coalesced: 6357
264 moves: 10448 coalesceable: 6311 coalesced: 5527
265 moves: 17 coalesceable: 11 coalesced: 11
266 moves: 17 coalesceable: 11 coalesced: 11
267 moves: 17 coalesceable: 11 coalesced: 11
268 moves: 17 coalesceable: 11 coalesced: 11
269 moves: 17 coalesceable: 11 coalesced: 11
270 moves: 17 coalesceable: 11 coalesced: 11
271 moves: 17 coalesceable: 11 coalesced: 11
272 moves: 17 coalesceable: 11 coalesced: 11
273 moves: 17 coalesceable: 11 coalesced: 11
274 moves: 17 coalesceable: 11 coalesced: 11
275 moves: 17 coalesceable: 11 coalesced: 11
276 moves: 102 coalesceable: 58 coalesced: 58
277 moves: 17 coalesceable: 11 coalesced: 11
278 moves: 17 coalesceable: 11 coalesced: 11
279 moves: 17 coalesceable: 11 coalesced: 11
280 moves: 17 coalesceable: 11 coalesced: 11
281 moves: 17 coalesceable: 11 coalesced: 11
282 moves: 17 coalesceable: 11 coalesced: 11
283 moves: 1828 coalesceable: 1001 coalesced: 913
284 moves: 17 coalesceable: 11 coalesced: 11
285 moves: 17 coalesceable: 11 coalesced: 11
286 moves: 17 coalesceable: 11 coalesced: 11
287 moves: 17 coalesceable: 11 coalesced: 11
288 moves: 17 coalesceable: 11 coalesced: 11
289 moves: 158 coalesceable: 117 coalesced: 117
290 moves: 17 coalesceable: 11 coalesced: 11
291 moves: 17 coalesceable: 11 coalesced: 11
292 moves: 17 coalesceable: 11 coalesced: 11
293 moves: 17 coalesceable: 11 coalesced: 11
294 moves: 5 coalesceable: 3 coalesced: 3
295 moves: 4 coalesceable: 4 coalesced: 4
296 moves: 6 coalesceable: 6 coalesced: 6
297 moves: 4 coalesceable: 4 coalesced: 4
298 moves: 6 coalesceable: 6 coalesced: 6
299 moves: 8 coalesceable: 8 coalesced: 8
300 moves: 46 coalesceable: 34 coalesced: 33
301 moves: 4 coalesceable: 4 coalesced: 4
302 moves: 3 coalesceable: 3 coalesced: 3
303 moves: 6 coalesceable: 6 coalesced: 6
304 moves: 3 coalesceable: 3 coalesced: 2
305 moves: 8 coalesceable: 8 coalesced: 8
306 moves: 99 coalesceable: 63 coalesced: 50
307 moves: 6 coalesceable: 6 coalesced: 6
308 moves: 7 coalesceable: 7 coalesced: 4
309 moves: 6 coalesceable: 6 coalesced: 6
310 moves: 29 coalesceable: 19 coalesced: 13
311 moves: 8 coalesceable: 8 coalesced: 8
312 moves: 103 coalesceable: 64 coalesced: 59
313 moves: 4 coalesceable: 4 coalesced: 4
314 moves: 7 coalesceable: 7 coalesced: 7
315 moves: 6 coalesceable: 6 coalesced: 6
316 moves: 49 coalesceable: 36 coalesced: 34
317 moves: 6 coalesceable: 6 coalesced: 6
318 moves: 32 coalesceable: 23 coalesced: 18
319 moves: 4 coalesceable: 4 coalesced: 4
320 moves: 5 coalesceable: 5 coalesced: 3
321 moves: 4 coalesceable: 4 coalesced: 4
322 moves: 7 coalesceable: 7 coalesced: 7
323 moves: 6 coalesceable: 6 coalesced: 6
324 moves: 86 coalesceable: 57 coalesced: 51
325 moves: 6 coalesceable: 6 coalesced: 6
326 moves: 76 coalesceable: 47 coalesced: 43
327 moves: 6 coalesceable: 6 coalesced: 6
328 moves: 42 coalesceable: 27 coalesced: 25
329 moves: 8 coalesceable: 8 coalesced: 8
330 moves: 52 coalesceable: 37 coalesced: 31
331 moves: 4 coalesceable: 4 coalesced: 4
332 moves: 95 coalesceable: 58 coalesced: 57
333 moves: 6 coalesceable: 6 coalesced: 6
334 moves: 49 coalesceable: 37 coalesced: 35
335 moves: 4 coalesceable: 4 coalesced: 4
336 moves: 73 coalesceable: 49 coalesced: 47
337 moves: 6 coalesceable: 6 coalesced: 6
338 moves: 79 coalesceable: 57 coalesced: 54
339 moves: 6 coalesceable: 6 coalesced: 6
340 moves: 42 coalesceable: 27 coalesced: 26
341 moves: 4 coalesceable: 4 coalesced: 4
342 moves: 12 coalesceable: 11 coalesced: 9
343 moves: 4 coalesceable: 4 coalesced: 4
344 moves: 9 coalesceable: 9 coalesced: 8
345 moves: 4 coalesceable: 4 coalesced: 4
346 moves: 29 coalesceable: 12 coalesced: 11
347 moves: 8 coalesceable: 8 coalesced: 8
348 moves: 124 coalesceable: 72 coalesced: 58
349 moves: 6 coalesceable: 6 coalesced: 6
350 moves: 62 coalesceable: 31 coalesced: 29
351 moves: 4 coalesceable: 4 coalesced: 4
352 moves: 48 coalesceable: 23 coalesced: 21
353 moves: 6 coalesceable: 6 coalesced: 6
354 moves: 23 coalesceable: 15 coalesced: 11
355 moves: 6 coalesceable: 6 coalesced: 6
356 moves: 23 coalesceable: 15 coalesced: 11
357 moves: 6 coalesceable: 6 coalesced: 6
358 moves: 30 coalesceable: 19 coalesced: 16
359 moves: 6 coalesceable: 6 coalesced: 6
360 moves: 29 coalesceable: 21 coalesced: 17
361 moves: 6 coalesceable: 6 coalesced: 6
362 moves: 24 coalesceable: 16 coalesced: 13
363 moves: 6 coalesceable: 6 coalesced: 6
364 moves: 24 coalesceable: 16 coalesced: 13
365 moves: 6 coalesceable: 6 coalesced: 6
366 moves: 30 coalesceable: 22 coalesced: 19
367 moves: 6 coalesceable: 6 coalesced: 6
368 moves: 60 coalesceable: 44 coalesced: 41
369 moves: 6 coalesceable: 6 coalesced: 6
370 moves: 62 coalesceable: 31 coalesced: 29
371 moves: 4 coalesceable: 4 coalesced: 4
372 moves: 3 coalesceable: 3 coalesced: 3
373 moves: 4 coalesceable: 4 coalesced: 4
374 moves: 43 coalesceable: 29 coalesced: 25
375 moves: 4 coalesceable: 4 coalesced: 4
376 moves: 25 coalesceable: 18 coalesced: 16
377 moves: 4 coalesceable: 4 coalesced: 4
378 moves: 3 coalesceable: 3 coalesced: 3
379 moves: 6 coalesceable: 6 coalesced: 6
380 moves: 36 coalesceable: 23 coalesced: 17
381 moves: 6 coalesceable: 6 coalesced: 6
382 moves: 21 coalesceable: 19 coalesced: 19
383 moves: 4 coalesceable: 4 coalesced: 4
384 moves: 9 coalesceable: 9 coalesced: 8
385 moves: 8 coalesceable: 8 coalesced: 8
386 moves: 22 coalesceable: 20 coalesced: 20
387 moves: 12 coalesceable: 12 coalesced: 12
388 moves: 218 coalesceable: 134 coalesced: 94
389 moves: 12 coalesceable: 12 coalesced: 12
390 moves: 218 coalesceable: 134 coalesced: 94
391 moves: 8 coalesceable: 8 coalesced: 8
392 moves: 124 coalesceable: 72 coalesced: 58
393 moves: 4 coalesceable: 4 coalesced: 4
394 moves: 77 coalesceable: 56 coalesced: 53
395 moves: 6 coalesceable: 6 coalesced: 6
396 moves: 110 coalesceable: 79 coalesced: 69
397 moves: 8 coalesceable: 8 coalesced: 8
398 moves: 407 coalesceable: 208 coalesced: 175
399 moves: 4 coalesceable: 4 coalesced: 4
400 moves: 56 coalesceable: 33 coalesced: 30
401 moves: 4 coalesceable: 4 coalesced: 4
402 moves: 8 coalesceable: 6 coalesced: 6
403 moves: 8 coalesceable: 8 coalesced: 8
404 moves: 163 coalesceable: 110 coalesced: 96
405 moves: 6 coalesceable: 6 coalesced: 6
406 moves: 114 coalesceable: 80 coalesced: 72
407 moves: 4 coalesceable: 4 coalesced: 4
408 moves: 6 coalesceable: 6 coalesced: 6
409 moves: 4 coalesceable: 4 coalesced: 4
410 moves: 6 coalesceable: 6 coalesced: 6
411 moves: 8 coalesceable: 8 coalesced: 8
412 moves: 128 coalesceable: 77 coalesced: 70
413 moves: 8 coalesceable: 8 coalesced: 8
414 moves: 111 coalesceable: 66 coalesced: 51
415 moves: 6 coalesceable: 6 coalesced: 6
416 moves: 427 coalesceable: 263 coalesced: 198
417 moves: 4 coalesceable: 4 coalesced: 4
418 moves: 5 coalesceable: 5 coalesced: 5
419 moves: 4 coalesceable: 4 coalesced: 4
420 moves: 272 coalesceable: 139 coalesced: 131
421 moves: 4 coalesceable: 4 coalesced: 4
422 moves: 69 coalesceable: 54 coalesced: 54
423 moves: 6 coalesceable: 6 coalesced: 6
424 moves: 78 coalesceable: 59 coalesced: 56
425 moves: 4 coalesceable: 4 coalesced: 4
426 moves: 21 coalesceable: 18 coalesced: 16
427 moves: 4 coalesceable: 4 coalesced: 4
428 moves: 164 coalesceable: 106 coalesced: 89
429 moves: 224 coalesceable: 137 coalesced: 113
430 moves: 217 coalesceable: 133 coalesced: 108
431 moves: 4 coalesceable: 4 coalesced: 4
432 moves: 45 coalesceable: 26 coalesced: 24
433 moves: 6 coalesceable: 6 coalesced: 6
434 moves: 152 coalesceable: 102 coalesced: 97
435 moves: 6 coalesceable: 6 coalesced: 6
436 moves: 847 coalesceable: 556 coalesced: 502
437 moves: 6 coalesceable: 6 coalesced: 6
438 moves: 30 coalesceable: 21 coalesced: 16
439 moves: 4 coalesceable: 4 coalesced: 4
440 moves: 7 coalesceable: 7 coalesced: 7
441 moves: 6 coalesceable: 6 coalesced: 6
442 moves: 30 coalesceable: 17 coalesced: 16
443 moves: 10 coalesceable: 10 coalesced: 10
444 moves: 2844 coalesceable: 1470 coalesced: 781
445 moves: 10 coalesceable: 10 coalesced: 10
446 moves: 2803 coalesceable: 1454 coalesced: 770
447 moves: 4 coalesceable: 4 coalesced: 4
448 moves: 150 coalesceable: 86 coalesced: 76
449 moves: 4 coalesceable: 4 coalesced: 4
450 moves: 4 coalesceable: 4 coalesced: 4
451 moves: 8 coalesceable: 8 coalesced: 8
452 moves: 99 coalesceable: 63 coalesced: 57
453 moves: 8 coalesceable: 8 coalesced: 8
454 moves: 72 coalesceable: 48 coalesced: 44
455 moves: 10 coalesceable: 10 coalesced: 10
456 moves: 195 coalesceable: 104 coalesced: 68
457 moves: 8 coalesceable: 8 coalesced: 8
458 moves: 74 coalesceable: 47 coalesced: 43
459 moves: 6 coalesceable: 6 coalesced: 6
460 moves: 58 coalesceable: 40 coalesced: 33
461 moves: 6 coalesceable: 6 coalesced: 6
462 moves: 634 coalesceable: 440 coalesced: 316
463 moves: 6 coalesceable: 6 coalesced: 6
464 moves: 15 coalesceable: 15 coalesced: 15
465 moves: 4 coalesceable: 4 coalesced: 4
466 moves: 321 coalesceable: 204 coalesced: 200
467 moves: 8 coalesceable: 8 coalesced: 8
468 moves: 107 coalesceable: 65 coalesced: 65
469 moves: 10 coalesceable: 10 coalesced: 10
470 moves: 514 coalesceable: 292 coalesced: 271
471 moves: 4 coalesceable: 4 coalesced: 4
472 moves: 26 coalesceable: 19 coalesced: 17
473 moves: 8 coalesceable: 8 coalesced: 8
474 moves: 256 coalesceable: 149 coalesced: 130
475 moves: 8 coalesceable: 8 coalesced: 8
476 moves: 789 coalesceable: 475 coalesced: 427
477 moves: 6 coalesceable: 6 coalesced: 6
478 moves: 37 coalesceable: 23 coalesced: 22
479 moves: 4 coalesceable: 4 coalesced: 4
480 moves: 201 coalesceable: 119 coalesced: 113
481 moves: 6 coalesceable: 6 coalesced: 6
482 moves: 220 coalesceable: 158 coalesced: 129
483 moves: 4 coalesceable: 4 coalesced: 4
484 moves: 477 coalesceable: 295 coalesced: 290
485 moves: 6 coalesceable: 6 coalesced: 6
486 moves: 16 coalesceable: 9 coalesced: 6
487 moves: 6 coalesceable: 6 coalesced: 6
488 moves: 42 coalesceable: 26 coalesced: 25
489 moves: 4 coalesceable: 4 coalesced: 4
490 moves: 208 coalesceable: 121 coalesced: 117
491 moves: 4 coalesceable: 4 coalesced: 4
492 moves: 419 coalesceable: 260 coalesced: 230
493 moves: 4 coalesceable: 4 coalesced: 4
494 moves: 21 coalesceable: 14 coalesced: 13
495 moves: 6 coalesceable: 6 coalesced: 6
496 moves: 188 coalesceable: 117 coalesced: 112
497 moves: 6 coalesceable: 6 coalesced: 6
498 moves: 161 coalesceable: 117 coalesced: 95
499 moves: 4 coalesceable: 4 coalesced: 4
500 moves: 156 coalesceable: 103 coalesced: 98
501 moves: 4 coalesceable: 4 coalesced: 4
502 moves: 138 coalesceable: 92 coalesced: 88
503 moves: 4 coalesceable: 4 coalesced: 4
504 moves: 4 coalesceable: 4 coalesced: 4
505 moves: 4 coalesceable: 4 coalesced: 4
506 moves: 100 coalesceable: 64 coalesced: 61
507 moves: 6 coalesceable: 6 coalesced: 6
508 moves: 7 coalesceable: 7 coalesced: 7
509 moves: 10 coalesceable: 10 coalesced: 10
510 moves: 70 coalesceable: 61 coalesced: 55
511 moves: 4 coalesceable: 4 coalesced: 4
512 moves: 174 coalesceable: 110 coalesced: 105
513 moves: 4 coalesceable: 4 coalesced: 4
514 moves: 23 coalesceable: 15 coalesced: 14
515 moves: 9 coalesceable: 9 coalesced: 9
516 moves: 6 coalesceable: 6 coalesced: 6
517 moves: 232 coalesceable: 126 coalesced: 117
518 moves: 37 coalesceable: 23 coalesced: 20
519 moves: 4 coalesceable: 4 coalesced: 4
520 moves: 25 coalesceable: 16 coalesced: 14
521 moves: 10 coalesceable: 10 coalesced: 10
522 moves: 224 coalesceable: 128 coalesced: 94
523 moves: 8 coalesceable: 8 coalesced: 8
524 moves: 282 coalesceable: 163 coalesced: 151
525 moves: 6 coalesceable: 6 coalesced: 6
526 moves: 8 coalesceable: 8 coalesced: 6
527 moves: 6 coalesceable: 6 coalesced: 6
528 moves: 11 coalesceable: 11 coalesced: 9
529 moves: 10 coalesceable: 10 coalesced: 10
530 moves: 405 coalesceable: 209 coalesced: 162
531 moves: 10 coalesceable: 10 coalesced: 10
532 moves: 1186 coalesceable: 706 coalesced: 410
533 moves: 10 coalesceable: 10 coalesced: 10
534 moves: 96 coalesceable: 62 coalesced: 53
535 moves: 6 coalesceable: 6 coalesced: 6
536 moves: 24 coalesceable: 16 coalesced: 13
537 moves: 4 coalesceable: 4 coalesced: 4
538 moves: 36 coalesceable: 24 coalesced: 23
539 moves: 6 coalesceable: 6 coalesced: 6
540 moves: 24 coalesceable: 16 coalesced: 13
541 moves: 4 coalesceable: 4 coalesced: 4
542 moves: 147 coalesceable: 73 coalesced: 54
543 moves: 4 coalesceable: 4 coalesced: 4
544 moves: 89 coalesceable: 54 coalesced: 47
545 moves: 4 coalesceable: 4 coalesced: 4
546 moves: 22 coalesceable: 14 coalesced: 13
547 moves: 6 coalesceable: 6 coalesced: 6
548 moves: 40 coalesceable: 23 coalesced: 19
549 moves: 8 coalesceable: 8 coalesced: 8
550 moves: 64 coalesceable: 35 coalesced: 33
551 moves: 6 coalesceable: 6 coalesced: 6
552 moves: 24 coalesceable: 16 coalesced: 13
553 moves: 4 coalesceable: 4 coalesced: 4
554 moves: 59 coalesceable: 34 coalesced: 31
555 moves: 4 coalesceable: 4 coalesced: 4
556 moves: 252 coalesceable: 137 coalesced: 115
557 moves: 4 coalesceable: 4 coalesced: 4
558 moves: 18 coalesceable: 10 coalesced: 10
559 moves: 6 coalesceable: 6 coalesced: 6
560 moves: 148 coalesceable: 60 coalesced: 56
561 moves: 4 coalesceable: 4 coalesced: 4
562 moves: 6 coalesceable: 6 coalesced: 6
563 moves: 4 coalesceable: 4 coalesced: 4
564 moves: 6 coalesceable: 6 coalesced: 6
565 moves: 6 coalesceable: 6 coalesced: 6
566 moves: 86 coalesceable: 55 coalesced: 53
567 moves: 6 coalesceable: 6 coalesced: 6
568 moves: 77 coalesceable: 49 coalesced: 44
569 moves: 4 coalesceable: 4 coalesced: 4
570 moves: 21 coalesceable: 14 coalesced: 13
571 moves: 4 coalesceable: 4 coalesced: 4
572 moves: 21 coalesceable: 14 coalesced: 13
573 moves: 1595 coalesceable: 918 coalesced: 834
574 moves: 4 coalesceable: 4 coalesced: 4
575 moves: 10 coalesceable: 9 coalesced: 9
576 moves: 6 coalesceable: 6 coalesced: 6
577 moves: 40 coalesceable: 25 coalesced: 24
578 moves: 14 coalesceable: 14 coalesced: 14
579 moves: 79 coalesceable: 47 coalesced: 41
580 moves: 4 coalesceable: 4 coalesced: 4
581 moves: 18 coalesceable: 16 coalesced: 16
582 moves: 4 coalesceable: 4 coalesced: 4
583 moves: 158 coalesceable: 90 coalesced: 87
584 moves: 4 coalesceable: 4 coalesced: 4
585 moves: 111 coalesceable: 80 coalesced: 77
586 moves: 4 coalesceable: 4 coalesced: 4
587 moves: 30 coalesceable: 19 coalesced: 18
588 moves: 4 coalesceable: 4 coalesced: 4
589 moves: 17 coalesceable: 15 coalesced: 15
590 moves: 4 coalesceable: 4 coalesced: 4
591 moves: 12 coalesceable: 11 coalesced: 11
592 moves: 4 coalesceable: 4 coalesced: 4
593 moves: 69 coalesceable: 40 coalesced: 39
594 moves: 6 coalesceable: 6 coalesced: 6
595 moves: 3 coalesceable: 3 coalesced: 2
596 moves: 6 coalesceable: 6 coalesced: 6
597 moves: 37 coalesceable: 22 coalesced: 21
598 moves: 6 coalesceable: 6 coalesced: 6
599 moves: 3 coalesceable: 3 coalesced: 3
600 moves: 6 coalesceable: 6 coalesced: 6
601 moves: 37 coalesceable: 22 coalesced: 21
602 moves: 4 coalesceable: 4 coalesced: 4
603 moves: 55 coalesceable: 35 coalesced: 31
604 moves: 6 coalesceable: 6 coalesced: 6
605 moves: 23 coalesceable: 21 coalesced: 21
606 moves: 4 coalesceable: 4 coalesced: 4
607 moves: 25 coalesceable: 17 coalesced: 16
608 moves: 4 coalesceable: 4 coalesced: 4
609 moves: 77 coalesceable: 51 coalesced: 48
610 moves: 6 coalesceable: 6 coalesced: 6
611 moves: 20 coalesceable: 18 coalesced: 14
612 moves: 38 coalesceable: 25 coalesced: 24
613 moves: 79 coalesceable: 50 coalesced: 47
614 moves: 6 coalesceable: 6 coalesced: 6
615 moves: 85 coalesceable: 57 coalesced: 54
616 moves: 4 coalesceable: 4 coalesced: 4
617 moves: 40 coalesceable: 25 coalesced: 24
618 moves: 6 coalesceable: 6 coalesced: 6
619 moves: 26 coalesceable: 19 coalesced: 19
620 moves: 4 coalesceable: 4 coalesced: 4
621 moves: 21 coalesceable: 14 coalesced: 13
622 moves: 4 coalesceable: 4 coalesced: 4
623 moves: 53 coalesceable: 34 coalesced: 32
624 moves: 167 coalesceable: 107 coalesced: 107
625 moves: 37 coalesceable: 26 coalesced: 25
626 moves: 6 coalesceable: 6 coalesced: 6
627 moves: 34 coalesceable: 23 coalesced: 21
628 moves: 4 coalesceable: 4 coalesced: 4
629 moves: 5 coalesceable: 5 coalesced: 5
630 moves: 38 coalesceable: 25 coalesced: 24
631 moves: 110 coalesceable: 74 coalesced: 72
632 moves: 6 coalesceable: 6 coalesced: 6
633 moves: 34 coalesceable: 23 coalesced: 21
634 moves: 32 coalesceable: 22 coalesced: 22
635 moves: 102 coalesceable: 69 coalesced: 67
636 moves: 6 coalesceable: 6 coalesced: 6
637 moves: 34 coalesceable: 23 coalesced: 21
638 moves: 4 coalesceable: 4 coalesced: 4
639 moves: 5 coalesceable: 5 coalesced: 5
640 moves: 4 coalesceable: 4 coalesced: 4
641 moves: 21 coalesceable: 14 coalesced: 13
642 moves: 4 coalesceable: 4 coalesced: 4
643 moves: 132 coalesceable: 89 coalesced: 80
644 moves: 4 coalesceable: 4 coalesced: 4
645 moves: 88 coalesceable: 59 coalesced: 56
646 moves: 4 coalesceable: 4 coalesced: 4
647 moves: 29 coalesceable: 23 coalesced: 21
648 moves: 4 coalesceable: 4 coalesced: 4
649 moves: 49 coalesceable: 37 coalesced: 37
650 moves: 4 coalesceable: 4 coalesced: 4
651 moves: 5 coalesceable: 5 coalesced: 5
652 moves: 4 coalesceable: 4 coalesced: 4
653 moves: 49 coalesceable: 37 coalesced: 37
654 moves: 4 coalesceable: 4 coalesced: 4
655 moves: 5 coalesceable: 5 coalesced: 5
656 moves: 4 coalesceable: 4 coalesced: 4
657 moves: 5 coalesceable: 5 coalesced: 5
658 moves: 4 coalesceable: 4 coalesced: 4
659 moves: 5 coalesceable: 5 coalesced: 5
660 moves: 4 coalesceable: 4 coalesced: 4
661 moves: 5 coalesceable: 5 coalesced: 5
662 moves: 4 coalesceable: 4 coalesced: 4
663 moves: 5 coalesceable: 5 coalesced: 5
664 moves: 4 coalesceable: 4 coalesced: 4
665 moves: 5 coalesceable: 5 coalesced: 5
666 moves: 4 coalesceable: 4 coalesced: 4
667 moves: 51 coalesceable: 29 coalesced: 28
668 moves: 4 coalesceable: 4 coalesced: 4
669 moves: 108 coalesceable: 74 coalesced: 72
670 moves: 8 coalesceable: 8 coalesced: 8
671 moves: 99 coalesceable: 51 coalesced: 48
672 moves: 4 coalesceable: 4 coalesced: 4
673 moves: 266 coalesceable: 170 coalesced: 166
674 moves: 6 coalesceable: 6 coalesced: 6
675 moves: 503 coalesceable: 392 coalesced: 384
676 moves: 125 coalesceable: 50 coalesced: 45
677 moves: 4 coalesceable: 4 coalesced: 4
678 moves: 210 coalesceable: 128 coalesced: 124
679 moves: 6 coalesceable: 6 coalesced: 6
680 moves: 14 coalesceable: 12 coalesced: 12
681 moves: 6 coalesceable: 6 coalesced: 6
682 moves: 35 coalesceable: 25 coalesced: 22
683 moves: 38 coalesceable: 28 coalesced: 23
684 moves: 4 coalesceable: 4 coalesced: 4
685 moves: 302 coalesceable: 186 coalesced: 181
runtime: 6m22s, gctime: 5.0s, systime: 0.36490s.
external oracle real: 6m23s
external oracle size: 552987
apply colour (par) eval: runtime: 7m08s, gctime: 19.3s, systime: 2.6s.
apply colour (par) real: 2m31s
apply colour (par) size: 2110074
check colour eval: runtime: 20.9s, gctime: 5.1s, systime: 0.82880s.
check colour real: 21.8s
check colour size: 2110761
word_to_stack eval: runtime: 2m59s, gctime: 3.1s, systime: 0.48039s.
word_to_stack real: 3m00s
word_to_stack size: 1648117
stack_rawcall eval: runtime: 1m54s, gctime: 1.8s, systime: 0.19617s.
stack_rawcall real: 1m54s
stack_rawcall size: 1635100
stack_alloc (par) eval: runtime: 3m12s, gctime: 2.2s, systime: 0.35772s.
stack_alloc (par) real: 1m00s
stack_alloc (par) size: 1650958
expand stack_remove_def eval: runtime: 0.03610s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.03603s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 4m02s, gctime: 3.0s, systime: 0.53263s.
stack_remove (par) real: 1m05s
stack_remove (par) size: 2710987
stack_names (par) eval: runtime: 2m14s, gctime: 3.3s, systime: 0.35511s.
stack_names (par) real: 44.2s
stack_names (par) size: 2801809
stack_to_lab (par) eval: runtime: 5m03s, gctime: 31.3s, systime: 2.2s.
stack_to_lab (par) real: 1m55s
stack_to_lab (par) size: 3422428
lab_to_target eval: runtime: 8m05s, gctime: 19.3s, systime: 2.7s.
lab_to_target real: 8m08s
lab_to_target size: 5117408
export: runtime: 0.95898s, gctime: 0.26061s, systime: 0.02896s.
Saved theorem _____ "grep_compiled"
Exporting theory "grepCompile" ... done.
Theory "grepCompile" took 59m58s to build
cc grep.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o -o cake_grep
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "helloCompile">>
to_flat eval: runtime: 6.8s, gctime: 0.39318s, systime: 0.05387s.
to_flat real: 6.9s
to_flat size: 56823
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.23215s, gctime: 0.05153s, systime: 0.00597s.
to_clos real: 0.23857s
to_clos size: 33725
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 3.8s, gctime: 0.16997s, systime: 0.01102s.
to_bvl real: 3.8s
to_bvl size: 55296
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 32.8s, gctime: 0.47886s, systime: 0.04401s.
to_bvi real: 32.9s
to_bvi size: 63033
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 10.5s, gctime: 0.51793s, systime: 0.03697s.
to_data real: 10.6s
to_data size: 111238
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 14.4s, gctime: 0.61943s, systime: 0.04593s.
data_to_word real: 14.5s
data_to_word size: 296757
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 1m02s, gctime: 4.0s, systime: 0.31865s.
inst,ssa,two-reg (par) real: 33.7s
inst,ssa,two-reg (par) size: 1199208
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 12.8s, gctime: 6.7s, systime: 0.83254s.
get_clash (par) real: 10.1s
get_clash (par) size: 1867589
external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75 coalesceable: 61 coalesced: 53
1 moves: 24 coalesceable: 22 coalesced: 20
2 moves: 90 coalesceable: 68 coalesced: 53
3 moves: 25 coalesceable: 19 coalesced: 17
4 moves: 16 coalesceable: 15 coalesced: 12
5 moves: 148 coalesceable: 116 coalesced: 110
6 moves: 7 coalesceable: 7 coalesced: 7
7 moves: 7 coalesceable: 7 coalesced: 7
8 moves: 7 coalesceable: 7 coalesced: 7
9 moves: 7 coalesceable: 7 coalesced: 7
10 moves: 7 coalesceable: 7 coalesced: 7
11 moves: 19 coalesceable: 17 coalesced: 12
12 moves: 47 coalesceable: 41 coalesced: 37
13 moves: 31 coalesceable: 20 coalesced: 17
14 moves: 58 coalesceable: 48 coalesced: 42
15 moves: 0 coalesceable: 0 coalesced: 0
16 moves: 10 coalesceable: 8 coalesced: 5
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 21 coalesceable: 20 coalesced: 20
19 moves: 22 coalesceable: 21 coalesced: 20
20 moves: 19 coalesceable: 15 coalesced: 15
21 moves: 35 coalesceable: 29 coalesced: 25
22 moves: 40 coalesceable: 34 coalesced: 33
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 19 coalesceable: 17 coalesced: 15
25 moves: 42 coalesceable: 38 coalesced: 29
26 moves: 20 coalesceable: 20 coalesced: 14
27 moves: 20 coalesceable: 20 coalesced: 10
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 316 coalesceable: 269 coalesced: 269
31 moves: 26 coalesceable: 23 coalesced: 23
32 moves: 24 coalesceable: 23 coalesced: 23
33 moves: 16 coalesceable: 15 coalesced: 15
34 moves: 22 coalesceable: 19 coalesced: 19
35 moves: 90 coalesceable: 81 coalesced: 81
36 moves: 85 coalesceable: 82 coalesced: 82
37 moves: 65 coalesceable: 62 coalesced: 62
38 moves: 88 coalesceable: 85 coalesced: 85
39 moves: 29 coalesceable: 26 coalesced: 26
40 moves: 48 coalesceable: 45 coalesced: 45
41 moves: 7 coalesceable: 6 coalesced: 6
42 moves: 22 coalesceable: 19 coalesced: 19
43 moves: 12 coalesceable: 11 coalesced: 11
44 moves: 21 coalesceable: 18 coalesced: 18
45 moves: 51 coalesceable: 48 coalesced: 48
46 moves: 8 coalesceable: 7 coalesced: 7
47 moves: 11 coalesceable: 10 coalesced: 10
48 moves: 22 coalesceable: 19 coalesced: 19
49 moves: 26 coalesceable: 23 coalesced: 23
50 moves: 15 coalesceable: 14 coalesced: 14
51 moves: 20 coalesceable: 17 coalesced: 17
52 moves: 24 coalesceable: 21 coalesced: 21
53 moves: 190 coalesceable: 117 coalesced: 103
54 moves: 92 coalesceable: 65 coalesced: 51
55 moves: 41 coalesceable: 26 coalesced: 25
56 moves: 35 coalesceable: 26 coalesced: 21
57 moves: 56 coalesceable: 42 coalesced: 36
58 moves: 71 coalesceable: 46 coalesced: 40
59 moves: 48 coalesceable: 37 coalesced: 32
60 moves: 71 coalesceable: 46 coalesced: 38
61 moves: 927 coalesceable: 603 coalesced: 410
62 moves: 1088 coalesceable: 687 coalesced: 404
63 moves: 1169 coalesceable: 725 coalesced: 434
64 moves: 1254 coalesceable: 765 coalesced: 434
65 moves: 1343 coalesceable: 807 coalesced: 407
66 moves: 1436 coalesceable: 851 coalesced: 420
67 moves: 1533 coalesceable: 897 coalesced: 459
68 moves: 1634 coalesceable: 943 coalesced: 482
69 moves: 1739 coalesceable: 989 coalesced: 504
70 moves: 1848 coalesceable: 1035 coalesced: 506
71 moves: 17 coalesceable: 15 coalesced: 15
72 moves: 19 coalesceable: 17 coalesced: 17
73 moves: 21 coalesceable: 18 coalesced: 17
74 moves: 21 coalesceable: 19 coalesced: 19
75 moves: 23 coalesceable: 20 coalesced: 19
76 moves: 25 coalesceable: 21 coalesced: 20
77 moves: 23 coalesceable: 21 coalesced: 21
78 moves: 25 coalesceable: 22 coalesced: 21
79 moves: 27 coalesceable: 23 coalesced: 22
80 moves: 29 coalesceable: 24 coalesced: 23
81 moves: 25 coalesceable: 23 coalesced: 19
82 moves: 27 coalesceable: 24 coalesced: 20
83 moves: 29 coalesceable: 25 coalesced: 21
84 moves: 31 coalesceable: 26 coalesced: 22
85 moves: 33 coalesceable: 27 coalesced: 23
86 moves: 27 coalesceable: 24 coalesced: 21
87 moves: 29 coalesceable: 25 coalesced: 22
88 moves: 31 coalesceable: 26 coalesced: 23
89 moves: 33 coalesceable: 27 coalesced: 24
90 moves: 35 coalesceable: 28 coalesced: 25
91 moves: 37 coalesceable: 29 coalesced: 26
92 moves: 29 coalesceable: 25 coalesced: 16
93 moves: 31 coalesceable: 26 coalesced: 18
94 moves: 33 coalesceable: 27 coalesced: 23
95 moves: 35 coalesceable: 28 coalesced: 21
96 moves: 37 coalesceable: 29 coalesced: 22
97 moves: 39 coalesceable: 30 coalesced: 23
98 moves: 41 coalesceable: 31 coalesced: 24
99 moves: 31 coalesceable: 25 coalesced: 12
100 moves: 33 coalesceable: 27 coalesced: 9
101 moves: 35 coalesceable: 28 coalesced: 16
102 moves: 37 coalesceable: 29 coalesced: 23
103 moves: 39 coalesceable: 30 coalesced: 23
104 moves: 41 coalesceable: 31 coalesced: 21
105 moves: 43 coalesceable: 32 coalesced: 22
106 moves: 45 coalesceable: 33 coalesced: 25
107 moves: 33 coalesceable: 25 coalesced: 14
108 moves: 35 coalesceable: 27 coalesced: 10
109 moves: 37 coalesceable: 29 coalesced: 11
110 moves: 39 coalesceable: 30 coalesced: 14
111 moves: 41 coalesceable: 31 coalesced: 21
112 moves: 43 coalesceable: 32 coalesced: 23
113 moves: 45 coalesceable: 33 coalesced: 23
114 moves: 47 coalesceable: 34 coalesced: 23
115 moves: 49 coalesceable: 35 coalesced: 25
116 moves: 62 coalesceable: 11 coalesced: 7
117 moves: 934 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 11 coalesced: 11
119 moves: 17 coalesceable: 11 coalesced: 11
120 moves: 17 coalesceable: 11 coalesced: 11
121 moves: 17 coalesceable: 11 coalesced: 11
122 moves: 17 coalesceable: 11 coalesced: 11
123 moves: 17 coalesceable: 11 coalesced: 11
124 moves: 17 coalesceable: 11 coalesced: 11
125 moves: 17 coalesceable: 11 coalesced: 11
126 moves: 17 coalesceable: 11 coalesced: 11
127 moves: 4375 coalesceable: 2573 coalesced: 2573
128 moves: 17 coalesceable: 11 coalesced: 11
129 moves: 17 coalesceable: 11 coalesced: 11
130 moves: 17 coalesceable: 11 coalesced: 11
131 moves: 17 coalesceable: 11 coalesced: 11
132 moves: 17 coalesceable: 11 coalesced: 11
133 moves: 17 coalesceable: 11 coalesced: 11
134 moves: 17 coalesceable: 11 coalesced: 11
135 moves: 17 coalesceable: 11 coalesced: 11
136 moves: 10 coalesceable: 6 coalesced: 6
137 moves: 60 coalesceable: 41 coalesced: 40
138 moves: 17 coalesceable: 11 coalesced: 11
139 moves: 17 coalesceable: 11 coalesced: 11
140 moves: 17 coalesceable: 11 coalesced: 11
141 moves: 17 coalesceable: 11 coalesced: 11
142 moves: 2 coalesceable: 2 coalesced: 2
143 moves: 17 coalesceable: 11 coalesced: 11
144 moves: 5 coalesceable: 3 coalesced: 3
145 moves: 4 coalesceable: 4 coalesced: 4
146 moves: 9 coalesceable: 9 coalesced: 8
147 moves: 8 coalesceable: 8 coalesced: 8
148 moves: 124 coalesceable: 72 coalesced: 58
149 moves: 6 coalesceable: 6 coalesced: 6
150 moves: 23 coalesceable: 15 coalesced: 11
151 moves: 6 coalesceable: 6 coalesced: 6
152 moves: 23 coalesceable: 15 coalesced: 11
153 moves: 6 coalesceable: 6 coalesced: 6
154 moves: 30 coalesceable: 19 coalesced: 16
155 moves: 6 coalesceable: 6 coalesced: 6
156 moves: 29 coalesceable: 21 coalesced: 17
157 moves: 6 coalesceable: 6 coalesced: 6
158 moves: 24 coalesceable: 16 coalesced: 13
159 moves: 6 coalesceable: 6 coalesced: 6
160 moves: 24 coalesceable: 16 coalesced: 13
161 moves: 6 coalesceable: 6 coalesced: 6
162 moves: 30 coalesceable: 22 coalesced: 19
163 moves: 4 coalesceable: 4 coalesced: 4
164 moves: 25 coalesceable: 18 coalesced: 16
165 moves: 4 coalesceable: 4 coalesced: 4
166 moves: 3 coalesceable: 3 coalesced: 3
167 moves: 6 coalesceable: 6 coalesced: 6
168 moves: 21 coalesceable: 19 coalesced: 19
169 moves: 8 coalesceable: 8 coalesced: 8
170 moves: 22 coalesceable: 20 coalesced: 20
171 moves: 12 coalesceable: 12 coalesced: 12
172 moves: 218 coalesceable: 134 coalesced: 94
173 moves: 8 coalesceable: 8 coalesced: 8
174 moves: 163 coalesceable: 110 coalesced: 96
175 moves: 6 coalesceable: 6 coalesced: 6
176 moves: 114 coalesceable: 80 coalesced: 72
177 moves: 4 coalesceable: 4 coalesced: 4
178 moves: 6 coalesceable: 6 coalesced: 6
179 moves: 8 coalesceable: 8 coalesced: 8
180 moves: 128 coalesceable: 77 coalesced: 70
181 moves: 8 coalesceable: 8 coalesced: 8
182 moves: 111 coalesceable: 66 coalesced: 51
183 moves: 6 coalesceable: 6 coalesced: 6
184 moves: 427 coalesceable: 263 coalesced: 198
185 moves: 4 coalesceable: 4 coalesced: 4
186 moves: 5 coalesceable: 5 coalesced: 5
187 moves: 4 coalesceable: 4 coalesced: 4
188 moves: 64 coalesceable: 47 coalesced: 47
runtime: 8.9s, gctime: 0.02193s, systime: 0.04590s.
external oracle real: 9.0s
external oracle size: 133870
apply colour (par) eval: runtime: 1m14s, gctime: 1.8s, systime: 0.72928s.
apply colour (par) real: 45.8s
apply colour (par) size: 592770
check colour eval: runtime: 0.88733s, gctime: 0.00000s, systime: 0.00000s.
check colour real: 0.88881s
check colour size: 592960
word_to_stack eval: runtime: 59.0s, gctime: 0.95471s, systime: 0.12468s.
word_to_stack real: 59.2s
word_to_stack size: 487197
stack_rawcall eval: runtime: 33.6s, gctime: 0.36369s, systime: 0.04888s.
stack_rawcall real: 33.7s
stack_rawcall size: 481116
stack_alloc (par) eval: runtime: 44.8s, gctime: 0.59542s, systime: 0.09193s.
stack_alloc (par) real: 22.8s
stack_alloc (par) size: 482377
expand stack_remove_def eval: runtime: 0.03411s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.03418s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 1m00s, gctime: 0.70774s, systime: 0.08865s.
stack_remove (par) real: 35.3s
stack_remove (par) size: 826411
stack_names (par) eval: runtime: 31.7s, gctime: 0.66482s, systime: 0.06288s.
stack_names (par) real: 16.3s
stack_names (par) size: 852930
stack_to_lab (par) eval: runtime: 1m04s, gctime: 1.2s, systime: 0.13589s.
stack_to_lab (par) real: 32.9s
stack_to_lab (par) size: 1035167
lab_to_target eval: runtime: 3m18s, gctime: 5.1s, systime: 0.56482s.
lab_to_target real: 3m19s
lab_to_target size: 1656145
export: runtime: 0.38493s, gctime: 0.00637s, systime: 0.02596s.
Saved theorem _____ "hello_compiled"
Exporting theory "helloCompile" ... done.
Theory "helloCompile" took 12m23s to build
cc hello.S /home/cake/oven/regression/cakeml-1483/basis/basis_ffi.o -o cake_hello
Linking /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript.uo to produce theory-builder executable
/home/cake/oven/regression/HOL-02777f989ba557fe906094a01dd6a18ec7fb2e94/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cake/oven/regression/cakeml-1483/compiler/compilationLib.sml:188: warning: Pattern is not exhaustive.
Found near
val (_, [conf_tm, ...]) = to_data_thm |> concl |> lhs |> strip_comb
<<HOL message: Created theory "helloErrCompile">>
to_flat eval: runtime: 6.6s, gctime: 0.36687s, systime: 0.21370s.
to_flat real: 6.8s
to_flat size: 57713
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.24417s, gctime: 0.05660s, systime: 0.02394s.
to_clos real: 0.26860s
to_clos size: 34220
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 3.7s, gctime: 0.13065s, systime: 0.01294s.
to_bvl real: 3.7s
to_bvl size: 56636
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 32.8s, gctime: 0.24827s, systime: 0.02679s.
to_bvi real: 32.9s
to_bvi size: 64310
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 10.1s, gctime: 0.43435s, systime: 0.04390s.
to_data real: 10.1s
to_data size: 112949
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 13.9s, gctime: 0.44034s, systime: 0.05091s.
data_to_word real: 14.0s
data_to_word size: 299804
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 59.5s, gctime: 2.4s, systime: 0.28287s.
inst,ssa,two-reg (par) real: 31.0s
inst,ssa,two-reg (par) size: 1207123
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 6.8s, gctime: 0.98342s, systime: 0.08598s.
get_clash (par) real: 3.8s
get_clash (par) size: 1878430
external oracle eval: Num regs: 9 Alg: IRC
0 moves: 75 coalesceable: 61 coalesced: 53
1 moves: 24 coalesceable: 22 coalesced: 20
2 moves: 90 coalesceable: 68 coalesced: 53
3 moves: 25 coalesceable: 19 coalesced: 17
4 moves: 16 coalesceable: 15 coalesced: 12
5 moves: 148 coalesceable: 116 coalesced: 110
6 moves: 7 coalesceable: 7 coalesced: 7
7 moves: 7 coalesceable: 7 coalesced: 7
8 moves: 7 coalesceable: 7 coalesced: 7
9 moves: 7 coalesceable: 7 coalesced: 7
10 moves: 7 coalesceable: 7 coalesced: 7
11 moves: 19 coalesceable: 17 coalesced: 12
12 moves: 47 coalesceable: 41 coalesced: 37
13 moves: 31 coalesceable: 20 coalesced: 17
14 moves: 58 coalesceable: 48 coalesced: 42
15 moves: 0 coalesceable: 0 coalesced: 0
16 moves: 10 coalesceable: 8 coalesced: 5
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 21 coalesceable: 20 coalesced: 20
19 moves: 22 coalesceable: 21 coalesced: 20
20 moves: 19 coalesceable: 15 coalesced: 15
21 moves: 35 coalesceable: 29 coalesced: 25
22 moves: 40 coalesceable: 34 coalesced: 33
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 19 coalesceable: 17 coalesced: 15
25 moves: 42 coalesceable: 38 coalesced: 29
26 moves: 20 coalesceable: 20 coalesced: 14
27 moves: 20 coalesceable: 20 coalesced: 10
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 316 coalesceable: 269 coalesced: 269
31 moves: 26 coalesceable: 23 coalesced: 23
32 moves: 24 coalesceable: 23 coalesced: 23
33 moves: 16 coalesceable: 15 coalesced: 15
34 moves: 22 coalesceable: 19 coalesced: 19
35 moves: 90 coalesceable: 81 coalesced: 81
36 moves: 85 coalesceable: 82 coalesced: 82
37 moves: 65 coalesceable: 62 coalesced: 62
38 moves: 88 coalesceable: 85 coalesced: 85
39 moves: 29 coalesceable: 26 coalesced: 26
40 moves: 48 coalesceable: 45 coalesced: 45
41 moves: 7 coalesceable: 6 coalesced: 6
42 moves: 22 coalesceable: 19 coalesced: 19
43 moves: 12 coalesceable: 11 coalesced: 11
44 moves: 21 coalesceable: 18 coalesced: 18
45 moves: 51 coalesceable: 48 coalesced: 48
46 moves: 8 coalesceable: 7 coalesced: 7
47 moves: 11 coalesceable: 10 coalesced: 10
48 moves: 22 coalesceable: 19 coalesced: 19
49 moves: 26 coalesceable: 23 coalesced: 23
50 moves: 15 coalesceable: 14 coalesced: 14
51 moves: 20 coalesceable: 17 coalesced: 17
52 moves: 24 coalesceable: 21 coalesced: 21
53 moves: 190 coalesceable: 117 coalesced: 103
54 moves: 92 coalesceable: 65 coalesced: 51
55 moves: 41 coalesceable: 26 coalesced: 25
56 moves: 35 coalesceable: 26 coalesced: 21
57 moves: 56 coalesceable: 42 coalesced: 36
58 moves: 71 coalesceable: 46 coalesced: 40
59 moves: 48 coalesceable: 37 coalesced: 32
60 moves: 71 coalesceable: 46 coalesced: 38
61 moves: 927 coalesceable: 603 coalesced: 410
62 moves: 1088 coalesceable: 687 coalesced: 404
63 moves: 1169 coalesceable: 725 coalesced: 434
64 moves: 1254 coalesceable: 765 coalesced: 434
65 moves: 1343 coalesceable: 807 coalesced: 407
66 moves: 1436 coalesceable: 851 coalesced: 420
67 moves: 1533 coalesceable: 897 coalesced: 459
68 moves: 1634 coalesceable: 943 coalesced: 482
69 moves: 1739 coalesceable: 989 coalesced: 504
70 moves: 1848 coalesceable: 1035 coalesced: 506
71 moves: 17 coalesceable: 15 coalesced: 15
72 moves: 19 coalesceable: 17 coalesced: 17
73 moves: 21 coalesceable: 18 coalesced: 17
74 moves: 21 coalesceable: 19 coalesced: 19
75 moves: 23 coalesceable: 20 coalesced: 19
76 moves: 25 coalesceable: 21 coalesced: 20
77 moves: 23 coalesceable: 21 coalesced: 21
78 moves: 25 coalesceable: 22 coalesced: 21
79 moves: 27 coalesceable: 23 coalesced: 22
80 moves: 29 coalesceable: 24 coalesced: 23
81 moves: 25 coalesceable: 23 coalesced: 19
82 moves: 27 coalesceable: 24 coalesced: 20
83 moves: 29 coalesceable: 25 coalesced: 21
84 moves: 31 coalesceable: 26 coalesced: 22
85 moves: 33 coalesceable: 27 coalesced: 23
86 moves: 27 coalesceable: 24 coalesced: 21
87 moves: 29 coalesceable: 25 coalesced: 22
88 moves: 31 coalesceable: 26 coalesced: 23
89 moves: 33 coalesceable: 27 coalesced: 24
90 moves: 35 coalesceable: 28 coalesced: 25
91 moves: 37 coalesceable: 29 coalesced: 26
92 moves: 29 coalesceable: 25 coalesced: 16
93 moves: 31 coalesceable: 26 coalesced: 18
94 moves: 33 coalesceable: 27 coalesced: 23
95 moves: 35 coalesceable: 28 coalesced: 21
96 moves: 37 coalesceable: 29 coalesced: 22
97 moves: 39 coalesceable: 30 coalesced: 23
98 moves: 41 coalesceable: 31 coalesced: 24
99 moves: 31 coalesceable: 25 coalesced: 12
100 moves: 33 coalesceable: 27 coalesced: 9
101 moves: 35 coalesceable: 28 coalesced: 16
102 moves: 37 coalesceable: 29 coalesced: 23
103 moves: 39 coalesceable: 30 coalesced: 23
104 moves: 41 coalesceable: 31 coalesced: 21
105 moves: 43 coalesceable: 32 coalesced: 22
106 moves: 45 coalesceable: 33 coalesced: 25
107 moves: 33 coalesceable: 25 coalesced: 14
108 moves: 35 coalesceable: 27 coalesced: 10
109 moves: 37 coalesceable: 29 coalesced: 11
110 moves: 39 coalesceable: 30 coalesced: 14
111 moves: 41 coalesceable: 31 coalesced: 21
112 moves: 43 coalesceable: 32 coalesced: 23
113 moves: 45 coalesceable: 33 coalesced: 23
114 moves: 47 coalesceable: 34 coalesced: 23
115 moves: 49 coalesceable: 35 coalesced: 25
116 moves: 62 coalesceable: 11 coalesced: 7
117 moves: 934 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 11 coalesced: 11
119 moves: 17 coalesceable: 11 coalesced: 11
120 moves: 17 coalesceable: 11 coalesced: 11
121 moves: 17 coalesceable: 11 coalesced: 11
122 moves: 17 coalesceable: 11 coalesced: 11
123 moves: 17 coalesceable: 11 coalesced: 11
124 moves: 17 coalesceable: 11 coalesced: 11
125 moves: 17 coalesceable: 11 coalesced: 11
126 moves: 17 coalesceable: 11 coalesced: 11
127 moves: 17 coalesceable: 11 coalesced: 11
128 moves: 17 coalesceable: 11 coalesced: 11
129 moves: 4375 coalesceable: 2573 coalesced: 2573
130 moves: 17 coalesceable: 11 coalesced: 11
131 moves: 17 coalesceable: 11 coalesced: 11
132 moves: 17 coalesceable: 11 coalesced: 11
133 moves: 17 coalesceable: 11 coalesced: 11
134 moves: 17 coalesceable: 11 coalesced: 11
135 moves: 17 coalesceable: 11 coalesced: 11
136 moves: 17 coalesceable: 11 coalesced: 11
137 moves: 17 coalesceable: 11 coalesced: 11
138 moves: 10 coalesceable: 6 coalesced: 6
139 moves: 60 coalesceable: 41 coalesced: 40
140 moves: 60 coalesceable: 41 coalesced: 40
141 moves: 17 coalesceable: 11 coalesced: 11
142 moves: 17 coalesceable: 11 coalesced: 11
143 moves: 17 coalesceable: 11 coalesced: 11
144 moves: 17 coalesceable: 11 coalesced: 11
145 moves: 2 coalesceable: 2 coalesced: 2
146 moves: 17 coalesceable: 11 coalesced: 11
147 moves: 5 coalesceable: 3 coalesced: 3
148 moves: 4 coalesceable: 4 coalesced: 4
149 moves: 69 coalesceable: 44 coalesced: 38
150 moves: 4 coalesceable: 4 coalesced: 4
151 moves: 3 coalesceable: 3 coalesced: 3
152 moves: 4 coalesceable: 4 coalesced: 4
153 moves: 9 coalesceable: 9 coalesced: 8
154 moves: 8 coalesceable: 8 coalesced: 8
155 moves: 124 coalesceable: 72 coalesced: 58
156 moves: 6 coalesceable: 6 coalesced: 6
157 moves: 23 coalesceable: 15 coalesced: 11
158 moves: 6 coalesceable: 6 coalesced: 6
159 moves: 23 coalesceable: 15 coalesced: 11
160 moves: 6 coalesceable: 6 coalesced: 6
161 moves: 30 coalesceable: 19 coalesced: 16
162 moves: 6 coalesceable: 6 coalesced: 6
163 moves: 29 coalesceable: 21 coalesced: 17
164 moves: 6 coalesceable: 6 coalesced: 6
165 moves: 24 coalesceable: 16 coalesced: 13
166 moves: 6 coalesceable: 6 coalesced: 6
167 moves: 24 coalesceable: 16 coalesced: 13
168 moves: 6 coalesceable: 6 coalesced: 6
169 moves: 30 coalesceable: 22 coalesced: 19
170 moves: 4 coalesceable: 4 coalesced: 4
171 moves: 25 coalesceable: 18 coalesced: 16
172 moves: 4 coalesceable: 4 coalesced: 4
173 moves: 3 coalesceable: 3 coalesced: 3
174 moves: 6 coalesceable: 6 coalesced: 6
175 moves: 21 coalesceable: 19 coalesced: 19
176 moves: 8 coalesceable: 8 coalesced: 8
177 moves: 22 coalesceable: 20 coalesced: 20
178 moves: 12 coalesceable: 12 coalesced: 12
179 moves: 218 coalesceable: 134 coalesced: 94
180 moves: 8 coalesceable: 8 coalesced: 8
181 moves: 163 coalesceable: 110 coalesced: 96
182 moves: 6 coalesceable: 6 coalesced: 6
183 moves: 114 coalesceable: 80 coalesced: 72
184 moves: 4 coalesceable: 4 coalesced: 4
185 moves: 6 coalesceable: 6 coalesced: 6
186 moves: 8 coalesceable: 8 coalesced: 8
187 moves: 128 coalesceable: 77 coalesced: 70
188 moves: 8 coalesceable: 8 coalesced: 8
189 moves: 111 coalesceable: 66 coalesced: 51
190 moves: 6 coalesceable: 6 coalesced: 6
191 moves: 427 coalesceable: 263 coalesced: 198
192 moves: 4 coalesceable: 4 coalesced: 4
193 moves: 5 coalesceable: 5 coalesced: 5
194 moves: 4 coalesceable: 4 coalesced: 4
195 moves: 71 coalesceable: 51 coalesced: 51
runtime: 9.1s, gctime: 0.09115s, systime: 0.01094s.
external oracle real: 9.1s
external oracle size: 135006
apply colour (par) eval: runtime: 1m20s, gctime: 8.8s, systime: 0.86696s.
apply colour (par) real: 52.0s
apply colour (par) size: 597855
check colour eval: runtime: 1.0s, gctime: 0.11515s, systime: 0.00199s.
check colour real: 1.0s
check colour size: 598052
word_to_stack eval: runtime: 57.3s, gctime: 1.1s, systime: 0.05956s.
word_to_stack real: 57.5s
word_to_stack size: 490894
stack_rawcall eval: runtime: 33.8s, gctime: 0.42785s, systime: 0.02682s.
stack_rawcall real: 33.8s
stack_rawcall size: 484724
stack_alloc (par) eval: runtime: 44.6s, gctime: 0.46708s, systime: 0.03092s.
stack_alloc (par) real: 22.4s
stack_alloc (par) size: 486045
expand stack_remove_def eval: runtime: 0.03374s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.03383s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 59.5s, gctime: 0.84219s, systime: 0.08884s.
stack_remove (par) real: 34.4s
stack_remove (par) size: 831882
stack_names (par) eval: runtime: 31.7s, gctime: 0.69986s, systime: 0.06091s.
stack_names (par) real: 16.1s
stack_names (par) size: 858623
stack_to_lab (par) eval: runtime: 1m03s, gctime: 1.3s, systime: 0.14179s.
stack_to_lab (par) real: 32.2s
stack_to_lab (par) size: 1042262
lab_to_target eval: runtime: 3m13s, gctime: 6.4s, systime: 0.55978s.
lab_to_target real: 3m14s
lab_to_target size: 1667906
export: runtime: 0.48073s, gctime: 0.07626s, systime: 0.02197s.
Saved theorem _____ "helloErr_compiled"
Exporting theory "helloErrCompile" ... Run out of store - interrupting threads
Failure while writing theory!
error in quse /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript.sml : Interrupt
error in load /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript : Interrupt
Uncaught exception: Interrupt
Failed script build for /home/cake/oven/regression/cakeml-1483/examples/compilation/x64/helloErrCompileScript - exited with code 1