OverviewCakeML:a2713f8e8f8b719d4618f4be35c23419b5f4c348
Merge pull request #831 from CakeML/pancake
HOL:a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042
Adjust miller deps for inclusion in parallel builds
Machine:oven3 4.19.67.1.amd64-smp
Claimed job
Building HOL
Starting developers
Finished developers 7s 131MB
Starting developers/bin
Finished developers/bin 13s 1GB
Starting semantics/ffi
Finished semantics/ffi 24s 264MB
Starting semantics
Finished semantics 3m11s 1GB
Starting semantics/proofs
Finished semantics/proofs 8m01s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 19s 391MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 4m55s 1GB
Starting basis/pure
Finished basis/pure 6m09s 913MB
Starting translator
Finished translator 6m46s 1GB
Starting compiler/parsing
Finished compiler/parsing 2m32s 2GB
Starting characteristic
Finished characteristic 12m13s 2GB
Starting translator/monadic
Finished translator/monadic 3m29s 1GB
Starting basis
Finished basis 1h35m58s 16GB
Starting compiler/inference
Finished compiler/inference 2m43s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 2m06s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 7m02s 1GB
Starting compiler/backend
Finished compiler/backend 9m43s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 50s 798MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 2m21s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 4m32s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 1m23s 975MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 3m10s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 3m59s 852MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 41s 901MB
Starting compiler/backend/x64
Finished compiler/backend/x64 40s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 43s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 43s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 45s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 42s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 2m26s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 12m52s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 5m26s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 1h01m31s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 7m47s 951MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 1h40m23s 20GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 21m44s 5GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 30m21s 3GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 15m26s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 22m29s 2GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 20m25s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 5m44s 852MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 51s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 51s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 49s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 49s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 49s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 27m40s 3GB
Starting compiler/proofs
Finished compiler/proofs 4m22s 3GB
Starting candle/set-theory
Finished candle/set-theory 59s 768MB
Starting candle/syntax-lib
Finished candle/syntax-lib 23s 648MB
Starting candle/standard/syntax
Finished candle/standard/syntax 3m54s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 3m45s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 3m39s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 12m11s 4GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 6m39s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 26m12s 4GB
Starting pancake
Finished pancake 1m44s 796MB
Starting pancake/ffi
Finished pancake/ffi 0s 9MB
Starting pancake/semantics
Finished pancake/semantics 4m49s 1GB
Starting pancake/proofs
Finished pancake/proofs 27m14s 7GB
Starting characteristic/examples
Finished characteristic/examples 2m54s 3GB
Starting tutorial/solutions
Finished tutorial/solutions 34m16s 8GB
Starting translator/monadic/examples
Finished translator/monadic/examples 5m54s 3GB
Starting examples
Finished examples 16m58s 4GB
Starting examples/compilation/x64
FAILED: examples/compilation/x64
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[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)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/topology[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
/root/regression/cakeml-1571/developers/readme_gen catCompileScript.sml diffCompileScript.sml echoCompileScript.sml grepCompileScript.sml helloCompileScript.sml helloErrCompileScript.sml iocatCompileScript.sml patchCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml
Linking /root/regression/cakeml-1571/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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: 47.1s, gctime: 1.4s, systime: 0.44689s.
to_flat real: 47.5s
to_flat size: 108464
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.75965s, gctime: 0.09532s, systime: 0.01004s.
to_clos real: 0.76977s
to_clos size: 44517
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 9.8s, gctime: 0.39426s, systime: 0.06002s.
to_bvl real: 9.9s
to_bvl size: 79151
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m36s, gctime: 1.1s, systime: 0.53309s.
to_bvi real: 1m36s
to_bvi size: 83664
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 21.8s, gctime: 1.1s, systime: 0.17007s.
to_data real: 21.9s
to_data size: 132309
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 31.5s, gctime: 1.3s, systime: 0.22339s.
data_to_word real: 31.7s
data_to_word size: 323571
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m20s, gctime: 8.7s, systime: 5.3s.
inst,ssa,two-reg (par) real: 1m11s
inst,ssa,two-reg (par) size: 1288173
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 36.3s, gctime: 15.2s, systime: 4.3s.
get_clash (par) real: 25.2s
get_clash (par) size: 1998562
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: 954 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 10 coalesceable: 6 coalesced: 6
156 moves: 60 coalesceable: 41 coalesced: 40
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: 2 coalesceable: 2 coalesced: 2
168 moves: 17 coalesceable: 11 coalesced: 11
169 moves: 17 coalesceable: 11 coalesced: 11
170 moves: 17 coalesceable: 11 coalesced: 11
171 moves: 5 coalesceable: 3 coalesced: 3
172 moves: 6 coalesceable: 6 coalesced: 6
173 moves: 29 coalesceable: 19 coalesced: 13
174 moves: 4 coalesceable: 4 coalesced: 4
175 moves: 7 coalesceable: 7 coalesced: 7
176 moves: 4 coalesceable: 4 coalesced: 4
177 moves: 9 coalesceable: 9 coalesced: 8
178 moves: 8 coalesceable: 8 coalesced: 8
179 moves: 124 coalesceable: 72 coalesced: 58
180 moves: 6 coalesceable: 6 coalesced: 6
181 moves: 62 coalesceable: 31 coalesced: 29
182 moves: 4 coalesceable: 4 coalesced: 4
183 moves: 48 coalesceable: 23 coalesced: 21
184 moves: 6 coalesceable: 6 coalesced: 6
185 moves: 23 coalesceable: 15 coalesced: 11
186 moves: 6 coalesceable: 6 coalesced: 6
187 moves: 23 coalesceable: 15 coalesced: 11
188 moves: 6 coalesceable: 6 coalesced: 6
189 moves: 30 coalesceable: 19 coalesced: 16
190 moves: 6 coalesceable: 6 coalesced: 6
191 moves: 29 coalesceable: 21 coalesced: 17
192 moves: 6 coalesceable: 6 coalesced: 6
193 moves: 24 coalesceable: 16 coalesced: 13
194 moves: 6 coalesceable: 6 coalesced: 6
195 moves: 24 coalesceable: 16 coalesced: 13
196 moves: 6 coalesceable: 6 coalesced: 6
197 moves: 30 coalesceable: 22 coalesced: 19
198 moves: 6 coalesceable: 6 coalesced: 6
199 moves: 60 coalesceable: 44 coalesced: 41
200 moves: 6 coalesceable: 6 coalesced: 6
201 moves: 62 coalesceable: 31 coalesced: 29
202 moves: 4 coalesceable: 4 coalesced: 4
203 moves: 3 coalesceable: 3 coalesced: 3
204 moves: 4 coalesceable: 4 coalesced: 4
205 moves: 43 coalesceable: 29 coalesced: 25
206 moves: 4 coalesceable: 4 coalesced: 4
207 moves: 3 coalesceable: 3 coalesced: 3
208 moves: 4 coalesceable: 4 coalesced: 4
209 moves: 18 coalesceable: 16 coalesced: 16
210 moves: 4 coalesceable: 4 coalesced: 4
211 moves: 25 coalesceable: 18 coalesced: 16
212 moves: 4 coalesceable: 4 coalesced: 4
213 moves: 3 coalesceable: 3 coalesced: 3
214 moves: 6 coalesceable: 6 coalesced: 6
215 moves: 36 coalesceable: 23 coalesced: 17
216 moves: 6 coalesceable: 6 coalesced: 6
217 moves: 21 coalesceable: 19 coalesced: 19
218 moves: 8 coalesceable: 8 coalesced: 8
219 moves: 22 coalesceable: 20 coalesced: 20
220 moves: 12 coalesceable: 12 coalesced: 12
221 moves: 218 coalesceable: 134 coalesced: 94
222 moves: 8 coalesceable: 8 coalesced: 8
223 moves: 124 coalesceable: 72 coalesced: 58
224 moves: 4 coalesceable: 4 coalesced: 4
225 moves: 77 coalesceable: 56 coalesced: 53
226 moves: 6 coalesceable: 6 coalesced: 6
227 moves: 110 coalesceable: 79 coalesced: 69
228 moves: 8 coalesceable: 8 coalesced: 8
229 moves: 407 coalesceable: 208 coalesced: 175
230 moves: 4 coalesceable: 4 coalesced: 4
231 moves: 56 coalesceable: 33 coalesced: 30
232 moves: 4 coalesceable: 4 coalesced: 4
233 moves: 8 coalesceable: 6 coalesced: 6
234 moves: 8 coalesceable: 8 coalesced: 8
235 moves: 163 coalesceable: 110 coalesced: 96
236 moves: 6 coalesceable: 6 coalesced: 6
237 moves: 114 coalesceable: 80 coalesced: 72
238 moves: 4 coalesceable: 4 coalesced: 4
239 moves: 6 coalesceable: 6 coalesced: 6
240 moves: 4 coalesceable: 4 coalesced: 4
241 moves: 6 coalesceable: 6 coalesced: 6
242 moves: 8 coalesceable: 8 coalesced: 8
243 moves: 128 coalesceable: 77 coalesced: 70
244 moves: 8 coalesceable: 8 coalesced: 8
245 moves: 111 coalesceable: 66 coalesced: 51
246 moves: 6 coalesceable: 6 coalesced: 6
247 moves: 50 coalesceable: 38 coalesced: 35
248 moves: 6 coalesceable: 6 coalesced: 6
249 moves: 427 coalesceable: 263 coalesced: 198
250 moves: 4 coalesceable: 4 coalesced: 4
251 moves: 5 coalesceable: 5 coalesced: 5
252 moves: 4 coalesceable: 4 coalesced: 4
253 moves: 272 coalesceable: 139 coalesced: 131
254 moves: 4 coalesceable: 4 coalesced: 4
255 moves: 69 coalesceable: 54 coalesced: 54
256 moves: 6 coalesceable: 6 coalesced: 6
257 moves: 78 coalesceable: 59 coalesced: 56
258 moves: 4 coalesceable: 4 coalesced: 4
259 moves: 21 coalesceable: 18 coalesced: 16
260 moves: 4 coalesceable: 4 coalesced: 4
261 moves: 15 coalesceable: 12 coalesced: 12
262 moves: 25 coalesceable: 21 coalesced: 21
263 moves: 24 coalesceable: 15 coalesced: 15
264 moves: 4 coalesceable: 4 coalesced: 4
265 moves: 34 coalesceable: 19 coalesced: 17
266 moves: 4 coalesceable: 4 coalesced: 4
267 moves: 16 coalesceable: 11 coalesced: 10
268 moves: 4 coalesceable: 4 coalesced: 4
269 moves: 11 coalesceable: 7 coalesced: 7
runtime: 20.2s, gctime: 0.05132s, systime: 0.41319s.
external oracle real: 20.6s
external oracle size: 146942
apply colour (par) eval: runtime: 2m48s, gctime: 4.8s, systime: 12.6s.
apply colour (par) real: 1m42s
apply colour (par) size: 648526
check colour eval: runtime: 2.1s, gctime: 0.00000s, systime: 0.12329s.
check colour real: 2.3s
check colour size: 648797
word_to_stack eval: runtime: 2m10s, gctime: 2.4s, systime: 2.3s.
word_to_stack real: 2m12s
word_to_stack size: 528258
stack_rawcall eval: runtime: 1m11s, gctime: 0.95374s, systime: 0.85316s.
stack_rawcall real: 1m12s
stack_rawcall size: 521088
stack_alloc (par) eval: runtime: 1m39s, gctime: 1.2s, systime: 8.2s.
stack_alloc (par) real: 50.5s
stack_alloc (par) size: 523057
expand stack_remove_def eval: runtime: 0.08649s, gctime: 0.00000s, systime: 0.04000s.
expand stack_remove_def real: 0.12635s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m14s, gctime: 1.8s, systime: 5.3s.
stack_remove (par) real: 1m14s
stack_remove (par) size: 891840
stack_names (par) eval: runtime: 1m08s, gctime: 1.5s, systime: 3.2s.
stack_names (par) real: 33.3s
stack_names (par) size: 920477
stack_to_lab (par) eval: runtime: 2m20s, gctime: 3.1s, systime: 6.3s.
stack_to_lab (par) real: 1m07s
stack_to_lab (par) size: 1122115
lab_to_target eval: runtime: 8m01s, gctime: 39.4s, systime: 8.3s.
lab_to_target real: 8m09s
lab_to_target size: 1808541
export: runtime: 0.74331s, gctime: 0.00000s, systime: 0.00000s.
Saved theorem _____ "cat_compiled"
Exporting theory "catCompile" ... done.
Theory "catCompile" took 29m51s to build
Linking /root/regression/cakeml-1571/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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: 51.8s, gctime: 1.2s, systime: 0.59320s.
to_flat real: 52.4s
to_flat size: 156755
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 1.7s, gctime: 0.17204s, systime: 0.01313s.
to_clos real: 1.7s
to_clos size: 67276
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 13.5s, gctime: 0.38476s, systime: 0.08657s.
to_bvl real: 13.6s
to_bvl size: 124955
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 2m01s, gctime: 1.2s, systime: 0.67978s.
to_bvi real: 2m02s
to_bvi size: 122650
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 26.3s, gctime: 1.1s, systime: 0.24348s.
to_data real: 26.5s
to_data size: 194278
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 39.9s, gctime: 1.6s, systime: 0.33325s.
data_to_word real: 40.2s
data_to_word size: 432685
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 3m27s, gctime: 19.2s, systime: 6.1s.
inst,ssa,two-reg (par) real: 1m25s
inst,ssa,two-reg (par) size: 1677665
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 29.4s, gctime: 2.7s, systime: 1.3s.
get_clash (par) real: 10.0s
get_clash (par) size: 2634628
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: 986 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 17 coalesceable: 11 coalesced: 11
170 moves: 10 coalesceable: 6 coalesced: 6
171 moves: 60 coalesceable: 41 coalesced: 40
172 moves: 60 coalesceable: 41 coalesced: 40
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: 17 coalesceable: 11 coalesced: 11
186 moves: 2 coalesceable: 2 coalesced: 2
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: 17 coalesceable: 11 coalesced: 11
204 moves: 114 coalesceable: 84 coalesced: 84
205 moves: 17 coalesceable: 11 coalesced: 11
206 moves: 17 coalesceable: 11 coalesced: 11
207 moves: 5 coalesceable: 3 coalesced: 3
208 moves: 4 coalesceable: 4 coalesced: 4
209 moves: 6 coalesceable: 6 coalesced: 6
210 moves: 4 coalesceable: 4 coalesced: 4
211 moves: 6 coalesceable: 6 coalesced: 6
212 moves: 6 coalesceable: 6 coalesced: 6
213 moves: 29 coalesceable: 19 coalesced: 13
214 moves: 6 coalesceable: 6 coalesced: 6
215 moves: 32 coalesceable: 23 coalesced: 18
216 moves: 4 coalesceable: 4 coalesced: 4
217 moves: 5 coalesceable: 5 coalesced: 3
218 moves: 6 coalesceable: 6 coalesced: 6
219 moves: 36 coalesceable: 25 coalesced: 24
220 moves: 4 coalesceable: 4 coalesced: 4
221 moves: 5 coalesceable: 5 coalesced: 3
222 moves: 4 coalesceable: 4 coalesced: 4
223 moves: 7 coalesceable: 7 coalesced: 7
224 moves: 4 coalesceable: 4 coalesced: 4
225 moves: 7 coalesceable: 7 coalesced: 7
226 moves: 4 coalesceable: 4 coalesced: 4
227 moves: 45 coalesceable: 35 coalesced: 33
228 moves: 6 coalesceable: 6 coalesced: 6
229 moves: 86 coalesceable: 57 coalesced: 51
230 moves: 6 coalesceable: 6 coalesced: 6
231 moves: 76 coalesceable: 47 coalesced: 43
232 moves: 4 coalesceable: 4 coalesced: 4
233 moves: 9 coalesceable: 9 coalesced: 8
234 moves: 8 coalesceable: 8 coalesced: 8
235 moves: 124 coalesceable: 72 coalesced: 58
236 moves: 6 coalesceable: 6 coalesced: 6
237 moves: 62 coalesceable: 31 coalesced: 29
238 moves: 4 coalesceable: 4 coalesced: 4
239 moves: 48 coalesceable: 23 coalesced: 21
240 moves: 6 coalesceable: 6 coalesced: 6
241 moves: 23 coalesceable: 15 coalesced: 11
242 moves: 6 coalesceable: 6 coalesced: 6
243 moves: 23 coalesceable: 15 coalesced: 11
244 moves: 6 coalesceable: 6 coalesced: 6
245 moves: 30 coalesceable: 19 coalesced: 16
246 moves: 6 coalesceable: 6 coalesced: 6
247 moves: 29 coalesceable: 21 coalesced: 17
248 moves: 6 coalesceable: 6 coalesced: 6
249 moves: 24 coalesceable: 16 coalesced: 13
250 moves: 6 coalesceable: 6 coalesced: 6
251 moves: 24 coalesceable: 16 coalesced: 13
252 moves: 6 coalesceable: 6 coalesced: 6
253 moves: 30 coalesceable: 22 coalesced: 19
254 moves: 6 coalesceable: 6 coalesced: 6
255 moves: 60 coalesceable: 44 coalesced: 41
256 moves: 6 coalesceable: 6 coalesced: 6
257 moves: 62 coalesceable: 31 coalesced: 29
258 moves: 6 coalesceable: 6 coalesced: 6
259 moves: 79 coalesceable: 52 coalesced: 46
260 moves: 4 coalesceable: 4 coalesced: 4
261 moves: 162 coalesceable: 108 coalesced: 98
262 moves: 8 coalesceable: 8 coalesced: 8
263 moves: 284 coalesceable: 173 coalesced: 140
264 moves: 8 coalesceable: 8 coalesced: 8
265 moves: 119 coalesceable: 79 coalesced: 60
266 moves: 4 coalesceable: 4 coalesced: 4
267 moves: 423 coalesceable: 264 coalesced: 209
268 moves: 4 coalesceable: 4 coalesced: 4
269 moves: 3 coalesceable: 3 coalesced: 3
270 moves: 4 coalesceable: 4 coalesced: 4
271 moves: 43 coalesceable: 29 coalesced: 25
272 moves: 4 coalesceable: 4 coalesced: 4
273 moves: 25 coalesceable: 18 coalesced: 16
274 moves: 4 coalesceable: 4 coalesced: 4
275 moves: 3 coalesceable: 3 coalesced: 3
276 moves: 6 coalesceable: 6 coalesced: 6
277 moves: 36 coalesceable: 23 coalesced: 17
278 moves: 6 coalesceable: 6 coalesced: 6
279 moves: 21 coalesceable: 19 coalesced: 19
280 moves: 4 coalesceable: 4 coalesced: 4
281 moves: 9 coalesceable: 9 coalesced: 8
282 moves: 8 coalesceable: 8 coalesced: 8
283 moves: 22 coalesceable: 20 coalesced: 20
284 moves: 12 coalesceable: 12 coalesced: 12
285 moves: 218 coalesceable: 134 coalesced: 94
286 moves: 12 coalesceable: 12 coalesced: 12
287 moves: 218 coalesceable: 134 coalesced: 94
288 moves: 8 coalesceable: 8 coalesced: 8
289 moves: 124 coalesceable: 72 coalesced: 58
290 moves: 4 coalesceable: 4 coalesced: 4
291 moves: 77 coalesceable: 56 coalesced: 53
292 moves: 6 coalesceable: 6 coalesced: 6
293 moves: 110 coalesceable: 79 coalesced: 69
294 moves: 8 coalesceable: 8 coalesced: 8
295 moves: 407 coalesceable: 208 coalesced: 175
296 moves: 4 coalesceable: 4 coalesced: 4
297 moves: 56 coalesceable: 33 coalesced: 30
298 moves: 4 coalesceable: 4 coalesced: 4
299 moves: 8 coalesceable: 6 coalesced: 6
300 moves: 8 coalesceable: 8 coalesced: 8
301 moves: 163 coalesceable: 110 coalesced: 96
302 moves: 6 coalesceable: 6 coalesced: 6
303 moves: 114 coalesceable: 80 coalesced: 72
304 moves: 4 coalesceable: 4 coalesced: 4
305 moves: 6 coalesceable: 6 coalesced: 6
306 moves: 4 coalesceable: 4 coalesced: 4
307 moves: 6 coalesceable: 6 coalesced: 6
308 moves: 8 coalesceable: 8 coalesced: 8
309 moves: 128 coalesceable: 77 coalesced: 70
310 moves: 8 coalesceable: 8 coalesced: 8
311 moves: 111 coalesceable: 66 coalesced: 51
312 moves: 6 coalesceable: 6 coalesced: 6
313 moves: 427 coalesceable: 263 coalesced: 198
314 moves: 4 coalesceable: 4 coalesced: 4
315 moves: 5 coalesceable: 5 coalesced: 5
316 moves: 4 coalesceable: 4 coalesced: 4
317 moves: 17 coalesceable: 12 coalesced: 11
318 moves: 4 coalesceable: 4 coalesced: 4
319 moves: 272 coalesceable: 139 coalesced: 131
320 moves: 4 coalesceable: 4 coalesced: 4
321 moves: 69 coalesceable: 54 coalesced: 54
322 moves: 6 coalesceable: 6 coalesced: 6
323 moves: 78 coalesceable: 59 coalesced: 56
324 moves: 4 coalesceable: 4 coalesced: 4
325 moves: 21 coalesceable: 18 coalesced: 16
326 moves: 4 coalesceable: 4 coalesced: 4
327 moves: 164 coalesceable: 106 coalesced: 89
328 moves: 224 coalesceable: 137 coalesced: 113
329 moves: 217 coalesceable: 133 coalesced: 108
330 moves: 4 coalesceable: 4 coalesced: 4
331 moves: 45 coalesceable: 26 coalesced: 24
332 moves: 4 coalesceable: 4 coalesced: 4
333 moves: 42 coalesceable: 23 coalesced: 22
334 moves: 4 coalesceable: 4 coalesced: 4
335 moves: 15 coalesceable: 12 coalesced: 12
336 moves: 36 coalesceable: 18 coalesced: 18
337 moves: 6 coalesceable: 6 coalesced: 6
338 moves: 95 coalesceable: 59 coalesced: 59
339 moves: 12 coalesceable: 12 coalesced: 12
340 moves: 362 coalesceable: 166 coalesced: 106
341 moves: 8 coalesceable: 8 coalesced: 8
342 moves: 98 coalesceable: 66 coalesced: 52
343 moves: 6 coalesceable: 6 coalesced: 6
344 moves: 84 coalesceable: 52 coalesced: 43
345 moves: 6 coalesceable: 6 coalesced: 6
346 moves: 55 coalesceable: 28 coalesced: 23
347 moves: 6 coalesceable: 6 coalesced: 6
348 moves: 90 coalesceable: 61 coalesced: 58
349 moves: 8 coalesceable: 8 coalesced: 8
350 moves: 157 coalesceable: 106 coalesced: 88
351 moves: 6 coalesceable: 6 coalesced: 6
352 moves: 99 coalesceable: 62 coalesced: 56
353 moves: 6 coalesceable: 6 coalesced: 6
354 moves: 275 coalesceable: 122 coalesced: 107
355 moves: 6 coalesceable: 6 coalesced: 6
356 moves: 7 coalesceable: 7 coalesced: 7
357 moves: 10 coalesceable: 10 coalesced: 10
358 moves: 375 coalesceable: 141 coalesced: 119
359 moves: 6 coalesceable: 6 coalesced: 6
360 moves: 35 coalesceable: 25 coalesced: 20
361 moves: 10 coalesceable: 10 coalesced: 10
362 moves: 1001 coalesceable: 448 coalesced: 387
363 moves: 6 coalesceable: 6 coalesced: 6
364 moves: 162 coalesceable: 92 coalesced: 88
365 moves: 33 coalesceable: 25 coalesced: 23
366 moves: 33 coalesceable: 25 coalesced: 23
367 moves: 12 coalesceable: 12 coalesced: 12
368 moves: 2015 coalesceable: 1063 coalesced: 797
369 moves: 6 coalesceable: 6 coalesced: 6
370 moves: 690 coalesceable: 353 coalesced: 200
371 moves: 4 coalesceable: 4 coalesced: 4
372 moves: 266 coalesceable: 170 coalesced: 166
373 moves: 6 coalesceable: 6 coalesced: 6
374 moves: 570 coalesceable: 359 coalesced: 352
375 moves: 4 coalesceable: 4 coalesced: 4
376 moves: 47 coalesceable: 39 coalesced: 39
runtime: 21.5s, gctime: 0.28879s, systime: 0.11330s.
external oracle real: 21.6s
external oracle size: 198885
apply colour (par) eval: runtime: 3m58s, gctime: 17.9s, systime: 6.9s.
apply colour (par) real: 1m52s
apply colour (par) size: 850829
check colour eval: runtime: 5.1s, gctime: 0.64471s, systime: 0.07995s.
check colour real: 5.2s
check colour size: 851207
word_to_stack eval: runtime: 3m10s, gctime: 16.6s, systime: 2.9s.
word_to_stack real: 3m13s
word_to_stack size: 675063
stack_rawcall eval: runtime: 1m32s, gctime: 1.8s, systime: 0.57912s.
stack_rawcall real: 1m33s
stack_rawcall size: 666264
stack_alloc (par) eval: runtime: 2m12s, gctime: 3.0s, systime: 1.5s.
stack_alloc (par) real: 48.8s
stack_alloc (par) size: 670251
expand stack_remove_def eval: runtime: 0.07971s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.07978s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 3m43s, gctime: 28.0s, systime: 4.8s.
stack_remove (par) real: 1m51s
stack_remove (par) size: 1121907
stack_names (par) eval: runtime: 1m50s, gctime: 12.9s, systime: 2.2s.
stack_names (par) real: 46.9s
stack_names (par) size: 1158724
stack_to_lab (par) eval: runtime: 3m20s, gctime: 16.5s, systime: 3.6s.
stack_to_lab (par) real: 1m21s
stack_to_lab (par) size: 1427705
lab_to_target eval: runtime: 9m20s, gctime: 19.5s, systime: 10.2s.
lab_to_target real: 9m31s
lab_to_target size: 2321450
export: runtime: 1.2s, gctime: 0.32376s, systime: 0.05672s.
Saved theorem _____ "diff_compiled"
Exporting theory "diffCompile" ... done.
Theory "diffCompile" took 39m12s to build
Linking /root/regression/cakeml-1571/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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: 47.4s, gctime: 1.7s, systime: 0.46704s.
to_flat real: 47.9s
to_flat size: 103100
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.60922s, gctime: 0.04147s, systime: 0.00669s.
to_clos real: 0.61583s
to_clos size: 41653
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 9.2s, gctime: 0.45898s, systime: 0.08331s.
to_bvl real: 9.3s
to_bvl size: 69819
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m33s, gctime: 1.8s, systime: 0.43637s.
to_bvi real: 1m33s
to_bvi size: 75662
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 21.7s, gctime: 1.4s, systime: 0.27336s.
to_data real: 22.0s
to_data size: 124241
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 31.0s, gctime: 1.8s, systime: 0.18328s.
data_to_word real: 31.1s
data_to_word size: 312276
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m29s, gctime: 22.8s, systime: 4.4s.
inst,ssa,two-reg (par) real: 1m26s
inst,ssa,two-reg (par) size: 1254462
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 18.9s, gctime: 1.8s, systime: 1.1s.
get_clash (par) real: 9.0s
get_clash (par) size: 1951150
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: 948 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 10 coalesceable: 6 coalesced: 6
151 moves: 60 coalesceable: 41 coalesced: 40
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: 2 coalesceable: 2 coalesced: 2
158 moves: 17 coalesceable: 11 coalesced: 11
159 moves: 5 coalesceable: 3 coalesced: 3
160 moves: 6 coalesceable: 6 coalesced: 6
161 moves: 29 coalesceable: 19 coalesced: 13
162 moves: 4 coalesceable: 4 coalesced: 4
163 moves: 7 coalesceable: 7 coalesced: 7
164 moves: 4 coalesceable: 4 coalesced: 4
165 moves: 9 coalesceable: 9 coalesced: 8
166 moves: 8 coalesceable: 8 coalesced: 8
167 moves: 124 coalesceable: 72 coalesced: 58
168 moves: 6 coalesceable: 6 coalesced: 6
169 moves: 62 coalesceable: 31 coalesced: 29
170 moves: 8 coalesceable: 8 coalesced: 8
171 moves: 180 coalesceable: 93 coalesced: 89
172 moves: 6 coalesceable: 6 coalesced: 6
173 moves: 7 coalesceable: 7 coalesced: 4
174 moves: 6 coalesceable: 6 coalesced: 6
175 moves: 23 coalesceable: 15 coalesced: 11
176 moves: 6 coalesceable: 6 coalesced: 6
177 moves: 23 coalesceable: 15 coalesced: 11
178 moves: 6 coalesceable: 6 coalesced: 6
179 moves: 30 coalesceable: 19 coalesced: 16
180 moves: 6 coalesceable: 6 coalesced: 6
181 moves: 29 coalesceable: 21 coalesced: 17
182 moves: 6 coalesceable: 6 coalesced: 6
183 moves: 24 coalesceable: 16 coalesced: 13
184 moves: 6 coalesceable: 6 coalesced: 6
185 moves: 24 coalesceable: 16 coalesced: 13
186 moves: 6 coalesceable: 6 coalesced: 6
187 moves: 30 coalesceable: 22 coalesced: 19
188 moves: 4 coalesceable: 4 coalesced: 4
189 moves: 3 coalesceable: 3 coalesced: 3
190 moves: 4 coalesceable: 4 coalesced: 4
191 moves: 25 coalesceable: 18 coalesced: 16
192 moves: 4 coalesceable: 4 coalesced: 4
193 moves: 3 coalesceable: 3 coalesced: 3
194 moves: 6 coalesceable: 6 coalesced: 6
195 moves: 36 coalesceable: 23 coalesced: 17
196 moves: 6 coalesceable: 6 coalesced: 6
197 moves: 21 coalesceable: 19 coalesced: 19
198 moves: 8 coalesceable: 8 coalesced: 8
199 moves: 22 coalesceable: 20 coalesced: 20
200 moves: 12 coalesceable: 12 coalesced: 12
201 moves: 218 coalesceable: 134 coalesced: 94
202 moves: 8 coalesceable: 8 coalesced: 8
203 moves: 124 coalesceable: 72 coalesced: 58
204 moves: 4 coalesceable: 4 coalesced: 4
205 moves: 77 coalesceable: 56 coalesced: 53
206 moves: 6 coalesceable: 6 coalesced: 6
207 moves: 110 coalesceable: 79 coalesced: 69
208 moves: 8 coalesceable: 8 coalesced: 8
209 moves: 407 coalesceable: 208 coalesced: 175
210 moves: 4 coalesceable: 4 coalesced: 4
211 moves: 56 coalesceable: 33 coalesced: 30
212 moves: 4 coalesceable: 4 coalesced: 4
213 moves: 8 coalesceable: 6 coalesced: 6
214 moves: 8 coalesceable: 8 coalesced: 8
215 moves: 163 coalesceable: 110 coalesced: 96
216 moves: 6 coalesceable: 6 coalesced: 6
217 moves: 114 coalesceable: 80 coalesced: 72
218 moves: 4 coalesceable: 4 coalesced: 4
219 moves: 6 coalesceable: 6 coalesced: 6
220 moves: 8 coalesceable: 8 coalesced: 8
221 moves: 128 coalesceable: 77 coalesced: 70
222 moves: 8 coalesceable: 8 coalesced: 8
223 moves: 111 coalesceable: 66 coalesced: 51
224 moves: 6 coalesceable: 6 coalesced: 6
225 moves: 50 coalesceable: 38 coalesced: 35
226 moves: 6 coalesceable: 6 coalesced: 6
227 moves: 427 coalesceable: 263 coalesced: 198
228 moves: 4 coalesceable: 4 coalesced: 4
229 moves: 5 coalesceable: 5 coalesced: 5
230 moves: 4 coalesceable: 4 coalesced: 4
231 moves: 36 coalesceable: 21 coalesced: 19
runtime: 20.3s, gctime: 0.10844s, systime: 0.10668s.
external oracle real: 20.4s
external oracle size: 142021
apply colour (par) eval: runtime: 2m42s, gctime: 8.3s, systime: 3.5s.
apply colour (par) real: 1m40s
apply colour (par) size: 626759
check colour eval: runtime: 9.1s, gctime: 7.2s, systime: 0.93676s.
check colour real: 10.1s
check colour size: 626992
word_to_stack eval: runtime: 2m13s, gctime: 8.3s, systime: 8.1s.
word_to_stack real: 2m21s
word_to_stack size: 512149
stack_rawcall eval: runtime: 1m09s, gctime: 0.91087s, systime: 1.4s.
stack_rawcall real: 1m10s
stack_rawcall size: 505493
stack_alloc (par) eval: runtime: 1m36s, gctime: 1.1s, systime: 9.6s.
stack_alloc (par) real: 52.8s
stack_alloc (par) size: 507162
expand stack_remove_def eval: runtime: 0.08282s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.08288s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m09s, gctime: 1.7s, systime: 4.7s.
stack_remove (par) real: 1m15s
stack_remove (par) size: 866124
stack_names (par) eval: runtime: 1m06s, gctime: 1.3s, systime: 5.2s.
stack_names (par) real: 34.3s
stack_names (par) size: 893873
stack_to_lab (par) eval: runtime: 2m12s, gctime: 2.6s, systime: 3.3s.
stack_to_lab (par) real: 1m05s
stack_to_lab (par) size: 1087668
lab_to_target eval: runtime: 7m16s, gctime: 11.2s, systime: 7.1s.
lab_to_target real: 7m23s
lab_to_target size: 1749273
export: runtime: 0.80410s, gctime: 0.09468s, systime: 0.01336s.
Saved theorem _____ "echo_compiled"
Exporting theory "echoCompile" ... done.
Theory "echoCompile" took 28m28s to build
cc cat.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_cat
cc diff.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_diff
cc echo.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_echo
Linking /root/regression/cakeml-1571/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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: 1m29s, gctime: 1.8s, systime: 1.1s.
to_flat real: 1m30s
to_flat size: 355136
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 5.5s, gctime: 0.26916s, systime: 0.07002s.
to_clos real: 5.5s
to_clos size: 152983
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 32.9s, gctime: 1.2s, systime: 0.31012s.
to_bvl real: 33.2s
to_bvl size: 273519
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 4m04s, gctime: 2.7s, systime: 1.5s.
to_bvi real: 4m06s
to_bvi size: 242916
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 55.9s, gctime: 2.9s, systime: 0.56664s.
to_data real: 56.4s
to_data size: 449246
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 2m12s, gctime: 5.7s, systime: 1.2s.
data_to_word real: 2m13s
data_to_word size: 1269463
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 23m13s, gctime: 2m27s, systime: 40.3s.
inst,ssa,two-reg (par) real: 18m00s
inst,ssa,two-reg (par) size: 4752623
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 1m16s, gctime: 7.3s, systime: 3.6s.
get_clash (par) real: 29.6s
get_clash (par) size: 7259369
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: 204 coalesceable: 2 coalesced: 2
118 moves: 1002 coalesceable: 2 coalesced: 2
119 moves: 17 coalesceable: 12 coalesced: 12
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: 17 coalesceable: 11 coalesced: 11
248 moves: 74 coalesceable: 49 coalesced: 43
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: 17 coalesceable: 11 coalesced: 11
263 moves: 5885 coalesceable: 3532 coalesced: 3033
264 moves: 11474 coalesceable: 7187 coalesced: 6357
265 moves: 10448 coalesceable: 6311 coalesced: 5527
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: 17 coalesceable: 11 coalesced: 11
277 moves: 102 coalesceable: 58 coalesced: 58
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: 17 coalesceable: 11 coalesced: 11
284 moves: 1828 coalesceable: 1001 coalesced: 913
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: 17 coalesceable: 11 coalesced: 11
290 moves: 158 coalesceable: 117 coalesced: 117
291 moves: 17 coalesceable: 11 coalesced: 11
292 moves: 17 coalesceable: 11 coalesced: 11
293 moves: 17 coalesceable: 11 coalesced: 11
294 moves: 17 coalesceable: 11 coalesced: 11
295 moves: 5 coalesceable: 3 coalesced: 3
296 moves: 4 coalesceable: 4 coalesced: 4
297 moves: 6 coalesceable: 6 coalesced: 6
298 moves: 4 coalesceable: 4 coalesced: 4
299 moves: 6 coalesceable: 6 coalesced: 6
300 moves: 8 coalesceable: 8 coalesced: 8
301 moves: 46 coalesceable: 34 coalesced: 33
302 moves: 4 coalesceable: 4 coalesced: 4
303 moves: 3 coalesceable: 3 coalesced: 3
304 moves: 6 coalesceable: 6 coalesced: 6
305 moves: 3 coalesceable: 3 coalesced: 2
306 moves: 8 coalesceable: 8 coalesced: 8
307 moves: 99 coalesceable: 63 coalesced: 50
308 moves: 6 coalesceable: 6 coalesced: 6
309 moves: 7 coalesceable: 7 coalesced: 4
310 moves: 6 coalesceable: 6 coalesced: 6
311 moves: 29 coalesceable: 19 coalesced: 13
312 moves: 8 coalesceable: 8 coalesced: 8
313 moves: 103 coalesceable: 64 coalesced: 59
314 moves: 4 coalesceable: 4 coalesced: 4
315 moves: 7 coalesceable: 7 coalesced: 7
316 moves: 6 coalesceable: 6 coalesced: 6
317 moves: 49 coalesceable: 36 coalesced: 34
318 moves: 6 coalesceable: 6 coalesced: 6
319 moves: 32 coalesceable: 23 coalesced: 18
320 moves: 4 coalesceable: 4 coalesced: 4
321 moves: 5 coalesceable: 5 coalesced: 3
322 moves: 4 coalesceable: 4 coalesced: 4
323 moves: 7 coalesceable: 7 coalesced: 7
324 moves: 6 coalesceable: 6 coalesced: 6
325 moves: 86 coalesceable: 57 coalesced: 51
326 moves: 6 coalesceable: 6 coalesced: 6
327 moves: 76 coalesceable: 47 coalesced: 43
328 moves: 6 coalesceable: 6 coalesced: 6
329 moves: 42 coalesceable: 27 coalesced: 25
330 moves: 4 coalesceable: 4 coalesced: 4
331 moves: 95 coalesceable: 58 coalesced: 57
332 moves: 6 coalesceable: 6 coalesced: 6
333 moves: 49 coalesceable: 37 coalesced: 35
334 moves: 4 coalesceable: 4 coalesced: 4
335 moves: 73 coalesceable: 49 coalesced: 47
336 moves: 6 coalesceable: 6 coalesced: 6
337 moves: 79 coalesceable: 57 coalesced: 54
338 moves: 6 coalesceable: 6 coalesced: 6
339 moves: 42 coalesceable: 27 coalesced: 26
340 moves: 4 coalesceable: 4 coalesced: 4
341 moves: 12 coalesceable: 11 coalesced: 9
342 moves: 4 coalesceable: 4 coalesced: 4
343 moves: 9 coalesceable: 9 coalesced: 8
344 moves: 4 coalesceable: 4 coalesced: 4
345 moves: 29 coalesceable: 12 coalesced: 11
346 moves: 8 coalesceable: 8 coalesced: 8
347 moves: 124 coalesceable: 72 coalesced: 58
348 moves: 6 coalesceable: 6 coalesced: 6
349 moves: 62 coalesceable: 31 coalesced: 29
350 moves: 4 coalesceable: 4 coalesced: 4
351 moves: 48 coalesceable: 23 coalesced: 21
352 moves: 6 coalesceable: 6 coalesced: 6
353 moves: 23 coalesceable: 15 coalesced: 11
354 moves: 6 coalesceable: 6 coalesced: 6
355 moves: 23 coalesceable: 15 coalesced: 11
356 moves: 6 coalesceable: 6 coalesced: 6
357 moves: 30 coalesceable: 19 coalesced: 16
358 moves: 6 coalesceable: 6 coalesced: 6
359 moves: 29 coalesceable: 21 coalesced: 17
360 moves: 6 coalesceable: 6 coalesced: 6
361 moves: 24 coalesceable: 16 coalesced: 13
362 moves: 6 coalesceable: 6 coalesced: 6
363 moves: 24 coalesceable: 16 coalesced: 13
364 moves: 6 coalesceable: 6 coalesced: 6
365 moves: 30 coalesceable: 22 coalesced: 19
366 moves: 6 coalesceable: 6 coalesced: 6
367 moves: 60 coalesceable: 44 coalesced: 41
368 moves: 6 coalesceable: 6 coalesced: 6
369 moves: 62 coalesceable: 31 coalesced: 29
370 moves: 4 coalesceable: 4 coalesced: 4
371 moves: 3 coalesceable: 3 coalesced: 3
372 moves: 4 coalesceable: 4 coalesced: 4
373 moves: 43 coalesceable: 29 coalesced: 25
374 moves: 4 coalesceable: 4 coalesced: 4
375 moves: 25 coalesceable: 18 coalesced: 16
376 moves: 4 coalesceable: 4 coalesced: 4
377 moves: 3 coalesceable: 3 coalesced: 3
378 moves: 6 coalesceable: 6 coalesced: 6
379 moves: 36 coalesceable: 23 coalesced: 17
380 moves: 6 coalesceable: 6 coalesced: 6
381 moves: 21 coalesceable: 19 coalesced: 19
382 moves: 4 coalesceable: 4 coalesced: 4
383 moves: 9 coalesceable: 9 coalesced: 8
384 moves: 8 coalesceable: 8 coalesced: 8
385 moves: 22 coalesceable: 20 coalesced: 20
386 moves: 12 coalesceable: 12 coalesced: 12
387 moves: 218 coalesceable: 134 coalesced: 94
388 moves: 12 coalesceable: 12 coalesced: 12
389 moves: 218 coalesceable: 134 coalesced: 94
390 moves: 8 coalesceable: 8 coalesced: 8
391 moves: 124 coalesceable: 72 coalesced: 58
392 moves: 4 coalesceable: 4 coalesced: 4
393 moves: 77 coalesceable: 56 coalesced: 53
394 moves: 6 coalesceable: 6 coalesced: 6
395 moves: 110 coalesceable: 79 coalesced: 69
396 moves: 8 coalesceable: 8 coalesced: 8
397 moves: 407 coalesceable: 208 coalesced: 175
398 moves: 4 coalesceable: 4 coalesced: 4
399 moves: 56 coalesceable: 33 coalesced: 30
400 moves: 4 coalesceable: 4 coalesced: 4
401 moves: 8 coalesceable: 6 coalesced: 6
402 moves: 8 coalesceable: 8 coalesced: 8
403 moves: 163 coalesceable: 110 coalesced: 96
404 moves: 6 coalesceable: 6 coalesced: 6
405 moves: 114 coalesceable: 80 coalesced: 72
406 moves: 4 coalesceable: 4 coalesced: 4
407 moves: 6 coalesceable: 6 coalesced: 6
408 moves: 4 coalesceable: 4 coalesced: 4
409 moves: 6 coalesceable: 6 coalesced: 6
410 moves: 8 coalesceable: 8 coalesced: 8
411 moves: 128 coalesceable: 77 coalesced: 70
412 moves: 8 coalesceable: 8 coalesced: 8
413 moves: 111 coalesceable: 66 coalesced: 51
414 moves: 6 coalesceable: 6 coalesced: 6
415 moves: 427 coalesceable: 263 coalesced: 198
416 moves: 4 coalesceable: 4 coalesced: 4
417 moves: 5 coalesceable: 5 coalesced: 5
418 moves: 4 coalesceable: 4 coalesced: 4
419 moves: 272 coalesceable: 139 coalesced: 131
420 moves: 4 coalesceable: 4 coalesced: 4
421 moves: 69 coalesceable: 54 coalesced: 54
422 moves: 6 coalesceable: 6 coalesced: 6
423 moves: 78 coalesceable: 59 coalesced: 56
424 moves: 4 coalesceable: 4 coalesced: 4
425 moves: 21 coalesceable: 18 coalesced: 16
426 moves: 4 coalesceable: 4 coalesced: 4
427 moves: 164 coalesceable: 106 coalesced: 89
428 moves: 224 coalesceable: 137 coalesced: 113
429 moves: 217 coalesceable: 133 coalesced: 108
430 moves: 4 coalesceable: 4 coalesced: 4
431 moves: 45 coalesceable: 26 coalesced: 24
432 moves: 6 coalesceable: 6 coalesced: 6
433 moves: 152 coalesceable: 102 coalesced: 97
434 moves: 6 coalesceable: 6 coalesced: 6
435 moves: 847 coalesceable: 556 coalesced: 502
436 moves: 6 coalesceable: 6 coalesced: 6
437 moves: 30 coalesceable: 21 coalesced: 16
438 moves: 4 coalesceable: 4 coalesced: 4
439 moves: 7 coalesceable: 7 coalesced: 7
440 moves: 6 coalesceable: 6 coalesced: 6
441 moves: 30 coalesceable: 17 coalesced: 16
442 moves: 10 coalesceable: 10 coalesced: 10
443 moves: 2844 coalesceable: 1470 coalesced: 781
444 moves: 10 coalesceable: 10 coalesced: 10
445 moves: 2803 coalesceable: 1454 coalesced: 770
446 moves: 4 coalesceable: 4 coalesced: 4
447 moves: 150 coalesceable: 86 coalesced: 76
448 moves: 4 coalesceable: 4 coalesced: 4
449 moves: 4 coalesceable: 4 coalesced: 4
450 moves: 8 coalesceable: 8 coalesced: 8
451 moves: 99 coalesceable: 63 coalesced: 57
452 moves: 8 coalesceable: 8 coalesced: 8
453 moves: 72 coalesceable: 48 coalesced: 44
454 moves: 10 coalesceable: 10 coalesced: 10
455 moves: 195 coalesceable: 104 coalesced: 68
456 moves: 8 coalesceable: 8 coalesced: 8
457 moves: 74 coalesceable: 47 coalesced: 43
458 moves: 6 coalesceable: 6 coalesced: 6
459 moves: 58 coalesceable: 40 coalesced: 33
460 moves: 6 coalesceable: 6 coalesced: 6
461 moves: 634 coalesceable: 440 coalesced: 316
462 moves: 6 coalesceable: 6 coalesced: 6
463 moves: 15 coalesceable: 15 coalesced: 15
464 moves: 4 coalesceable: 4 coalesced: 4
465 moves: 321 coalesceable: 204 coalesced: 200
466 moves: 8 coalesceable: 8 coalesced: 8
467 moves: 107 coalesceable: 65 coalesced: 65
468 moves: 10 coalesceable: 10 coalesced: 10
469 moves: 514 coalesceable: 292 coalesced: 271
470 moves: 4 coalesceable: 4 coalesced: 4
471 moves: 26 coalesceable: 19 coalesced: 17
472 moves: 8 coalesceable: 8 coalesced: 8
473 moves: 256 coalesceable: 149 coalesced: 130
474 moves: 8 coalesceable: 8 coalesced: 8
475 moves: 789 coalesceable: 475 coalesced: 427
476 moves: 6 coalesceable: 6 coalesced: 6
477 moves: 37 coalesceable: 23 coalesced: 22
478 moves: 4 coalesceable: 4 coalesced: 4
479 moves: 201 coalesceable: 119 coalesced: 113
480 moves: 6 coalesceable: 6 coalesced: 6
481 moves: 220 coalesceable: 158 coalesced: 129
482 moves: 4 coalesceable: 4 coalesced: 4
483 moves: 477 coalesceable: 295 coalesced: 290
484 moves: 6 coalesceable: 6 coalesced: 6
485 moves: 16 coalesceable: 9 coalesced: 6
486 moves: 6 coalesceable: 6 coalesced: 6
487 moves: 42 coalesceable: 26 coalesced: 25
488 moves: 4 coalesceable: 4 coalesced: 4
489 moves: 208 coalesceable: 121 coalesced: 117
490 moves: 4 coalesceable: 4 coalesced: 4
491 moves: 419 coalesceable: 260 coalesced: 230
492 moves: 4 coalesceable: 4 coalesced: 4
493 moves: 21 coalesceable: 14 coalesced: 13
494 moves: 6 coalesceable: 6 coalesced: 6
495 moves: 188 coalesceable: 117 coalesced: 112
496 moves: 6 coalesceable: 6 coalesced: 6
497 moves: 161 coalesceable: 117 coalesced: 95
498 moves: 4 coalesceable: 4 coalesced: 4
499 moves: 156 coalesceable: 103 coalesced: 98
500 moves: 4 coalesceable: 4 coalesced: 4
501 moves: 138 coalesceable: 92 coalesced: 88
502 moves: 4 coalesceable: 4 coalesced: 4
503 moves: 4 coalesceable: 4 coalesced: 4
504 moves: 4 coalesceable: 4 coalesced: 4
505 moves: 100 coalesceable: 64 coalesced: 61
506 moves: 6 coalesceable: 6 coalesced: 6
507 moves: 7 coalesceable: 7 coalesced: 7
508 moves: 10 coalesceable: 10 coalesced: 10
509 moves: 70 coalesceable: 61 coalesced: 55
510 moves: 4 coalesceable: 4 coalesced: 4
511 moves: 174 coalesceable: 110 coalesced: 105
512 moves: 4 coalesceable: 4 coalesced: 4
513 moves: 23 coalesceable: 15 coalesced: 14
514 moves: 9 coalesceable: 9 coalesced: 9
515 moves: 6 coalesceable: 6 coalesced: 6
516 moves: 232 coalesceable: 126 coalesced: 117
517 moves: 37 coalesceable: 23 coalesced: 20
518 moves: 4 coalesceable: 4 coalesced: 4
519 moves: 25 coalesceable: 16 coalesced: 14
520 moves: 10 coalesceable: 10 coalesced: 10
521 moves: 224 coalesceable: 128 coalesced: 94
522 moves: 8 coalesceable: 8 coalesced: 8
523 moves: 282 coalesceable: 163 coalesced: 151
524 moves: 8 coalesceable: 8 coalesced: 8
525 moves: 52 coalesceable: 37 coalesced: 31
526 moves: 6 coalesceable: 6 coalesced: 6
527 moves: 8 coalesceable: 8 coalesced: 6
528 moves: 6 coalesceable: 6 coalesced: 6
529 moves: 11 coalesceable: 11 coalesced: 9
530 moves: 10 coalesceable: 10 coalesced: 10
531 moves: 405 coalesceable: 209 coalesced: 162
532 moves: 10 coalesceable: 10 coalesced: 10
533 moves: 1186 coalesceable: 706 coalesced: 410
534 moves: 10 coalesceable: 10 coalesced: 10
535 moves: 96 coalesceable: 62 coalesced: 53
536 moves: 6 coalesceable: 6 coalesced: 6
537 moves: 24 coalesceable: 16 coalesced: 13
538 moves: 4 coalesceable: 4 coalesced: 4
539 moves: 36 coalesceable: 24 coalesced: 23
540 moves: 6 coalesceable: 6 coalesced: 6
541 moves: 24 coalesceable: 16 coalesced: 13
542 moves: 4 coalesceable: 4 coalesced: 4
543 moves: 147 coalesceable: 73 coalesced: 54
544 moves: 4 coalesceable: 4 coalesced: 4
545 moves: 89 coalesceable: 54 coalesced: 47
546 moves: 4 coalesceable: 4 coalesced: 4
547 moves: 22 coalesceable: 14 coalesced: 13
548 moves: 6 coalesceable: 6 coalesced: 6
549 moves: 40 coalesceable: 23 coalesced: 19
550 moves: 8 coalesceable: 8 coalesced: 8
551 moves: 64 coalesceable: 35 coalesced: 33
552 moves: 6 coalesceable: 6 coalesced: 6
553 moves: 24 coalesceable: 16 coalesced: 13
554 moves: 4 coalesceable: 4 coalesced: 4
555 moves: 59 coalesceable: 34 coalesced: 31
556 moves: 4 coalesceable: 4 coalesced: 4
557 moves: 252 coalesceable: 137 coalesced: 115
558 moves: 4 coalesceable: 4 coalesced: 4
559 moves: 18 coalesceable: 10 coalesced: 10
560 moves: 6 coalesceable: 6 coalesced: 6
561 moves: 148 coalesceable: 60 coalesced: 56
562 moves: 4 coalesceable: 4 coalesced: 4
563 moves: 6 coalesceable: 6 coalesced: 6
564 moves: 4 coalesceable: 4 coalesced: 4
565 moves: 6 coalesceable: 6 coalesced: 6
566 moves: 6 coalesceable: 6 coalesced: 6
567 moves: 86 coalesceable: 55 coalesced: 53
568 moves: 6 coalesceable: 6 coalesced: 6
569 moves: 77 coalesceable: 49 coalesced: 44
570 moves: 4 coalesceable: 4 coalesced: 4
571 moves: 21 coalesceable: 14 coalesced: 13
572 moves: 4 coalesceable: 4 coalesced: 4
573 moves: 21 coalesceable: 14 coalesced: 13
574 moves: 1595 coalesceable: 918 coalesced: 834
575 moves: 4 coalesceable: 4 coalesced: 4
576 moves: 10 coalesceable: 9 coalesced: 9
577 moves: 6 coalesceable: 6 coalesced: 6
578 moves: 40 coalesceable: 25 coalesced: 24
579 moves: 14 coalesceable: 14 coalesced: 14
580 moves: 79 coalesceable: 47 coalesced: 41
581 moves: 4 coalesceable: 4 coalesced: 4
582 moves: 18 coalesceable: 16 coalesced: 16
583 moves: 4 coalesceable: 4 coalesced: 4
584 moves: 158 coalesceable: 90 coalesced: 87
585 moves: 4 coalesceable: 4 coalesced: 4
586 moves: 111 coalesceable: 80 coalesced: 77
587 moves: 4 coalesceable: 4 coalesced: 4
588 moves: 30 coalesceable: 19 coalesced: 18
589 moves: 4 coalesceable: 4 coalesced: 4
590 moves: 17 coalesceable: 15 coalesced: 15
591 moves: 4 coalesceable: 4 coalesced: 4
592 moves: 12 coalesceable: 11 coalesced: 11
593 moves: 4 coalesceable: 4 coalesced: 4
594 moves: 69 coalesceable: 40 coalesced: 39
595 moves: 6 coalesceable: 6 coalesced: 6
596 moves: 3 coalesceable: 3 coalesced: 2
597 moves: 6 coalesceable: 6 coalesced: 6
598 moves: 37 coalesceable: 22 coalesced: 21
599 moves: 6 coalesceable: 6 coalesced: 6
600 moves: 3 coalesceable: 3 coalesced: 3
601 moves: 6 coalesceable: 6 coalesced: 6
602 moves: 37 coalesceable: 22 coalesced: 21
603 moves: 4 coalesceable: 4 coalesced: 4
604 moves: 55 coalesceable: 35 coalesced: 31
605 moves: 6 coalesceable: 6 coalesced: 6
606 moves: 23 coalesceable: 21 coalesced: 21
607 moves: 4 coalesceable: 4 coalesced: 4
608 moves: 25 coalesceable: 17 coalesced: 16
609 moves: 4 coalesceable: 4 coalesced: 4
610 moves: 77 coalesceable: 51 coalesced: 48
611 moves: 6 coalesceable: 6 coalesced: 6
612 moves: 20 coalesceable: 18 coalesced: 14
613 moves: 38 coalesceable: 25 coalesced: 24
614 moves: 79 coalesceable: 50 coalesced: 47
615 moves: 6 coalesceable: 6 coalesced: 6
616 moves: 85 coalesceable: 57 coalesced: 54
617 moves: 4 coalesceable: 4 coalesced: 4
618 moves: 40 coalesceable: 25 coalesced: 24
619 moves: 6 coalesceable: 6 coalesced: 6
620 moves: 26 coalesceable: 19 coalesced: 19
621 moves: 4 coalesceable: 4 coalesced: 4
622 moves: 21 coalesceable: 14 coalesced: 13
623 moves: 4 coalesceable: 4 coalesced: 4
624 moves: 53 coalesceable: 34 coalesced: 32
625 moves: 167 coalesceable: 107 coalesced: 107
626 moves: 37 coalesceable: 26 coalesced: 25
627 moves: 6 coalesceable: 6 coalesced: 6
628 moves: 34 coalesceable: 23 coalesced: 21
629 moves: 4 coalesceable: 4 coalesced: 4
630 moves: 5 coalesceable: 5 coalesced: 5
631 moves: 38 coalesceable: 25 coalesced: 24
632 moves: 110 coalesceable: 74 coalesced: 72
633 moves: 6 coalesceable: 6 coalesced: 6
634 moves: 34 coalesceable: 23 coalesced: 21
635 moves: 32 coalesceable: 22 coalesced: 22
636 moves: 102 coalesceable: 69 coalesced: 67
637 moves: 6 coalesceable: 6 coalesced: 6
638 moves: 34 coalesceable: 23 coalesced: 21
639 moves: 4 coalesceable: 4 coalesced: 4
640 moves: 5 coalesceable: 5 coalesced: 5
641 moves: 4 coalesceable: 4 coalesced: 4
642 moves: 21 coalesceable: 14 coalesced: 13
643 moves: 4 coalesceable: 4 coalesced: 4
644 moves: 132 coalesceable: 89 coalesced: 80
645 moves: 4 coalesceable: 4 coalesced: 4
646 moves: 88 coalesceable: 59 coalesced: 56
647 moves: 4 coalesceable: 4 coalesced: 4
648 moves: 29 coalesceable: 23 coalesced: 21
649 moves: 4 coalesceable: 4 coalesced: 4
650 moves: 49 coalesceable: 37 coalesced: 37
651 moves: 4 coalesceable: 4 coalesced: 4
652 moves: 5 coalesceable: 5 coalesced: 5
653 moves: 4 coalesceable: 4 coalesced: 4
654 moves: 49 coalesceable: 37 coalesced: 37
655 moves: 4 coalesceable: 4 coalesced: 4
656 moves: 5 coalesceable: 5 coalesced: 5
657 moves: 4 coalesceable: 4 coalesced: 4
658 moves: 5 coalesceable: 5 coalesced: 5
659 moves: 4 coalesceable: 4 coalesced: 4
660 moves: 5 coalesceable: 5 coalesced: 5
661 moves: 4 coalesceable: 4 coalesced: 4
662 moves: 5 coalesceable: 5 coalesced: 5
663 moves: 4 coalesceable: 4 coalesced: 4
664 moves: 5 coalesceable: 5 coalesced: 5
665 moves: 4 coalesceable: 4 coalesced: 4
666 moves: 5 coalesceable: 5 coalesced: 5
667 moves: 4 coalesceable: 4 coalesced: 4
668 moves: 51 coalesceable: 29 coalesced: 28
669 moves: 4 coalesceable: 4 coalesced: 4
670 moves: 108 coalesceable: 74 coalesced: 72
671 moves: 8 coalesceable: 8 coalesced: 8
672 moves: 99 coalesceable: 51 coalesced: 48
673 moves: 4 coalesceable: 4 coalesced: 4
674 moves: 266 coalesceable: 170 coalesced: 166
675 moves: 6 coalesceable: 6 coalesced: 6
676 moves: 503 coalesceable: 392 coalesced: 384
677 moves: 125 coalesceable: 50 coalesced: 45
678 moves: 4 coalesceable: 4 coalesced: 4
679 moves: 210 coalesceable: 128 coalesced: 124
680 moves: 6 coalesceable: 6 coalesced: 6
681 moves: 14 coalesceable: 12 coalesced: 12
682 moves: 6 coalesceable: 6 coalesced: 6
683 moves: 35 coalesceable: 25 coalesced: 22
684 moves: 38 coalesceable: 28 coalesced: 23
685 moves: 4 coalesceable: 4 coalesced: 4
686 moves: 302 coalesceable: 186 coalesced: 181
runtime: 11m24s, gctime: 0.84256s, systime: 3.1s.
external oracle real: 11m27s
external oracle size: 553121
apply colour (par) eval: runtime: 11m23s, gctime: 1m06s, systime: 20.1s.
apply colour (par) real: 5m18s
apply colour (par) size: 2110935
check colour eval: runtime: 49.9s, gctime: 22.8s, systime: 3.1s.
check colour real: 53.0s
check colour size: 2111623
word_to_stack eval: runtime: 6m10s, gctime: 7.2s, systime: 7.2s.
word_to_stack real: 6m17s
word_to_stack size: 1648861
stack_rawcall eval: runtime: 3m44s, gctime: 3.5s, systime: 3.7s.
stack_rawcall real: 3m47s
stack_rawcall size: 1635829
stack_alloc (par) eval: runtime: 5m27s, gctime: 4.5s, systime: 11.9s.
stack_alloc (par) real: 2m00s
stack_alloc (par) size: 1651709
expand stack_remove_def eval: runtime: 0.07598s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.07603s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 6m44s, gctime: 5.9s, systime: 7.8s.
stack_remove (par) real: 2m06s
stack_remove (par) size: 2712381
stack_names (par) eval: runtime: 3m48s, gctime: 6.7s, systime: 5.3s.
stack_names (par) real: 1m25s
stack_names (par) size: 2803247
stack_to_lab (par) eval: runtime: 8m26s, gctime: 53.0s, systime: 12.2s.
stack_to_lab (par) real: 3m35s
stack_to_lab (par) size: 3424167
lab_to_target eval: runtime: 17m36s, gctime: 39.8s, systime: 28.7s.
lab_to_target real: 18m04s
lab_to_target size: 5124391
export: runtime: 1.7s, gctime: 0.49722s, systime: 0.09002s.
Saved theorem _____ "grep_compiled"
Exporting theory "grepCompile" ... done.
Theory "grepCompile" took 1h52m59s to build
cc grep.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_grep
Linking /root/regression/cakeml-1571/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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: 46.6s, gctime: 1.5s, systime: 0.40063s.
to_flat real: 47.0s
to_flat size: 91672
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.39328s, gctime: 0.00000s, systime: 0.02333s.
to_clos real: 0.41658s
to_clos size: 34549
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 8.1s, gctime: 0.33171s, systime: 0.09355s.
to_bvl real: 8.2s
to_bvl size: 56478
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m27s, gctime: 1.3s, systime: 0.47988s.
to_bvi real: 1m28s
to_bvi size: 64296
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 21.2s, gctime: 1.2s, systime: 0.26339s.
to_data real: 21.4s
to_data size: 112556
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 29.0s, gctime: 1.4s, systime: 0.27014s.
data_to_word real: 29.3s
data_to_word size: 297398
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m07s, gctime: 9.3s, systime: 6.3s.
inst,ssa,two-reg (par) real: 1m11s
inst,ssa,two-reg (par) size: 1201172
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 34.8s, gctime: 16.8s, systime: 5.7s.
get_clash (par) real: 28.1s
get_clash (par) size: 1870124
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: 948 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 10 coalesceable: 6 coalesced: 6
138 moves: 60 coalesceable: 41 coalesced: 40
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: 2 coalesceable: 2 coalesced: 2
144 moves: 17 coalesceable: 11 coalesced: 11
145 moves: 5 coalesceable: 3 coalesced: 3
146 moves: 4 coalesceable: 4 coalesced: 4
147 moves: 9 coalesceable: 9 coalesced: 8
148 moves: 8 coalesceable: 8 coalesced: 8
149 moves: 124 coalesceable: 72 coalesced: 58
150 moves: 6 coalesceable: 6 coalesced: 6
151 moves: 23 coalesceable: 15 coalesced: 11
152 moves: 6 coalesceable: 6 coalesced: 6
153 moves: 23 coalesceable: 15 coalesced: 11
154 moves: 6 coalesceable: 6 coalesced: 6
155 moves: 30 coalesceable: 19 coalesced: 16
156 moves: 6 coalesceable: 6 coalesced: 6
157 moves: 29 coalesceable: 21 coalesced: 17
158 moves: 6 coalesceable: 6 coalesced: 6
159 moves: 24 coalesceable: 16 coalesced: 13
160 moves: 6 coalesceable: 6 coalesced: 6
161 moves: 24 coalesceable: 16 coalesced: 13
162 moves: 6 coalesceable: 6 coalesced: 6
163 moves: 30 coalesceable: 22 coalesced: 19
164 moves: 4 coalesceable: 4 coalesced: 4
165 moves: 25 coalesceable: 18 coalesced: 16
166 moves: 4 coalesceable: 4 coalesced: 4
167 moves: 3 coalesceable: 3 coalesced: 3
168 moves: 6 coalesceable: 6 coalesced: 6
169 moves: 21 coalesceable: 19 coalesced: 19
170 moves: 8 coalesceable: 8 coalesced: 8
171 moves: 22 coalesceable: 20 coalesced: 20
172 moves: 12 coalesceable: 12 coalesced: 12
173 moves: 218 coalesceable: 134 coalesced: 94
174 moves: 8 coalesceable: 8 coalesced: 8
175 moves: 163 coalesceable: 110 coalesced: 96
176 moves: 6 coalesceable: 6 coalesced: 6
177 moves: 114 coalesceable: 80 coalesced: 72
178 moves: 4 coalesceable: 4 coalesced: 4
179 moves: 6 coalesceable: 6 coalesced: 6
180 moves: 8 coalesceable: 8 coalesced: 8
181 moves: 128 coalesceable: 77 coalesced: 70
182 moves: 8 coalesceable: 8 coalesced: 8
183 moves: 111 coalesceable: 66 coalesced: 51
184 moves: 6 coalesceable: 6 coalesced: 6
185 moves: 427 coalesceable: 263 coalesced: 198
186 moves: 4 coalesceable: 4 coalesced: 4
187 moves: 5 coalesceable: 5 coalesced: 5
188 moves: 4 coalesceable: 4 coalesced: 4
189 moves: 64 coalesceable: 47 coalesced: 47
runtime: 18.5s, gctime: 0.03987s, systime: 0.47351s.
external oracle real: 19.0s
external oracle size: 134064
apply colour (par) eval: runtime: 2m30s, gctime: 4.2s, systime: 12.1s.
apply colour (par) real: 1m39s
apply colour (par) size: 593983
check colour eval: runtime: 2.0s, gctime: 0.32959s, systime: 0.20005s.
check colour real: 2.2s
check colour size: 594174
word_to_stack eval: runtime: 2m00s, gctime: 2.1s, systime: 2.3s.
word_to_stack real: 2m02s
word_to_stack size: 488265
stack_rawcall eval: runtime: 1m05s, gctime: 0.98847s, systime: 0.77616s.
stack_rawcall real: 1m06s
stack_rawcall size: 482167
stack_alloc (par) eval: runtime: 1m32s, gctime: 1.2s, systime: 8.6s.
stack_alloc (par) real: 50.3s
stack_alloc (par) size: 483449
expand stack_remove_def eval: runtime: 0.09210s, gctime: 0.00000s, systime: 0.03010s.
expand stack_remove_def real: 0.12207s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m03s, gctime: 1.6s, systime: 7.5s.
stack_remove (par) real: 1m15s
stack_remove (par) size: 828276
stack_names (par) eval: runtime: 1m02s, gctime: 1.3s, systime: 3.5s.
stack_names (par) real: 33.4s
stack_names (par) size: 854839
stack_to_lab (par) eval: runtime: 2m07s, gctime: 2.6s, systime: 6.5s.
stack_to_lab (par) real: 1m07s
stack_to_lab (par) size: 1037590
lab_to_target eval: runtime: 6m55s, gctime: 12.0s, systime: 4.0s.
lab_to_target real: 7m00s
lab_to_target size: 1660937
export: runtime: 0.82599s, gctime: 0.14290s, systime: 0.01346s.
Saved theorem _____ "hello_compiled"
Exporting theory "helloCompile" ... done.
Theory "helloCompile" took 27m03s to build
cc hello.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_hello
Linking /root/regression/cakeml-1571/examples/compilation/x64/helloErrCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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: 47.5s, gctime: 1.7s, systime: 0.22737s.
to_flat real: 47.7s
to_flat size: 92707
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.40416s, gctime: 0.00000s, systime: 0.00337s.
to_clos real: 0.40749s
to_clos size: 35208
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 8.3s, gctime: 0.37963s, systime: 0.07996s.
to_bvl real: 8.4s
to_bvl size: 58125
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m28s, gctime: 1.7s, systime: 0.47075s.
to_bvi real: 1m28s
to_bvi size: 65895
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 21.7s, gctime: 1.5s, systime: 0.13656s.
to_data real: 21.8s
to_data size: 114589
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 30.0s, gctime: 1.6s, systime: 0.21016s.
data_to_word real: 30.2s
data_to_word size: 300447
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m24s, gctime: 20.6s, systime: 6.6s.
inst,ssa,two-reg (par) real: 1m26s
inst,ssa,two-reg (par) size: 1209089
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 18.0s, gctime: 1.7s, systime: 2.3s.
get_clash (par) real: 9.2s
get_clash (par) size: 1880965
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: 948 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 10 coalesceable: 6 coalesced: 6
140 moves: 60 coalesceable: 41 coalesced: 40
141 moves: 60 coalesceable: 41 coalesced: 40
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: 2 coalesceable: 2 coalesced: 2
147 moves: 17 coalesceable: 11 coalesced: 11
148 moves: 5 coalesceable: 3 coalesced: 3
149 moves: 4 coalesceable: 4 coalesced: 4
150 moves: 69 coalesceable: 44 coalesced: 38
151 moves: 4 coalesceable: 4 coalesced: 4
152 moves: 3 coalesceable: 3 coalesced: 3
153 moves: 4 coalesceable: 4 coalesced: 4
154 moves: 9 coalesceable: 9 coalesced: 8
155 moves: 8 coalesceable: 8 coalesced: 8
156 moves: 124 coalesceable: 72 coalesced: 58
157 moves: 6 coalesceable: 6 coalesced: 6
158 moves: 23 coalesceable: 15 coalesced: 11
159 moves: 6 coalesceable: 6 coalesced: 6
160 moves: 23 coalesceable: 15 coalesced: 11
161 moves: 6 coalesceable: 6 coalesced: 6
162 moves: 30 coalesceable: 19 coalesced: 16
163 moves: 6 coalesceable: 6 coalesced: 6
164 moves: 29 coalesceable: 21 coalesced: 17
165 moves: 6 coalesceable: 6 coalesced: 6
166 moves: 24 coalesceable: 16 coalesced: 13
167 moves: 6 coalesceable: 6 coalesced: 6
168 moves: 24 coalesceable: 16 coalesced: 13
169 moves: 6 coalesceable: 6 coalesced: 6
170 moves: 30 coalesceable: 22 coalesced: 19
171 moves: 4 coalesceable: 4 coalesced: 4
172 moves: 25 coalesceable: 18 coalesced: 16
173 moves: 4 coalesceable: 4 coalesced: 4
174 moves: 3 coalesceable: 3 coalesced: 3
175 moves: 6 coalesceable: 6 coalesced: 6
176 moves: 21 coalesceable: 19 coalesced: 19
177 moves: 8 coalesceable: 8 coalesced: 8
178 moves: 22 coalesceable: 20 coalesced: 20
179 moves: 12 coalesceable: 12 coalesced: 12
180 moves: 218 coalesceable: 134 coalesced: 94
181 moves: 8 coalesceable: 8 coalesced: 8
182 moves: 163 coalesceable: 110 coalesced: 96
183 moves: 6 coalesceable: 6 coalesced: 6
184 moves: 114 coalesceable: 80 coalesced: 72
185 moves: 4 coalesceable: 4 coalesced: 4
186 moves: 6 coalesceable: 6 coalesced: 6
187 moves: 8 coalesceable: 8 coalesced: 8
188 moves: 128 coalesceable: 77 coalesced: 70
189 moves: 8 coalesceable: 8 coalesced: 8
190 moves: 111 coalesceable: 66 coalesced: 51
191 moves: 6 coalesceable: 6 coalesced: 6
192 moves: 427 coalesceable: 263 coalesced: 198
193 moves: 4 coalesceable: 4 coalesced: 4
194 moves: 5 coalesceable: 5 coalesced: 5
195 moves: 4 coalesceable: 4 coalesced: 4
196 moves: 71 coalesceable: 51 coalesced: 51
runtime: 18.3s, gctime: 0.05906s, systime: 0.01658s.
external oracle real: 18.3s
external oracle size: 135200
apply colour (par) eval: runtime: 2m46s, gctime: 16.4s, systime: 6.9s.
apply colour (par) real: 1m53s
apply colour (par) size: 599070
check colour eval: runtime: 1.8s, gctime: 0.26832s, systime: 0.06337s.
check colour real: 1.9s
check colour size: 599268
word_to_stack eval: runtime: 2m01s, gctime: 3.3s, systime: 0.92640s.
word_to_stack real: 2m02s
word_to_stack size: 491964
stack_rawcall eval: runtime: 1m06s, gctime: 1.3s, systime: 0.35989s.
stack_rawcall real: 1m06s
stack_rawcall size: 485777
stack_alloc (par) eval: runtime: 1m30s, gctime: 1.7s, systime: 3.0s.
stack_alloc (par) real: 47.1s
stack_alloc (par) size: 487119
expand stack_remove_def eval: runtime: 0.07554s, gctime: 0.00000s, systime: 0.00330s.
expand stack_remove_def real: 0.07890s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m24s, gctime: 14.6s, systime: 4.4s.
stack_remove (par) real: 1m33s
stack_remove (par) size: 833749
stack_names (par) eval: runtime: 1m05s, gctime: 2.5s, systime: 2.5s.
stack_names (par) real: 34.2s
stack_names (par) size: 860534
stack_to_lab (par) eval: runtime: 2m33s, gctime: 22.0s, systime: 4.6s.
stack_to_lab (par) real: 1m28s
stack_to_lab (par) size: 1044687
lab_to_target eval: runtime: 7m39s, gctime: 49.2s, systime: 7.5s.
lab_to_target real: 7m47s
lab_to_target size: 1672970
export: runtime: 0.67445s, gctime: 0.00000s, systime: 0.00003s.
Saved theorem _____ "helloErr_compiled"
Exporting theory "helloErrCompile" ... done.
Theory "helloErrCompile" took 28m36s to build
cc helloErr.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_helloErr
Linking /root/regression/cakeml-1571/examples/compilation/x64/iocatCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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 "iocatCompile">>
to_flat eval: runtime: 47.0s, gctime: 1.1s, systime: 0.82045s.
to_flat real: 47.8s
to_flat size: 105258
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.80069s, gctime: 0.16304s, systime: 0.02003s.
to_clos real: 0.82073s
to_clos size: 42782
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 9.5s, gctime: 0.31479s, systime: 0.10982s.
to_bvl real: 9.6s
to_bvl size: 74503
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m35s, gctime: 0.78887s, systime: 0.67661s.
to_bvi real: 1m36s
to_bvi size: 79326
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 21.6s, gctime: 1.0s, systime: 0.21344s.
to_data real: 21.8s
to_data size: 128094
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 30.9s, gctime: 1.2s, systime: 0.35988s.
data_to_word real: 31.3s
data_to_word size: 318955
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m15s, gctime: 5.6s, systime: 9.4s.
inst,ssa,two-reg (par) real: 1m09s
inst,ssa,two-reg (par) size: 1276591
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 19.8s, gctime: 2.1s, systime: 0.48399s.
get_clash (par) real: 8.7s
get_clash (par) size: 1983424
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: 950 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 10 coalesceable: 6 coalesced: 6
153 moves: 60 coalesceable: 41 coalesced: 40
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: 2 coalesceable: 2 coalesced: 2
163 moves: 17 coalesceable: 11 coalesced: 11
164 moves: 17 coalesceable: 11 coalesced: 11
165 moves: 5 coalesceable: 3 coalesced: 3
166 moves: 6 coalesceable: 6 coalesced: 6
167 moves: 29 coalesceable: 19 coalesced: 13
168 moves: 4 coalesceable: 4 coalesced: 4
169 moves: 7 coalesceable: 7 coalesced: 7
170 moves: 4 coalesceable: 4 coalesced: 4
171 moves: 9 coalesceable: 9 coalesced: 8
172 moves: 8 coalesceable: 8 coalesced: 8
173 moves: 124 coalesceable: 72 coalesced: 58
174 moves: 6 coalesceable: 6 coalesced: 6
175 moves: 62 coalesceable: 31 coalesced: 29
176 moves: 4 coalesceable: 4 coalesced: 4
177 moves: 48 coalesceable: 23 coalesced: 21
178 moves: 6 coalesceable: 6 coalesced: 6
179 moves: 23 coalesceable: 15 coalesced: 11
180 moves: 6 coalesceable: 6 coalesced: 6
181 moves: 23 coalesceable: 15 coalesced: 11
182 moves: 6 coalesceable: 6 coalesced: 6
183 moves: 30 coalesceable: 19 coalesced: 16
184 moves: 6 coalesceable: 6 coalesced: 6
185 moves: 29 coalesceable: 21 coalesced: 17
186 moves: 6 coalesceable: 6 coalesced: 6
187 moves: 24 coalesceable: 16 coalesced: 13
188 moves: 6 coalesceable: 6 coalesced: 6
189 moves: 24 coalesceable: 16 coalesced: 13
190 moves: 6 coalesceable: 6 coalesced: 6
191 moves: 30 coalesceable: 22 coalesced: 19
192 moves: 6 coalesceable: 6 coalesced: 6
193 moves: 60 coalesceable: 44 coalesced: 41
194 moves: 6 coalesceable: 6 coalesced: 6
195 moves: 62 coalesceable: 31 coalesced: 29
196 moves: 4 coalesceable: 4 coalesced: 4
197 moves: 43 coalesceable: 29 coalesced: 25
198 moves: 4 coalesceable: 4 coalesced: 4
199 moves: 25 coalesceable: 18 coalesced: 16
200 moves: 4 coalesceable: 4 coalesced: 4
201 moves: 3 coalesceable: 3 coalesced: 3
202 moves: 6 coalesceable: 6 coalesced: 6
203 moves: 36 coalesceable: 23 coalesced: 17
204 moves: 6 coalesceable: 6 coalesced: 6
205 moves: 21 coalesceable: 19 coalesced: 19
206 moves: 8 coalesceable: 8 coalesced: 8
207 moves: 22 coalesceable: 20 coalesced: 20
208 moves: 12 coalesceable: 12 coalesced: 12
209 moves: 218 coalesceable: 134 coalesced: 94
210 moves: 8 coalesceable: 8 coalesced: 8
211 moves: 124 coalesceable: 72 coalesced: 58
212 moves: 4 coalesceable: 4 coalesced: 4
213 moves: 77 coalesceable: 56 coalesced: 53
214 moves: 6 coalesceable: 6 coalesced: 6
215 moves: 110 coalesceable: 79 coalesced: 69
216 moves: 8 coalesceable: 8 coalesced: 8
217 moves: 407 coalesceable: 208 coalesced: 175
218 moves: 4 coalesceable: 4 coalesced: 4
219 moves: 56 coalesceable: 33 coalesced: 30
220 moves: 4 coalesceable: 4 coalesced: 4
221 moves: 8 coalesceable: 6 coalesced: 6
222 moves: 8 coalesceable: 8 coalesced: 8
223 moves: 163 coalesceable: 110 coalesced: 96
224 moves: 6 coalesceable: 6 coalesced: 6
225 moves: 114 coalesceable: 80 coalesced: 72
226 moves: 4 coalesceable: 4 coalesced: 4
227 moves: 6 coalesceable: 6 coalesced: 6
228 moves: 4 coalesceable: 4 coalesced: 4
229 moves: 6 coalesceable: 6 coalesced: 6
230 moves: 8 coalesceable: 8 coalesced: 8
231 moves: 128 coalesceable: 77 coalesced: 70
232 moves: 8 coalesceable: 8 coalesced: 8
233 moves: 111 coalesceable: 66 coalesced: 51
234 moves: 6 coalesceable: 6 coalesced: 6
235 moves: 427 coalesceable: 263 coalesced: 198
236 moves: 4 coalesceable: 4 coalesced: 4
237 moves: 5 coalesceable: 5 coalesced: 5
238 moves: 4 coalesceable: 4 coalesced: 4
239 moves: 272 coalesceable: 139 coalesced: 131
240 moves: 4 coalesceable: 4 coalesced: 4
241 moves: 69 coalesceable: 54 coalesced: 54
242 moves: 6 coalesceable: 6 coalesced: 6
243 moves: 78 coalesceable: 59 coalesced: 56
244 moves: 6 coalesceable: 6 coalesced: 6
245 moves: 31 coalesceable: 17 coalesced: 14
246 moves: 4 coalesceable: 4 coalesced: 4
247 moves: 30 coalesceable: 15 coalesced: 13
248 moves: 4 coalesceable: 4 coalesced: 4
249 moves: 11 coalesceable: 7 coalesced: 7
runtime: 21.0s, gctime: 0.27093s, systime: 0.10657s.
external oracle real: 21.1s
external oracle size: 145281
apply colour (par) eval: runtime: 3m15s, gctime: 25.1s, systime: 17.4s.
apply colour (par) real: 2m09s
apply colour (par) size: 640705
check colour eval: runtime: 2.2s, gctime: 0.33718s, systime: 0.06013s.
check colour real: 2.3s
check colour size: 640956
word_to_stack eval: runtime: 2m08s, gctime: 2.1s, systime: 1.9s.
word_to_stack real: 2m09s
word_to_stack size: 522319
stack_rawcall eval: runtime: 1m10s, gctime: 0.90131s, systime: 0.98606s.
stack_rawcall real: 1m11s
stack_rawcall size: 515360
stack_alloc (par) eval: runtime: 1m39s, gctime: 1.3s, systime: 10.2s.
stack_alloc (par) real: 50.9s
stack_alloc (par) size: 517193
expand stack_remove_def eval: runtime: 0.10210s, gctime: 0.00000s, systime: 0.01677s.
expand stack_remove_def real: 0.11868s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m12s, gctime: 1.6s, systime: 7.5s.
stack_remove (par) real: 1m15s
stack_remove (par) size: 881825
stack_names (par) eval: runtime: 1m08s, gctime: 1.5s, systime: 5.5s.
stack_names (par) real: 35.9s
stack_names (par) size: 910031
stack_to_lab (par) eval: runtime: 2m16s, gctime: 2.6s, systime: 3.6s.
stack_to_lab (par) real: 1m06s
stack_to_lab (par) size: 1108641
lab_to_target eval: runtime: 7m34s, gctime: 12.2s, systime: 4.8s.
lab_to_target real: 7m39s
lab_to_target size: 1784963
export: runtime: 0.92906s, gctime: 0.08223s, systime: 0.11010s.
Saved theorem _____ "iocat_compiled"
Exporting theory "iocatCompile" ... done.
Theory "iocatCompile" took 29m21s to build
cc iocat.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_iocat
Linking /root/regression/cakeml-1571/examples/compilation/x64/patchCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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 "patchCompile">>
to_flat eval: runtime: 53.0s, gctime: 1.4s, systime: 0.82640s.
to_flat real: 53.8s
to_flat size: 160817
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 1.9s, gctime: 0.07289s, systime: 0.04003s.
to_clos real: 2.0s
to_clos size: 68539
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 14.2s, gctime: 0.53434s, systime: 0.23302s.
to_bvl real: 14.4s
to_bvl size: 130971
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 2m04s, gctime: 1.5s, systime: 0.84005s.
to_bvi real: 2m05s
to_bvi size: 125050
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 26.7s, gctime: 1.3s, systime: 0.26332s.
to_data real: 27.0s
to_data size: 201627
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 41.5s, gctime: 1.8s, systime: 0.46658s.
data_to_word real: 41.9s
data_to_word size: 447464
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 3m56s, gctime: 27.8s, systime: 7.2s.
inst,ssa,two-reg (par) real: 1m35s
inst,ssa,two-reg (par) size: 1767437
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 31.7s, gctime: 2.5s, systime: 0.88259s.
get_clash (par) real: 10.2s
get_clash (par) size: 2788382
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: 966 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 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: 10 coalesceable: 6 coalesced: 6
174 moves: 60 coalesceable: 41 coalesced: 40
175 moves: 60 coalesceable: 41 coalesced: 40
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: 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: 2 coalesceable: 2 coalesced: 2
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: 122 coalesceable: 90 coalesced: 90
197 moves: 118 coalesceable: 87 coalesced: 87
198 moves: 17 coalesceable: 11 coalesced: 11
199 moves: 17 coalesceable: 11 coalesced: 11
200 moves: 5 coalesceable: 3 coalesced: 3
201 moves: 8 coalesceable: 8 coalesced: 8
202 moves: 46 coalesceable: 34 coalesced: 33
203 moves: 6 coalesceable: 6 coalesced: 6
204 moves: 29 coalesceable: 19 coalesced: 13
205 moves: 4 coalesceable: 4 coalesced: 4
206 moves: 4 coalesceable: 4 coalesced: 4
207 moves: 4 coalesceable: 4 coalesced: 4
208 moves: 7 coalesceable: 7 coalesced: 7
209 moves: 6 coalesceable: 6 coalesced: 6
210 moves: 49 coalesceable: 36 coalesced: 34
211 moves: 8 coalesceable: 8 coalesced: 8
212 moves: 93 coalesceable: 61 coalesced: 58
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: 6 coalesceable: 6 coalesced: 6
224 moves: 99 coalesceable: 62 coalesced: 56
225 moves: 6 coalesceable: 6 coalesced: 6
226 moves: 86 coalesceable: 57 coalesced: 51
227 moves: 4 coalesceable: 4 coalesced: 4
228 moves: 9 coalesceable: 9 coalesced: 8
229 moves: 8 coalesceable: 8 coalesced: 8
230 moves: 124 coalesceable: 72 coalesced: 58
231 moves: 6 coalesceable: 6 coalesced: 6
232 moves: 62 coalesceable: 31 coalesced: 29
233 moves: 4 coalesceable: 4 coalesced: 4
234 moves: 48 coalesceable: 23 coalesced: 21
235 moves: 12 coalesceable: 12 coalesced: 12
236 moves: 962 coalesceable: 558 coalesced: 400
237 moves: 6 coalesceable: 6 coalesced: 6
238 moves: 15 coalesceable: 14 coalesced: 10
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: 4 coalesceable: 4 coalesced: 4
258 moves: 111 coalesceable: 77 coalesced: 66
259 moves: 4 coalesceable: 4 coalesced: 4
260 moves: 26 coalesceable: 18 coalesced: 15
261 moves: 6 coalesceable: 6 coalesced: 6
262 moves: 23 coalesceable: 15 coalesced: 11
263 moves: 8 coalesceable: 8 coalesced: 8
264 moves: 415 coalesceable: 260 coalesced: 212
265 moves: 4 coalesceable: 4 coalesced: 4
266 moves: 26 coalesceable: 18 coalesced: 15
267 moves: 6 coalesceable: 6 coalesced: 6
268 moves: 23 coalesceable: 15 coalesced: 11
269 moves: 6 coalesceable: 6 coalesced: 6
270 moves: 515 coalesceable: 325 coalesced: 276
271 moves: 4 coalesceable: 4 coalesced: 4
272 moves: 3 coalesceable: 3 coalesced: 3
273 moves: 4 coalesceable: 4 coalesced: 4
274 moves: 21 coalesceable: 14 coalesced: 10
275 moves: 4 coalesceable: 4 coalesced: 4
276 moves: 3 coalesceable: 3 coalesced: 3
277 moves: 4 coalesceable: 4 coalesced: 4
278 moves: 3 coalesceable: 3 coalesced: 3
279 moves: 4 coalesceable: 4 coalesced: 4
280 moves: 671 coalesceable: 445 coalesced: 389
281 moves: 4 coalesceable: 4 coalesced: 4
282 moves: 49 coalesceable: 33 coalesced: 33
283 moves: 4 coalesceable: 4 coalesced: 4
284 moves: 3 coalesceable: 3 coalesced: 3
285 moves: 4 coalesceable: 4 coalesced: 4
286 moves: 43 coalesceable: 29 coalesced: 25
287 moves: 4 coalesceable: 4 coalesced: 4
288 moves: 25 coalesceable: 18 coalesced: 16
289 moves: 4 coalesceable: 4 coalesced: 4
290 moves: 3 coalesceable: 3 coalesced: 3
291 moves: 6 coalesceable: 6 coalesced: 6
292 moves: 36 coalesceable: 23 coalesced: 17
293 moves: 6 coalesceable: 6 coalesced: 6
294 moves: 21 coalesceable: 19 coalesced: 19
295 moves: 4 coalesceable: 4 coalesced: 4
296 moves: 9 coalesceable: 9 coalesced: 8
297 moves: 8 coalesceable: 8 coalesced: 8
298 moves: 22 coalesceable: 20 coalesced: 20
299 moves: 12 coalesceable: 12 coalesced: 12
300 moves: 218 coalesceable: 134 coalesced: 94
301 moves: 12 coalesceable: 12 coalesced: 12
302 moves: 218 coalesceable: 134 coalesced: 94
303 moves: 8 coalesceable: 8 coalesced: 8
304 moves: 124 coalesceable: 72 coalesced: 58
305 moves: 4 coalesceable: 4 coalesced: 4
306 moves: 77 coalesceable: 56 coalesced: 53
307 moves: 6 coalesceable: 6 coalesced: 6
308 moves: 110 coalesceable: 79 coalesced: 69
309 moves: 8 coalesceable: 8 coalesced: 8
310 moves: 407 coalesceable: 208 coalesced: 175
311 moves: 4 coalesceable: 4 coalesced: 4
312 moves: 56 coalesceable: 33 coalesced: 30
313 moves: 4 coalesceable: 4 coalesced: 4
314 moves: 8 coalesceable: 6 coalesced: 6
315 moves: 8 coalesceable: 8 coalesced: 8
316 moves: 163 coalesceable: 110 coalesced: 96
317 moves: 6 coalesceable: 6 coalesced: 6
318 moves: 114 coalesceable: 80 coalesced: 72
319 moves: 4 coalesceable: 4 coalesced: 4
320 moves: 6 coalesceable: 6 coalesced: 6
321 moves: 4 coalesceable: 4 coalesced: 4
322 moves: 6 coalesceable: 6 coalesced: 6
323 moves: 8 coalesceable: 8 coalesced: 8
324 moves: 128 coalesceable: 77 coalesced: 70
325 moves: 8 coalesceable: 8 coalesced: 8
326 moves: 111 coalesceable: 66 coalesced: 51
327 moves: 6 coalesceable: 6 coalesced: 6
328 moves: 427 coalesceable: 263 coalesced: 198
329 moves: 4 coalesceable: 4 coalesced: 4
330 moves: 5 coalesceable: 5 coalesced: 5
331 moves: 4 coalesceable: 4 coalesced: 4
332 moves: 17 coalesceable: 12 coalesced: 11
333 moves: 4 coalesceable: 4 coalesced: 4
334 moves: 272 coalesceable: 139 coalesced: 131
335 moves: 4 coalesceable: 4 coalesced: 4
336 moves: 69 coalesceable: 54 coalesced: 54
337 moves: 6 coalesceable: 6 coalesced: 6
338 moves: 78 coalesceable: 59 coalesced: 56
339 moves: 4 coalesceable: 4 coalesced: 4
340 moves: 21 coalesceable: 18 coalesced: 16
341 moves: 4 coalesceable: 4 coalesced: 4
342 moves: 164 coalesceable: 106 coalesced: 89
343 moves: 224 coalesceable: 137 coalesced: 113
344 moves: 217 coalesceable: 133 coalesced: 108
345 moves: 4 coalesceable: 4 coalesced: 4
346 moves: 45 coalesceable: 26 coalesced: 24
347 moves: 4 coalesceable: 4 coalesced: 4
348 moves: 42 coalesceable: 23 coalesced: 22
349 moves: 4 coalesceable: 4 coalesced: 4
350 moves: 15 coalesceable: 12 coalesced: 12
351 moves: 36 coalesceable: 18 coalesced: 18
352 moves: 4 coalesceable: 4 coalesced: 4
353 moves: 8 coalesceable: 8 coalesced: 8
354 moves: 4 coalesceable: 4 coalesced: 4
355 moves: 5 coalesceable: 5 coalesced: 5
356 moves: 4 coalesceable: 4 coalesced: 4
357 moves: 5 coalesceable: 5 coalesced: 5
358 moves: 4 coalesceable: 4 coalesced: 4
359 moves: 5 coalesceable: 5 coalesced: 5
360 moves: 4 coalesceable: 4 coalesced: 4
361 moves: 889 coalesceable: 524 coalesced: 479
362 moves: 4 coalesceable: 4 coalesced: 4
363 moves: 288 coalesceable: 174 coalesced: 152
364 moves: 4 coalesceable: 4 coalesced: 4
365 moves: 75 coalesceable: 47 coalesced: 45
366 moves: 10 coalesceable: 10 coalesced: 10
367 moves: 3809 coalesceable: 2164 coalesced: 1154
368 moves: 6 coalesceable: 6 coalesced: 6
369 moves: 19 coalesceable: 10 coalesced: 7
370 moves: 4 coalesceable: 4 coalesced: 4
371 moves: 270 coalesceable: 173 coalesced: 169
372 moves: 6 coalesceable: 6 coalesced: 6
373 moves: 597 coalesceable: 375 coalesced: 367
374 moves: 4 coalesceable: 4 coalesced: 4
375 moves: 47 coalesceable: 39 coalesced: 39
runtime: 28.1s, gctime: 0.09145s, systime: 0.05326s.
external oracle real: 28.2s
external oracle size: 207962
apply colour (par) eval: runtime: 4m29s, gctime: 19.7s, systime: 7.5s.
apply colour (par) real: 1m54s
apply colour (par) size: 879499
check colour eval: runtime: 5.4s, gctime: 0.38605s, systime: 0.08334s.
check colour real: 5.5s
check colour size: 879876
word_to_stack eval: runtime: 3m20s, gctime: 18.8s, systime: 2.8s.
word_to_stack real: 3m22s
word_to_stack size: 700904
stack_rawcall eval: runtime: 1m35s, gctime: 1.8s, systime: 0.60656s.
stack_rawcall real: 1m35s
stack_rawcall size: 692213
stack_alloc (par) eval: runtime: 2m17s, gctime: 3.0s, systime: 2.4s.
stack_alloc (par) real: 49.0s
stack_alloc (par) size: 696188
expand stack_remove_def eval: runtime: 0.10377s, gctime: 0.00000s, systime: 0.00001s.
expand stack_remove_def real: 0.10385s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 3m45s, gctime: 25.0s, systime: 5.6s.
stack_remove (par) real: 1m41s
stack_remove (par) size: 1155714
stack_names (par) eval: runtime: 1m51s, gctime: 12.4s, systime: 3.2s.
stack_names (par) real: 46.6s
stack_names (par) size: 1194294
stack_to_lab (par) eval: runtime: 3m42s, gctime: 26.5s, systime: 6.6s.
stack_to_lab (par) real: 1m34s
stack_to_lab (par) size: 1477647
lab_to_target eval: runtime: 10m25s, gctime: 59.0s, systime: 9.7s.
lab_to_target real: 10m34s
lab_to_target size: 2404609
export: runtime: 0.86200s, gctime: 0.00000s, systime: 0.00004s.
Saved theorem _____ "patch_compiled"
Exporting theory "patchCompile" ... done.
Theory "patchCompile" took 42m16s to build
cc patch.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_patch
Linking /root/regression/cakeml-1571/examples/compilation/x64/sortCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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 "sortCompile">>
to_flat eval: runtime: 48.3s, gctime: 1.1s, systime: 1.1s.
to_flat real: 49.4s
to_flat size: 132900
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 1.0s, gctime: 0.00000s, systime: 0.00000s.
to_clos real: 1.0s
to_clos size: 57430
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 11.6s, gctime: 0.40273s, systime: 0.10983s.
to_bvl real: 11.7s
to_bvl size: 100770
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m45s, gctime: 0.77119s, systime: 0.74348s.
to_bvi real: 1m45s
to_bvi size: 101126
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 23.1s, gctime: 1.0s, systime: 0.33650s.
to_data real: 23.4s
to_data size: 152382
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 33.5s, gctime: 0.94334s, systime: 0.26655s.
data_to_word real: 33.8s
data_to_word size: 355733
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m34s, gctime: 6.0s, systime: 5.7s.
inst,ssa,two-reg (par) real: 1m08s
inst,ssa,two-reg (par) size: 1402566
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 23.7s, gctime: 2.7s, systime: 0.56871s.
get_clash (par) real: 9.5s
get_clash (par) size: 2176029
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: 958 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 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: 10 coalesceable: 6 coalesced: 6
169 moves: 60 coalesceable: 41 coalesced: 40
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: 2 coalesceable: 2 coalesced: 2
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: 5 coalesceable: 3 coalesced: 3
189 moves: 6 coalesceable: 6 coalesced: 6
190 moves: 29 coalesceable: 19 coalesced: 13
191 moves: 6 coalesceable: 6 coalesced: 6
192 moves: 32 coalesceable: 23 coalesced: 18
193 moves: 4 coalesceable: 4 coalesced: 4
194 moves: 5 coalesceable: 5 coalesced: 3
195 moves: 4 coalesceable: 4 coalesced: 4
196 moves: 7 coalesceable: 7 coalesced: 7
197 moves: 4 coalesceable: 4 coalesced: 4
198 moves: 9 coalesceable: 9 coalesced: 8
199 moves: 8 coalesceable: 8 coalesced: 8
200 moves: 124 coalesceable: 72 coalesced: 58
201 moves: 6 coalesceable: 6 coalesced: 6
202 moves: 62 coalesceable: 31 coalesced: 29
203 moves: 4 coalesceable: 4 coalesced: 4
204 moves: 48 coalesceable: 23 coalesced: 21
205 moves: 12 coalesceable: 12 coalesced: 12
206 moves: 274 coalesceable: 177 coalesced: 132
207 moves: 6 coalesceable: 6 coalesced: 6
208 moves: 115 coalesceable: 84 coalesced: 80
209 moves: 6 coalesceable: 6 coalesced: 6
210 moves: 35 coalesceable: 25 coalesced: 24
211 moves: 6 coalesceable: 6 coalesced: 6
212 moves: 23 coalesceable: 15 coalesced: 11
213 moves: 6 coalesceable: 6 coalesced: 6
214 moves: 23 coalesceable: 15 coalesced: 11
215 moves: 6 coalesceable: 6 coalesced: 6
216 moves: 30 coalesceable: 19 coalesced: 16
217 moves: 6 coalesceable: 6 coalesced: 6
218 moves: 29 coalesceable: 21 coalesced: 17
219 moves: 6 coalesceable: 6 coalesced: 6
220 moves: 24 coalesceable: 16 coalesced: 13
221 moves: 6 coalesceable: 6 coalesced: 6
222 moves: 24 coalesceable: 16 coalesced: 13
223 moves: 6 coalesceable: 6 coalesced: 6
224 moves: 30 coalesceable: 22 coalesced: 19
225 moves: 6 coalesceable: 6 coalesced: 6
226 moves: 60 coalesceable: 44 coalesced: 41
227 moves: 6 coalesceable: 6 coalesced: 6
228 moves: 62 coalesceable: 31 coalesced: 29
229 moves: 4 coalesceable: 4 coalesced: 4
230 moves: 3 coalesceable: 3 coalesced: 3
231 moves: 4 coalesceable: 4 coalesced: 4
232 moves: 43 coalesceable: 29 coalesced: 25
233 moves: 4 coalesceable: 4 coalesced: 4
234 moves: 25 coalesceable: 18 coalesced: 16
235 moves: 4 coalesceable: 4 coalesced: 4
236 moves: 3 coalesceable: 3 coalesced: 3
237 moves: 6 coalesceable: 6 coalesced: 6
238 moves: 36 coalesceable: 23 coalesced: 17
239 moves: 6 coalesceable: 6 coalesced: 6
240 moves: 21 coalesceable: 19 coalesced: 19
241 moves: 4 coalesceable: 4 coalesced: 4
242 moves: 9 coalesceable: 9 coalesced: 8
243 moves: 8 coalesceable: 8 coalesced: 8
244 moves: 22 coalesceable: 20 coalesced: 20
245 moves: 12 coalesceable: 12 coalesced: 12
246 moves: 218 coalesceable: 134 coalesced: 94
247 moves: 12 coalesceable: 12 coalesced: 12
248 moves: 218 coalesceable: 134 coalesced: 94
249 moves: 8 coalesceable: 8 coalesced: 8
250 moves: 124 coalesceable: 72 coalesced: 58
251 moves: 6 coalesceable: 6 coalesced: 6
252 moves: 64 coalesceable: 42 coalesced: 35
253 moves: 4 coalesceable: 4 coalesced: 4
254 moves: 23 coalesceable: 13 coalesced: 12
255 moves: 6 coalesceable: 6 coalesced: 6
256 moves: 17 coalesceable: 15 coalesced: 15
257 moves: 4 coalesceable: 4 coalesced: 4
258 moves: 8 coalesceable: 8 coalesced: 8
259 moves: 8 coalesceable: 8 coalesced: 8
260 moves: 18 coalesceable: 16 coalesced: 16
261 moves: 8 coalesceable: 8 coalesced: 8
262 moves: 54 coalesceable: 36 coalesced: 33
263 moves: 4 coalesceable: 4 coalesced: 4
264 moves: 135 coalesceable: 82 coalesced: 73
265 moves: 10 coalesceable: 10 coalesced: 10
266 moves: 143 coalesceable: 91 coalesced: 80
267 moves: 6 coalesceable: 6 coalesced: 6
268 moves: 13 coalesceable: 12 coalesced: 8
269 moves: 4 coalesceable: 4 coalesced: 4
270 moves: 77 coalesceable: 56 coalesced: 53
271 moves: 6 coalesceable: 6 coalesced: 6
272 moves: 110 coalesceable: 79 coalesced: 69
273 moves: 8 coalesceable: 8 coalesced: 8
274 moves: 407 coalesceable: 208 coalesced: 175
275 moves: 4 coalesceable: 4 coalesced: 4
276 moves: 56 coalesceable: 33 coalesced: 30
277 moves: 4 coalesceable: 4 coalesced: 4
278 moves: 8 coalesceable: 6 coalesced: 6
279 moves: 8 coalesceable: 8 coalesced: 8
280 moves: 163 coalesceable: 110 coalesced: 96
281 moves: 6 coalesceable: 6 coalesced: 6
282 moves: 114 coalesceable: 80 coalesced: 72
283 moves: 4 coalesceable: 4 coalesced: 4
284 moves: 6 coalesceable: 6 coalesced: 6
285 moves: 4 coalesceable: 4 coalesced: 4
286 moves: 6 coalesceable: 6 coalesced: 6
287 moves: 8 coalesceable: 8 coalesced: 8
288 moves: 128 coalesceable: 77 coalesced: 70
289 moves: 8 coalesceable: 8 coalesced: 8
290 moves: 111 coalesceable: 66 coalesced: 51
291 moves: 6 coalesceable: 6 coalesced: 6
292 moves: 427 coalesceable: 263 coalesced: 198
293 moves: 4 coalesceable: 4 coalesced: 4
294 moves: 5 coalesceable: 5 coalesced: 5
295 moves: 4 coalesceable: 4 coalesced: 4
296 moves: 272 coalesceable: 139 coalesced: 131
297 moves: 4 coalesceable: 4 coalesced: 4
298 moves: 69 coalesceable: 54 coalesced: 54
299 moves: 6 coalesceable: 6 coalesced: 6
300 moves: 78 coalesceable: 59 coalesced: 56
301 moves: 4 coalesceable: 4 coalesced: 4
302 moves: 21 coalesceable: 18 coalesced: 16
303 moves: 4 coalesceable: 4 coalesced: 4
304 moves: 164 coalesceable: 106 coalesced: 89
305 moves: 224 coalesceable: 137 coalesced: 113
306 moves: 217 coalesceable: 133 coalesced: 108
307 moves: 4 coalesceable: 4 coalesced: 4
308 moves: 45 coalesceable: 26 coalesced: 24
309 moves: 102 coalesceable: 65 coalesced: 55
310 moves: 102 coalesceable: 67 coalesced: 53
311 moves: 130 coalesceable: 77 coalesced: 70
312 moves: 12 coalesceable: 12 coalesced: 12
313 moves: 124 coalesceable: 71 coalesced: 52
314 moves: 133 coalesceable: 84 coalesced: 64
315 moves: 6 coalesceable: 6 coalesced: 6
316 moves: 60 coalesceable: 40 coalesced: 36
317 moves: 6 coalesceable: 6 coalesced: 6
318 moves: 45 coalesceable: 26 coalesced: 24
319 moves: 6 coalesceable: 6 coalesced: 6
320 moves: 37 coalesceable: 16 coalesced: 14
321 moves: 4 coalesceable: 4 coalesced: 4
322 moves: 174 coalesceable: 149 coalesced: 149
323 moves: 45 coalesceable: 30 coalesced: 28
runtime: 18.7s, gctime: 0.24185s, systime: 0.03990s.
external oracle real: 18.8s
external oracle size: 163158
apply colour (par) eval: runtime: 3m25s, gctime: 19.6s, systime: 5.5s.
apply colour (par) real: 1m56s
apply colour (par) size: 716044
check colour eval: runtime: 3.3s, gctime: 0.36474s, systime: 0.08665s.
check colour real: 3.4s
check colour size: 716369
word_to_stack eval: runtime: 2m41s, gctime: 17.8s, systime: 2.9s.
word_to_stack real: 2m44s
word_to_stack size: 575942
stack_rawcall eval: runtime: 1m17s, gctime: 1.4s, systime: 0.51634s.
stack_rawcall real: 1m18s
stack_rawcall size: 568048
stack_alloc (par) eval: runtime: 1m47s, gctime: 2.2s, systime: 1.5s.
stack_alloc (par) real: 47.2s
stack_alloc (par) size: 570631
expand stack_remove_def eval: runtime: 0.13428s, gctime: 0.05176s, systime: 0.03336s.
expand stack_remove_def real: 0.16777s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m48s, gctime: 15.5s, systime: 2.9s.
stack_remove (par) real: 1m32s
stack_remove (par) size: 961056
stack_names (par) eval: runtime: 1m18s, gctime: 3.6s, systime: 1.2s.
stack_names (par) real: 36.1s
stack_names (par) size: 992448
stack_to_lab (par) eval: runtime: 2m47s, gctime: 14.1s, systime: 4.3s.
stack_to_lab (par) real: 1m19s
stack_to_lab (par) size: 1215298
lab_to_target eval: runtime: 8m34s, gctime: 46.6s, systime: 7.5s.
lab_to_target real: 8m42s
lab_to_target size: 1971307
export: runtime: 0.77523s, gctime: 0.00000s, systime: 0.00004s.
Saved theorem _____ "sort_compiled"
Exporting theory "sortCompile" ... done.
Theory "sortCompile" took 33m00s to build
cc sort.S /root/regression/cakeml-1571/basis/basis_ffi.o -o cake_sort
Linking /root/regression/cakeml-1571/examples/compilation/x64/wordcountCompileScript.uo to produce theory-builder executable
/root/regression/HOL-a8ccec8c32fc37fc23c8a5b4e6756b2f9cee7042/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 (...) |
(...) => ... ... |
... => ... |
...
/root/regression/cakeml-1571/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 "wordcountCompile">>
to_flat eval: runtime: 48.1s, gctime: 0.86720s, systime: 1.2s.
to_flat real: 49.3s
to_flat size: 129216
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 1.2s, gctime: 0.16243s, systime: 0.01665s.
to_clos real: 1.2s
to_clos size: 55821
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 11.5s, gctime: 0.33140s, systime: 0.06345s.
to_bvl real: 11.5s
to_bvl size: 101116
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 1m47s, gctime: 0.75338s, systime: 0.92062s.
to_bvi real: 1m47s
to_bvi size: 101096
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 23.0s, gctime: 1.0s, systime: 0.27673s.
to_data real: 23.3s
to_data size: 154923
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 34.5s, gctime: 1.1s, systime: 0.43995s.
data_to_word real: 35.0s
data_to_word size: 362122
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 2m39s, gctime: 5.7s, systime: 5.8s.
inst,ssa,two-reg (par) real: 1m07s
inst,ssa,two-reg (par) size: 1433866
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 23.8s, gctime: 2.5s, systime: 0.62353s.
get_clash (par) real: 9.2s
get_clash (par) size: 2232130
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: 954 coalesceable: 2 coalesced: 2
118 moves: 17 coalesceable: 12 coalesced: 12
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: 4375 coalesceable: 2573 coalesced: 2573
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: 17 coalesceable: 11 coalesced: 11
170 moves: 10 coalesceable: 6 coalesced: 6
171 moves: 60 coalesceable: 41 coalesced: 40
172 moves: 60 coalesceable: 41 coalesced: 40
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: 17 coalesceable: 11 coalesced: 11
186 moves: 2 coalesceable: 2 coalesced: 2
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: 5 coalesceable: 3 coalesced: 3
192 moves: 8 coalesceable: 8 coalesced: 8
193 moves: 46 coalesceable: 34 coalesced: 33
194 moves: 6 coalesceable: 6 coalesced: 6
195 moves: 29 coalesceable: 19 coalesced: 13
196 moves: 6 coalesceable: 6 coalesced: 6
197 moves: 32 coalesceable: 23 coalesced: 18
198 moves: 4 coalesceable: 4 coalesced: 4
199 moves: 5 coalesceable: 5 coalesced: 3
200 moves: 6 coalesceable: 6 coalesced: 6
201 moves: 36 coalesceable: 25 coalesced: 24
202 moves: 4 coalesceable: 4 coalesced: 4
203 moves: 5 coalesceable: 5 coalesced: 3
204 moves: 4 coalesceable: 4 coalesced: 4
205 moves: 7 coalesceable: 7 coalesced: 7
206 moves: 6 coalesceable: 6 coalesced: 6
207 moves: 76 coalesceable: 47 coalesced: 43
208 moves: 4 coalesceable: 4 coalesced: 4
209 moves: 35 coalesceable: 22 coalesced: 21
210 moves: 4 coalesceable: 4 coalesced: 4
211 moves: 9 coalesceable: 9 coalesced: 8
212 moves: 8 coalesceable: 8 coalesced: 8
213 moves: 124 coalesceable: 72 coalesced: 58
214 moves: 6 coalesceable: 6 coalesced: 6
215 moves: 62 coalesceable: 31 coalesced: 29
216 moves: 4 coalesceable: 4 coalesced: 4
217 moves: 48 coalesceable: 23 coalesced: 21
218 moves: 12 coalesceable: 12 coalesced: 12
219 moves: 962 coalesceable: 558 coalesced: 400
220 moves: 6 coalesceable: 6 coalesced: 6
221 moves: 15 coalesceable: 14 coalesced: 10
222 moves: 6 coalesceable: 6 coalesced: 6
223 moves: 23 coalesceable: 15 coalesced: 11
224 moves: 6 coalesceable: 6 coalesced: 6
225 moves: 23 coalesceable: 15 coalesced: 11
226 moves: 6 coalesceable: 6 coalesced: 6
227 moves: 30 coalesceable: 19 coalesced: 16
228 moves: 6 coalesceable: 6 coalesced: 6
229 moves: 29 coalesceable: 21 coalesced: 17
230 moves: 6 coalesceable: 6 coalesced: 6
231 moves: 24 coalesceable: 16 coalesced: 13
232 moves: 6 coalesceable: 6 coalesced: 6
233 moves: 24 coalesceable: 16 coalesced: 13
234 moves: 6 coalesceable: 6 coalesced: 6
235 moves: 30 coalesceable: 22 coalesced: 19
236 moves: 6 coalesceable: 6 coalesced: 6
237 moves: 60 coalesceable: 44 coalesced: 41
238 moves: 6 coalesceable: 6 coalesced: 6
239 moves: 62 coalesceable: 31 coalesced: 29
240 moves: 6 coalesceable: 6 coalesced: 6
241 moves: 79 coalesceable: 52 coalesced: 46
242 moves: 4 coalesceable: 4 coalesced: 4
243 moves: 162 coalesceable: 108 coalesced: 98
244 moves: 8 coalesceable: 8 coalesced: 8
245 moves: 284 coalesceable: 173 coalesced: 140
246 moves: 8 coalesceable: 8 coalesced: 8
247 moves: 119 coalesceable: 79 coalesced: 60
248 moves: 4 coalesceable: 4 coalesced: 4
249 moves: 423 coalesceable: 264 coalesced: 209
250 moves: 4 coalesceable: 4 coalesced: 4
251 moves: 3 coalesceable: 3 coalesced: 3
252 moves: 4 coalesceable: 4 coalesced: 4
253 moves: 43 coalesceable: 29 coalesced: 25
254 moves: 4 coalesceable: 4 coalesced: 4
255 moves: 42 coalesceable: 29 coalesced: 24
256 moves: 4 coalesceable: 4 coalesced: 4
257 moves: 25 coalesceable: 18 coalesced: 16
258 moves: 4 coalesceable: 4 coalesced: 4
259 moves: 3 coalesceable: 3 coalesced: 3
260 moves: 6 coalesceable: 6 coalesced: 6
261 moves: 36 coalesceable: 23 coalesced: 17
262 moves: 6 coalesceable: 6 coalesced: 6
263 moves: 21 coalesceable: 19 coalesced: 19
264 moves: 4 coalesceable: 4 coalesced: 4
265 moves: 9 coalesceable: 9 coalesced: 8
266 moves: 8 coalesceable: 8 coalesced: 8
267 moves: 22 coalesceable: 20 coalesced: 20
268 moves: 12 coalesceable: 12 coalesced: 12
269 moves: 218 coalesceable: 134 coalesced: 94
270 moves: 12 coalesceable: 12 coalesced: 12
271 moves: 218 coalesceable: 134 coalesced: 94
272 moves: 8 coalesceable: 8 coalesced: 8
273 moves: 124 coalesceable: 72 coalesced: 58
274 moves: 4 coalesceable: 4 coalesced: 4
275 moves: 77 coalesceable: 56 coalesced: 53
276 moves: 6 coalesceable: 6 coalesced: 6
277 moves: 110 coalesceable: 79 coalesced: 69
278 moves: 8 coalesceable: 8 coalesced: 8
279 moves: 407 coalesceable: 208 coalesced: 175
280 moves: 4 coalesceable: 4 coalesced: 4
281 moves: 56 coalesceable: 33 coalesced: 30
282 moves: 4 coalesceable: 4 coalesced: 4
283 moves: 8 coalesceable: 6 coalesced: 6
284 moves: 8 coalesceable: 8 coalesced: 8
285 moves: 163 coalesceable: 110 coalesced: 96
286 moves: 6 coalesceable: 6 coalesced: 6
287 moves: 114 coalesceable: 80 coalesced: 72
288 moves: 4 coalesceable: 4 coalesced: 4
289 moves: 6 coalesceable: 6 coalesced: 6
290 moves: 4 coalesceable: 4 coalesced: 4
291 moves: 6 coalesceable: 6 coalesced: 6
292 moves: 8 coalesceable: 8 coalesced: 8
293 moves: 128 coalesceable: 77 coalesced: 70
294 moves: 8 coalesceable: 8 coalesced: 8
295 moves: 111 coalesceable: 66 coalesced: 51
296 moves: 6 coalesceable: 6 coalesced: 6
297 moves: 50 coalesceable: 38 coalesced: 35
298 moves: 6 coalesceable: 6 coalesced: 6
299 moves: 427 coalesceable: 263 coalesced: 198
300 moves: 4 coalesceable: 4 coalesced: 4
301 moves: 5 coalesceable: 5 coalesced: 5
302 moves: 4 coalesceable: 4 coalesced: 4
303 moves: 272 coalesceable: 139 coalesced: 131
304 moves: 4 coalesceable: 4 coalesced: 4
305 moves: 69 coalesceable: 54 coalesced: 54
306 moves: 6 coalesceable: 6 coalesced: 6
307 moves: 78 coalesceable: 59 coalesced: 56
308 moves: 4 coalesceable: 4 coalesced: 4
309 moves: 21 coalesceable: 18 coalesced: 16
310 moves: 4 coalesceable: 4 coalesced: 4
311 moves: 164 coalesceable: 106 coalesced: 89
312 moves: 224 coalesceable: 137 coalesced: 113
313 moves: 217 coalesceable: 133 coalesced: 108
314 moves: 4 coalesceable: 4 coalesced: 4
315 moves: 45 coalesceable: 26 coalesced: 24
316 moves: 4 coalesceable: 4 coalesced: 4
317 moves: 42 coalesceable: 23 coalesced: 22
318 moves: 4 coalesceable: 4 coalesced: 4
319 moves: 15 coalesceable: 12 coalesced: 12
320 moves: 36 coalesceable: 18 coalesced: 18
321 moves: 4 coalesceable: 4 coalesced: 4
322 moves: 14 coalesceable: 13 coalesced: 11
323 moves: 4 coalesceable: 4 coalesced: 4
324 moves: 40 coalesceable: 28 coalesced: 23
325 moves: 4 coalesceable: 4 coalesced: 4
326 moves: 30 coalesceable: 21 coalesced: 20
327 moves: 4 coalesceable: 4 coalesced: 4
328 moves: 135 coalesceable: 83 coalesced: 79
runtime: 19.3s, gctime: 0.29169s, systime: 0.04312s.
external oracle real: 19.3s
external oracle size: 167296
apply colour (par) eval: runtime: 3m43s, gctime: 23.1s, systime: 13.6s.
apply colour (par) real: 2m05s
apply colour (par) size: 729967
check colour eval: runtime: 3.2s, gctime: 0.30789s, systime: 0.10006s.
check colour real: 3.3s
check colour size: 730297
word_to_stack eval: runtime: 2m28s, gctime: 2.8s, systime: 1.9s.
word_to_stack real: 2m30s
word_to_stack size: 586441
stack_rawcall eval: runtime: 1m20s, gctime: 1.2s, systime: 0.89565s.
stack_rawcall real: 1m21s
stack_rawcall size: 578453
stack_alloc (par) eval: runtime: 1m52s, gctime: 1.4s, systime: 5.9s.
stack_alloc (par) real: 48.8s
stack_alloc (par) size: 581307
expand stack_remove_def eval: runtime: 0.07570s, gctime: 0.00000s, systime: 0.00000s.
expand stack_remove_def real: 0.07576s
expand stack_remove_def size: 3014
stack_remove (par) eval: runtime: 2m33s, gctime: 2.0s, systime: 9.0s.
stack_remove (par) real: 1m18s
stack_remove (par) size: 981162
stack_names (par) eval: runtime: 1m18s, gctime: 1.6s, systime: 4.5s.
stack_names (par) real: 36.7s
stack_names (par) size: 1012779
stack_to_lab (par) eval: runtime: 2m37s, gctime: 3.2s, systime: 3.2s.
stack_to_lab (par) real: 1m06s
stack_to_lab (par) size: 1243662
lab_to_target eval: runtime: 8m28s, gctime: 15.5s, systime: 5.8s.
lab_to_target real: 8m34s
lab_to_target size: 2015378
export: runtime: 1.0s, gctime: 0.20409s, systime: 0.01998s.
Saved theorem _____ "wordcount_compiled"
Exporting theory "wordcountCompile" ... Run out of store - interrupting threads
Failure while writing theory!
error in quse /root/regression/cakeml-1571/examples/compilation/x64/wordcountCompileScript.sml : Interrupt
error in load /root/regression/cakeml-1571/examples/compilation/x64/wordcountCompileScript : Interrupt
Uncaught exception: Interrupt
Failed script build for /root/regression/cakeml-1571/examples/compilation/x64/wordcountCompileScript - exited with code 1