CakeML:13eb6f5aa6a5bb9c159b02dfa1cc8c1d7bfc4d3a Fix a mistake #842 (ramsey)Merging into:6b1184f731754a44e6368258d6c1b1cc729aa0f5 Merge pull request #843 from CakeML/newline-fixHOL:7e1cdab63fa78a67a3fabc28a9f2a909e65b6921 Make RPROD (and PAIR_REL and ###) more polymorphicMachine:oven3 4.19.67.1.amd64-smp Claimed job Building HOL Starting developers Finished developers 8s 98MB Starting developers/bin Finished developers/bin 12s 1GB Starting semantics/ffi Finished semantics/ffi 25s 257MB Starting semantics Finished semantics 3m13s 1GB Starting semantics/proofs Finished semantics/proofs 8m08s 1GB Starting semantics/alt_semantics Finished semantics/alt_semantics 22s 444MB Starting semantics/alt_semantics/proofs Finished semantics/alt_semantics/proofs 5m24s 994MB Starting basis/pure Finished basis/pure 6m05s 886MB Starting translator Finished translator 7m08s 1GB Starting compiler/parsing Finished compiler/parsing 2m38s 3GB Starting characteristic Finished characteristic 12m08s 2GB Starting translator/monadic Finished translator/monadic 3m30s 1GB Starting basis Finished basis 1h41m37s 16GB Starting compiler/inference Finished compiler/inference 2m44s 1GB Starting compiler/backend/reg_alloc Finished compiler/backend/reg_alloc 2m08s 1GB Starting compiler/backend/gc Finished compiler/backend/gc 6m59s 2GB Starting compiler/backend Finished compiler/backend 9m54s 5GB Starting compiler/encoders/asm Finished compiler/encoders/asm 49s 811MB Starting compiler/encoders/x64 Finished compiler/encoders/x64 2m16s 994MB Starting compiler/encoders/arm7 Finished compiler/encoders/arm7 4m39s 1GB Starting compiler/encoders/arm8 Finished compiler/encoders/arm8 1m22s 746MB Starting compiler/encoders/mips Finished compiler/encoders/mips 3m10s 1GB Starting compiler/encoders/riscv Finished compiler/encoders/riscv 4m02s 1GB Starting compiler/encoders/ag32 Finished compiler/encoders/ag32 40s 716MB Starting compiler/backend/x64 Finished compiler/backend/x64 41s 1GB Starting compiler/backend/arm7 Finished compiler/backend/arm7 46s 1GB Starting compiler/backend/arm8 Finished compiler/backend/arm8 42s 1GB Starting compiler/backend/mips Finished compiler/backend/mips 40s 1GB Starting compiler/backend/riscv Finished compiler/backend/riscv 42s 1GB Starting compiler/backend/ag32 Finished compiler/backend/ag32 2m30s 2GB Starting compiler/parsing/proofs Finished compiler/parsing/proofs 14m38s 1GB Starting compiler/inference/proofs Finished compiler/inference/proofs 5m30s 1GB Starting compiler/backend/semantics Finished compiler/backend/semantics 1h02m36s 2GB Starting compiler/backend/reg_alloc/proofs Finished compiler/backend/reg_alloc/proofs 7m32s 1GB Starting compiler/backend/proofs Finished compiler/backend/proofs 1h42m22s 17GB Starting compiler/backend/serialiser Finished compiler/backend/serialiser 2m24s 1GB Starting compiler/encoders/x64/proofs Finished compiler/encoders/x64/proofs 21m28s 5GB Starting compiler/encoders/arm7/proofs Finished compiler/encoders/arm7/proofs 30m11s 4GB Starting compiler/encoders/arm8/proofs Finished compiler/encoders/arm8/proofs 15m56s 1GB Starting compiler/encoders/mips/proofs Finished compiler/encoders/mips/proofs 23m00s 2GB Starting compiler/encoders/riscv/proofs Finished compiler/encoders/riscv/proofs 19m57s 1GB Starting compiler/encoders/ag32/proofs Finished compiler/encoders/ag32/proofs 5m46s 817MB Starting compiler/backend/x64/proofs Finished compiler/backend/x64/proofs 49s 1GB Starting compiler/backend/arm7/proofs Finished compiler/backend/arm7/proofs 51s 1GB Starting compiler/backend/arm8/proofs Finished compiler/backend/arm8/proofs 48s 1GB Starting compiler/backend/mips/proofs Finished compiler/backend/mips/proofs 48s 1GB Starting compiler/backend/riscv/proofs Finished compiler/backend/riscv/proofs 50s 1GB Starting compiler/backend/ag32/proofs Finished compiler/backend/ag32/proofs 28m09s 3GB Starting compiler/proofs Finished compiler/proofs 4m29s 3GB Starting candle/set-theory Finished candle/set-theory 59s 699MB Starting candle/syntax-lib Finished candle/syntax-lib 24s 454MB Starting candle/standard/syntax Finished candle/standard/syntax 3m59s 1GB Starting candle/standard/semantics Finished candle/standard/semantics 3m50s 1GB Starting candle/standard/monadic Finished candle/standard/monadic 3m44s 1GB Starting candle/standard/ml_kernel Finished candle/standard/ml_kernel 12m14s 4GB Starting candle/overloading/syntax Finished candle/overloading/syntax 6m36s 1GB Starting candle/overloading/semantics Finished candle/overloading/semantics 27m04s 5GB Starting pancake Finished pancake 3m52s 2GB Starting pancake/ffi Finished pancake/ffi 0s 9MB Starting pancake/semantics Finished pancake/semantics 4m50s 1GB Starting pancake/proofs Finished pancake/proofs 27m16s 6GB Starting characteristic/examples Finished characteristic/examples 3m31s 3GB Starting tutorial/solutions Finished tutorial/solutions 35m13s 14GB Starting translator/monadic/examples Finished translator/monadic/examples 5m53s 2GB Starting examples Finished examples 17m26s 3GB 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-1635/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-1635/examples/compilation/x64/catCompileScript.uo to produce theory-builder executable /root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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-1635/compiler/compilationLib.sml:711: 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: 48.8s, gctime: 1.5s, systime: 0.28335s. to_flat real: 49.0s to_flat size: 108009 Saved definition __ "flat_conf_def" Saved definition __ "flat_prog_def" to_clos eval: runtime: 0.64856s, gctime: 0.00000s, systime: 0.00000s. to_clos real: 0.64852s to_clos size: 44737 Saved definition __ "clos_prog_def" to_bvl eval: runtime: 9.7s, gctime: 0.33470s, systime: 0.07652s. to_bvl real: 9.8s to_bvl size: 79180 Saved definition __ "bvl_conf_def" Saved definition __ "bvl_prog_def" Saved definition __ "bvl_names_def" to_bvi eval: runtime: 1m35s, gctime: 1.3s, systime: 0.43307s. to_bvi real: 1m35s to_bvi size: 83752 Saved definition __ "bvi_conf_def" Saved definition __ "bvi_prog_def" Saved definition __ "bvi_names_def" to_data eval: runtime: 22.1s, gctime: 1.4s, systime: 0.22668s. to_data real: 22.4s to_data size: 132457 Saved theorem _____ "to_data_thm" data_to_word eval: runtime: 32.6s, gctime: 1.8s, systime: 0.21324s. data_to_word real: 32.8s data_to_word size: 432495 Saved definition __ "word_to_word_fn_def" inst,ssa,two-reg (par) eval: runtime: 2m35s, gctime: 20.7s, systime: 8.2s. inst,ssa,two-reg (par) real: 1m28s inst,ssa,two-reg (par) size: 1289047 Saved definition __ "clash_fn_def" get_clash (par) eval: runtime: 1m42s, gctime: 21.2s, systime: 9.6s. get_clash (par) real: 42.8s get_clash (par) size: 1999840 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: 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: 18.1s, gctime: 0.05014s, systime: 1.3s. external oracle real: 19.3s external oracle size: 147263 apply colour (par) eval: runtime: 2m46s, gctime: 4.6s, systime: 16.6s. apply colour (par) real: 1m45s apply colour (par) size: 648992 check colour eval: runtime: 2.6s, gctime: 0.00000s, systime: 0.02674s. check colour real: 2.7s check colour size: 649263 word_to_stack eval: runtime: 2m10s, gctime: 2.2s, systime: 2.7s. word_to_stack real: 2m12s word_to_stack size: 528688 stack_rawcall eval: runtime: 1m09s, gctime: 1.1s, systime: 1.0s. stack_rawcall real: 1m10s stack_rawcall size: 521518 stack_alloc (par) eval: runtime: 1m37s, gctime: 1.2s, systime: 7.6s. stack_alloc (par) real: 50.4s stack_alloc (par) size: 523487 expand stack_remove_def eval: runtime: 0.07680s, gctime: 0.00000s, systime: 0.04000s. expand stack_remove_def real: 0.11686s expand stack_remove_def size: 3014 stack_remove (par) eval: runtime: 2m14s, gctime: 1.8s, systime: 6.9s. stack_remove (par) real: 1m17s stack_remove (par) size: 892450 stack_names (par) eval: runtime: 1m09s, gctime: 1.6s, systime: 6.6s. stack_names (par) real: 36.3s stack_names (par) size: 921087 stack_to_lab (par) eval: runtime: 2m19s, gctime: 2.9s, systime: 6.3s. stack_to_lab (par) real: 1m08s stack_to_lab (par) size: 1122989 lab_to_target eval: runtime: 7m40s, gctime: 13.9s, systime: 6.6s. lab_to_target real: 7m47s lab_to_target size: 1892751 export: runtime: 0.88911s, gctime: 0.09087s, systime: 0.11666s. Saved theorem _____ "cat_compiled" Exporting theory "catCompile" ... done. Theory "catCompile" took 31m17s to build Linking /root/regression/cakeml-1635/examples/compilation/x64/diffCompileScript.uo to produce theory-builder executable /root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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-1635/compiler/compilationLib.sml:711: 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: 1m09s, gctime: 16.7s, systime: 1.8s. to_flat real: 1m11s to_flat size: 156286 Saved definition __ "flat_conf_def" Saved definition __ "flat_prog_def" to_clos eval: runtime: 1.6s, gctime: 0.14928s, systime: 0.02001s. to_clos real: 1.7s to_clos size: 67482 Saved definition __ "clos_prog_def" to_bvl eval: runtime: 13.5s, gctime: 0.46351s, systime: 0.16648s. to_bvl real: 13.7s to_bvl size: 124969 Saved definition __ "bvl_conf_def" Saved definition __ "bvl_prog_def" Saved definition __ "bvl_names_def" to_bvi eval: runtime: 2m00s, gctime: 0.58642s, systime: 0.80970s. to_bvi real: 2m00s to_bvi size: 122734 Saved definition __ "bvi_conf_def" Saved definition __ "bvi_prog_def" Saved definition __ "bvi_names_def" to_data eval: runtime: 26.4s, gctime: 1.0s, systime: 0.30004s. to_data real: 26.7s to_data size: 194423 Saved theorem _____ "to_data_thm" data_to_word eval: runtime: 40.4s, gctime: 1.5s, systime: 0.45983s. data_to_word real: 40.9s data_to_word size: 576662 Saved definition __ "word_to_word_fn_def" inst,ssa,two-reg (par) eval: runtime: 3m14s, gctime: 9.1s, systime: 5.2s. inst,ssa,two-reg (par) real: 1m11s inst,ssa,two-reg (par) size: 1678536 Saved definition __ "clash_fn_def" get_clash (par) eval: runtime: 3m46s, gctime: 57.6s, systime: 21.5s. get_clash (par) real: 1m31s get_clash (par) size: 2635906 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: 998 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.0s, gctime: 0.03128s, systime: 0.57311s. external oracle real: 21.7s external oracle size: 199313 apply colour (par) eval: runtime: 3m55s, gctime: 5.7s, systime: 20.8s. apply colour (par) real: 1m51s apply colour (par) size: 851292 check colour eval: runtime: 6.1s, gctime: 0.59597s, systime: 0.17661s. check colour real: 6.3s check colour size: 851670 word_to_stack eval: runtime: 3m06s, gctime: 2.8s, systime: 10.9s. word_to_stack real: 3m16s word_to_stack size: 675490 stack_rawcall eval: runtime: 1m30s, gctime: 1.0s, systime: 2.6s. stack_rawcall real: 1m32s stack_rawcall size: 666691 stack_alloc (par) eval: runtime: 2m09s, gctime: 1.4s, systime: 10.0s. stack_alloc (par) real: 50.0s stack_alloc (par) size: 670678 expand stack_remove_def eval: runtime: 0.10235s, gctime: 0.00000s, systime: 0.00661s. expand stack_remove_def real: 0.10901s expand stack_remove_def size: 3014 stack_remove (par) eval: runtime: 2m56s, gctime: 1.7s, systime: 7.7s. stack_remove (par) real: 1m16s stack_remove (par) size: 1122514 stack_names (par) eval: runtime: 1m31s, gctime: 1.3s, systime: 6.5s. stack_names (par) real: 36.8s stack_names (par) size: 1159331 stack_to_lab (par) eval: runtime: 3m06s, gctime: 2.8s, systime: 11.8s. stack_to_lab (par) real: 1m09s stack_to_lab (par) size: 1428576 lab_to_target eval: runtime: 9m46s, gctime: 13.3s, systime: 15.8s. lab_to_target real: 10m02s lab_to_target size: 2428612 export: runtime: 0.98177s, gctime: 0.00000s, systime: 0.00007s. Saved theorem _____ "diff_compiled" Exporting theory "diffCompile" ... done. Theory "diffCompile" took 42m36s to build Linking /root/regression/cakeml-1635/examples/compilation/x64/echoCompileScript.uo to produce theory-builder executable /root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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-1635/compiler/compilationLib.sml:711: 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: 49.7s, gctime: 0.85813s, systime: 0.93652s. to_flat real: 50.7s to_flat size: 102649 Saved definition __ "flat_conf_def" Saved definition __ "flat_prog_def" to_clos eval: runtime: 0.56245s, gctime: 0.00000s, systime: 0.00010s. to_clos real: 0.56246s to_clos size: 41877 Saved definition __ "clos_prog_def" to_bvl eval: runtime: 9.2s, gctime: 0.26652s, systime: 0.07329s. to_bvl real: 9.2s to_bvl size: 69850 Saved definition __ "bvl_conf_def" Saved definition __ "bvl_prog_def" Saved definition __ "bvl_names_def" to_bvi eval: runtime: 1m31s, gctime: 0.52873s, systime: 0.73685s. to_bvi real: 1m32s to_bvi size: 75750 Saved definition __ "bvi_conf_def" Saved definition __ "bvi_prog_def" Saved definition __ "bvi_names_def" to_data eval: runtime: 21.5s, gctime: 0.87242s, systime: 0.25331s. to_data real: 21.8s to_data size: 124389 Saved theorem _____ "to_data_thm" data_to_word eval: runtime: 31.0s, gctime: 1.2s, systime: 0.41662s. data_to_word real: 31.4s data_to_word size: 413772 Saved definition __ "word_to_word_fn_def" inst,ssa,two-reg (par) eval: runtime: 2m11s, gctime: 5.4s, systime: 5.7s. inst,ssa,two-reg (par) real: 1m08s inst,ssa,two-reg (par) size: 1255320 Saved definition __ "clash_fn_def" get_clash (par) eval: runtime: 1m32s, gctime: 24.5s, systime: 9.7s. get_clash (par) real: 46.1s get_clash (par) size: 1952396 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: 960 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: 18.4s, gctime: 0.10071s, systime: 0.44331s. external oracle real: 18.8s external oracle size: 142302 apply colour (par) eval: runtime: 2m43s, gctime: 4.5s, systime: 14.8s. apply colour (par) real: 1m46s apply colour (par) size: 627225 check colour eval: runtime: 2.2s, gctime: 0.25093s, systime: 0.12007s. check colour real: 2.3s check colour size: 627458 word_to_stack eval: runtime: 2m09s, gctime: 2.4s, systime: 2.0s. word_to_stack real: 2m11s word_to_stack size: 512579 stack_rawcall eval: runtime: 1m07s, gctime: 0.81045s, systime: 0.72975s. stack_rawcall real: 1m07s stack_rawcall size: 505923 stack_alloc (par) eval: runtime: 1m32s, gctime: 1.2s, systime: 4.4s. stack_alloc (par) real: 47.3s stack_alloc (par) size: 507592 expand stack_remove_def eval: runtime: 0.08129s, gctime: 0.00000s, systime: 0.00000s. expand stack_remove_def real: 0.08134s expand stack_remove_def size: 3014 stack_remove (par) eval: runtime: 2m11s, gctime: 1.9s, systime: 6.2s. stack_remove (par) real: 1m16s stack_remove (par) size: 866734 stack_names (par) eval: runtime: 1m05s, gctime: 1.5s, systime: 3.4s. stack_names (par) real: 34.1s stack_names (par) size: 894483 stack_to_lab (par) eval: runtime: 2m11s, gctime: 2.9s, systime: 3.9s. stack_to_lab (par) real: 1m05s stack_to_lab (par) size: 1088542 lab_to_target eval: runtime: 7m37s, gctime: 13.5s, systime: 5.5s. lab_to_target real: 7m42s lab_to_target size: 1829551 export: runtime: 0.96564s, gctime: 0.22219s, systime: 0.03671s. Saved theorem _____ "echo_compiled" Exporting theory "echoCompile" ... done. Theory "echoCompile" took 29m38s to build cc cat.S /root/regression/cakeml-1635/basis/basis_ffi.o -o cake_cat cc diff.S /root/regression/cakeml-1635/basis/basis_ffi.o -o cake_diff cc echo.S /root/regression/cakeml-1635/basis/basis_ffi.o -o cake_echo Linking /root/regression/cakeml-1635/examples/compilation/x64/grepCompileScript.uo to produce theory-builder executable /root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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-1635/compiler/compilationLib.sml:711: 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: 1m37s, gctime: 2.0s, systime: 0.83263s. to_flat real: 1m38s to_flat size: 387627 Saved definition __ "flat_conf_def" Saved definition __ "flat_prog_def" to_clos eval: runtime: 5.9s, gctime: 0.28061s, systime: 0.09672s. to_clos real: 6.0s to_clos size: 163422 Saved definition __ "clos_prog_def" to_bvl eval: runtime: 35.1s, gctime: 1.2s, systime: 0.35996s. to_bvl real: 35.5s to_bvl size: 293259 Saved definition __ "bvl_conf_def" Saved definition __ "bvl_prog_def" Saved definition __ "bvl_names_def" to_bvi eval: runtime: 4m17s, gctime: 2.7s, systime: 1.4s. to_bvi real: 4m19s to_bvi size: 254526 Saved definition __ "bvi_conf_def" Saved definition __ "bvi_prog_def" Saved definition __ "bvi_names_def" to_data eval: runtime: 57.9s, gctime: 3.3s, systime: 0.53342s. to_data real: 58.4s to_data size: 468364 Saved theorem _____ "to_data_thm" data_to_word eval: runtime: 2m19s, gctime: 7.6s, systime: 0.96979s. data_to_word real: 2m20s data_to_word size: 1579797 Saved definition __ "word_to_word_fn_def" inst,ssa,two-reg (par) eval: runtime: 22m50s, gctime: 2m17s, systime: 40.1s. inst,ssa,two-reg (par) real: 17m44s inst,ssa,two-reg (par) size: 4926391 Saved definition __ "clash_fn_def" get_clash (par) eval: runtime: 10m43s, gctime: 1m47s, systime: 37.7s. get_clash (par) real: 3m20s get_clash (par) size: 7516528 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: 242 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: 17 coalesceable: 11 coalesced: 11 264 moves: 17 coalesceable: 11 coalesced: 11 265 moves: 17 coalesceable: 11 coalesced: 11 266 moves: 17 coalesceable: 11 coalesced: 11 267 moves: 17 coalesceable: 11 coalesced: 11 268 moves: 17 coalesceable: 11 coalesced: 11 269 moves: 17 coalesceable: 11 coalesced: 11 270 moves: 17 coalesceable: 11 coalesced: 11 271 moves: 17 coalesceable: 11 coalesced: 11 272 moves: 5885 coalesceable: 3532 coalesced: 3033 273 moves: 11474 coalesceable: 7187 coalesced: 6357 274 moves: 10448 coalesceable: 6311 coalesced: 5527 275 moves: 17 coalesceable: 11 coalesced: 11 276 moves: 17 coalesceable: 11 coalesced: 11 277 moves: 17 coalesceable: 11 coalesced: 11 278 moves: 17 coalesceable: 11 coalesced: 11 279 moves: 17 coalesceable: 11 coalesced: 11 280 moves: 17 coalesceable: 11 coalesced: 11 281 moves: 17 coalesceable: 11 coalesced: 11 282 moves: 17 coalesceable: 11 coalesced: 11 283 moves: 17 coalesceable: 11 coalesced: 11 284 moves: 17 coalesceable: 11 coalesced: 11 285 moves: 17 coalesceable: 11 coalesced: 11 286 moves: 102 coalesceable: 58 coalesced: 58 287 moves: 17 coalesceable: 11 coalesced: 11 288 moves: 17 coalesceable: 11 coalesced: 11 289 moves: 17 coalesceable: 11 coalesced: 11 290 moves: 17 coalesceable: 11 coalesced: 11 291 moves: 17 coalesceable: 11 coalesced: 11 292 moves: 17 coalesceable: 11 coalesced: 11 293 moves: 2705 coalesceable: 1486 coalesced: 1387 294 moves: 17 coalesceable: 11 coalesced: 11 295 moves: 17 coalesceable: 11 coalesced: 11 296 moves: 17 coalesceable: 11 coalesced: 11 297 moves: 17 coalesceable: 11 coalesced: 11 298 moves: 17 coalesceable: 11 coalesced: 11 299 moves: 158 coalesceable: 117 coalesced: 117 300 moves: 17 coalesceable: 11 coalesced: 11 301 moves: 17 coalesceable: 11 coalesced: 11 302 moves: 17 coalesceable: 11 coalesced: 11 303 moves: 17 coalesceable: 11 coalesced: 11 304 moves: 5 coalesceable: 3 coalesced: 3 305 moves: 4 coalesceable: 4 coalesced: 4 306 moves: 6 coalesceable: 6 coalesced: 6 307 moves: 4 coalesceable: 4 coalesced: 4 308 moves: 6 coalesceable: 6 coalesced: 6 309 moves: 8 coalesceable: 8 coalesced: 8 310 moves: 46 coalesceable: 34 coalesced: 33 311 moves: 4 coalesceable: 4 coalesced: 4 312 moves: 3 coalesceable: 3 coalesced: 3 313 moves: 6 coalesceable: 6 coalesced: 6 314 moves: 3 coalesceable: 3 coalesced: 2 315 moves: 8 coalesceable: 8 coalesced: 8 316 moves: 99 coalesceable: 63 coalesced: 50 317 moves: 6 coalesceable: 6 coalesced: 6 318 moves: 7 coalesceable: 7 coalesced: 4 319 moves: 6 coalesceable: 6 coalesced: 6 320 moves: 29 coalesceable: 19 coalesced: 13 321 moves: 8 coalesceable: 8 coalesced: 8 322 moves: 103 coalesceable: 64 coalesced: 59 323 moves: 4 coalesceable: 4 coalesced: 4 324 moves: 7 coalesceable: 7 coalesced: 7 325 moves: 6 coalesceable: 6 coalesced: 6 326 moves: 49 coalesceable: 36 coalesced: 34 327 moves: 6 coalesceable: 6 coalesced: 6 328 moves: 32 coalesceable: 23 coalesced: 18 329 moves: 4 coalesceable: 4 coalesced: 4 330 moves: 5 coalesceable: 5 coalesced: 3 331 moves: 4 coalesceable: 4 coalesced: 4 332 moves: 7 coalesceable: 7 coalesced: 7 333 moves: 6 coalesceable: 6 coalesced: 6 334 moves: 86 coalesceable: 57 coalesced: 51 335 moves: 6 coalesceable: 6 coalesced: 6 336 moves: 76 coalesceable: 47 coalesced: 43 337 moves: 6 coalesceable: 6 coalesced: 6 338 moves: 42 coalesceable: 27 coalesced: 25 339 moves: 4 coalesceable: 4 coalesced: 4 340 moves: 95 coalesceable: 58 coalesced: 57 341 moves: 6 coalesceable: 6 coalesced: 6 342 moves: 49 coalesceable: 37 coalesced: 35 343 moves: 4 coalesceable: 4 coalesced: 4 344 moves: 73 coalesceable: 49 coalesced: 47 345 moves: 6 coalesceable: 6 coalesced: 6 346 moves: 79 coalesceable: 57 coalesced: 54 347 moves: 6 coalesceable: 6 coalesced: 6 348 moves: 42 coalesceable: 27 coalesced: 26 349 moves: 4 coalesceable: 4 coalesced: 4 350 moves: 12 coalesceable: 11 coalesced: 9 351 moves: 4 coalesceable: 4 coalesced: 4 352 moves: 9 coalesceable: 9 coalesced: 8 353 moves: 4 coalesceable: 4 coalesced: 4 354 moves: 29 coalesceable: 12 coalesced: 11 355 moves: 8 coalesceable: 8 coalesced: 8 356 moves: 124 coalesceable: 72 coalesced: 58 357 moves: 6 coalesceable: 6 coalesced: 6 358 moves: 62 coalesceable: 31 coalesced: 29 359 moves: 4 coalesceable: 4 coalesced: 4 360 moves: 48 coalesceable: 23 coalesced: 21 361 moves: 6 coalesceable: 6 coalesced: 6 362 moves: 23 coalesceable: 15 coalesced: 11 363 moves: 6 coalesceable: 6 coalesced: 6 364 moves: 23 coalesceable: 15 coalesced: 11 365 moves: 6 coalesceable: 6 coalesced: 6 366 moves: 30 coalesceable: 19 coalesced: 16 367 moves: 6 coalesceable: 6 coalesced: 6 368 moves: 29 coalesceable: 21 coalesced: 17 369 moves: 6 coalesceable: 6 coalesced: 6 370 moves: 24 coalesceable: 16 coalesced: 13 371 moves: 6 coalesceable: 6 coalesced: 6 372 moves: 24 coalesceable: 16 coalesced: 13 373 moves: 6 coalesceable: 6 coalesced: 6 374 moves: 30 coalesceable: 22 coalesced: 19 375 moves: 6 coalesceable: 6 coalesced: 6 376 moves: 60 coalesceable: 44 coalesced: 41 377 moves: 6 coalesceable: 6 coalesced: 6 378 moves: 62 coalesceable: 31 coalesced: 29 379 moves: 4 coalesceable: 4 coalesced: 4 380 moves: 3 coalesceable: 3 coalesced: 3 381 moves: 4 coalesceable: 4 coalesced: 4 382 moves: 43 coalesceable: 29 coalesced: 25 383 moves: 4 coalesceable: 4 coalesced: 4 384 moves: 25 coalesceable: 18 coalesced: 16 385 moves: 4 coalesceable: 4 coalesced: 4 386 moves: 3 coalesceable: 3 coalesced: 3 387 moves: 6 coalesceable: 6 coalesced: 6 388 moves: 36 coalesceable: 23 coalesced: 17 389 moves: 6 coalesceable: 6 coalesced: 6 390 moves: 21 coalesceable: 19 coalesced: 19 391 moves: 4 coalesceable: 4 coalesced: 4 392 moves: 9 coalesceable: 9 coalesced: 8 393 moves: 8 coalesceable: 8 coalesced: 8 394 moves: 22 coalesceable: 20 coalesced: 20 395 moves: 12 coalesceable: 12 coalesced: 12 396 moves: 218 coalesceable: 134 coalesced: 94 397 moves: 12 coalesceable: 12 coalesced: 12 398 moves: 218 coalesceable: 134 coalesced: 94 399 moves: 8 coalesceable: 8 coalesced: 8 400 moves: 124 coalesceable: 72 coalesced: 58 401 moves: 4 coalesceable: 4 coalesced: 4 402 moves: 77 coalesceable: 56 coalesced: 53 403 moves: 6 coalesceable: 6 coalesced: 6 404 moves: 110 coalesceable: 79 coalesced: 69 405 moves: 8 coalesceable: 8 coalesced: 8 406 moves: 407 coalesceable: 208 coalesced: 175 407 moves: 4 coalesceable: 4 coalesced: 4 408 moves: 56 coalesceable: 33 coalesced: 30 409 moves: 4 coalesceable: 4 coalesced: 4 410 moves: 8 coalesceable: 6 coalesced: 6 411 moves: 8 coalesceable: 8 coalesced: 8 412 moves: 163 coalesceable: 110 coalesced: 96 413 moves: 6 coalesceable: 6 coalesced: 6 414 moves: 114 coalesceable: 80 coalesced: 72 415 moves: 4 coalesceable: 4 coalesced: 4 416 moves: 6 coalesceable: 6 coalesced: 6 417 moves: 4 coalesceable: 4 coalesced: 4 418 moves: 6 coalesceable: 6 coalesced: 6 419 moves: 8 coalesceable: 8 coalesced: 8 420 moves: 128 coalesceable: 77 coalesced: 70 421 moves: 8 coalesceable: 8 coalesced: 8 422 moves: 111 coalesceable: 66 coalesced: 51 423 moves: 6 coalesceable: 6 coalesced: 6 424 moves: 427 coalesceable: 263 coalesced: 198 425 moves: 4 coalesceable: 4 coalesced: 4 426 moves: 5 coalesceable: 5 coalesced: 5 427 moves: 4 coalesceable: 4 coalesced: 4 428 moves: 272 coalesceable: 139 coalesced: 131 429 moves: 4 coalesceable: 4 coalesced: 4 430 moves: 69 coalesceable: 54 coalesced: 54 431 moves: 6 coalesceable: 6 coalesced: 6 432 moves: 78 coalesceable: 59 coalesced: 56 433 moves: 4 coalesceable: 4 coalesced: 4 434 moves: 21 coalesceable: 18 coalesced: 16 435 moves: 4 coalesceable: 4 coalesced: 4 436 moves: 164 coalesceable: 106 coalesced: 89 437 moves: 224 coalesceable: 137 coalesced: 113 438 moves: 217 coalesceable: 133 coalesced: 108 439 moves: 4 coalesceable: 4 coalesced: 4 440 moves: 45 coalesceable: 26 coalesced: 24 441 moves: 6 coalesceable: 6 coalesced: 6 442 moves: 152 coalesceable: 102 coalesced: 97 443 moves: 6 coalesceable: 6 coalesced: 6 444 moves: 847 coalesceable: 556 coalesced: 502 445 moves: 6 coalesceable: 6 coalesced: 6 446 moves: 30 coalesceable: 21 coalesced: 16 447 moves: 4 coalesceable: 4 coalesced: 4 448 moves: 7 coalesceable: 7 coalesced: 7 449 moves: 6 coalesceable: 6 coalesced: 6 450 moves: 30 coalesceable: 17 coalesced: 16 451 moves: 10 coalesceable: 10 coalesced: 10 452 moves: 2844 coalesceable: 1470 coalesced: 781 453 moves: 10 coalesceable: 10 coalesced: 10 454 moves: 2803 coalesceable: 1454 coalesced: 770 455 moves: 4 coalesceable: 4 coalesced: 4 456 moves: 150 coalesceable: 86 coalesced: 76 457 moves: 4 coalesceable: 4 coalesced: 4 458 moves: 4 coalesceable: 4 coalesced: 4 459 moves: 8 coalesceable: 8 coalesced: 8 460 moves: 99 coalesceable: 63 coalesced: 57 461 moves: 8 coalesceable: 8 coalesced: 8 462 moves: 72 coalesceable: 48 coalesced: 44 463 moves: 10 coalesceable: 10 coalesced: 10 464 moves: 195 coalesceable: 104 coalesced: 68 465 moves: 8 coalesceable: 8 coalesced: 8 466 moves: 74 coalesceable: 47 coalesced: 43 467 moves: 6 coalesceable: 6 coalesced: 6 468 moves: 58 coalesceable: 40 coalesced: 33 469 moves: 6 coalesceable: 6 coalesced: 6 470 moves: 634 coalesceable: 440 coalesced: 316 471 moves: 6 coalesceable: 6 coalesced: 6 472 moves: 15 coalesceable: 15 coalesced: 15 473 moves: 4 coalesceable: 4 coalesced: 4 474 moves: 321 coalesceable: 204 coalesced: 200 475 moves: 8 coalesceable: 8 coalesced: 8 476 moves: 107 coalesceable: 65 coalesced: 65 477 moves: 10 coalesceable: 10 coalesced: 10 478 moves: 514 coalesceable: 292 coalesced: 271 479 moves: 4 coalesceable: 4 coalesced: 4 480 moves: 26 coalesceable: 19 coalesced: 17 481 moves: 8 coalesceable: 8 coalesced: 8 482 moves: 256 coalesceable: 149 coalesced: 130 483 moves: 8 coalesceable: 8 coalesced: 8 484 moves: 789 coalesceable: 475 coalesced: 427 485 moves: 6 coalesceable: 6 coalesced: 6 486 moves: 37 coalesceable: 23 coalesced: 22 487 moves: 4 coalesceable: 4 coalesced: 4 488 moves: 201 coalesceable: 119 coalesced: 113 489 moves: 6 coalesceable: 6 coalesced: 6 490 moves: 220 coalesceable: 158 coalesced: 129 491 moves: 4 coalesceable: 4 coalesced: 4 492 moves: 477 coalesceable: 295 coalesced: 290 493 moves: 6 coalesceable: 6 coalesced: 6 494 moves: 16 coalesceable: 9 coalesced: 6 495 moves: 6 coalesceable: 6 coalesced: 6 496 moves: 42 coalesceable: 26 coalesced: 25 497 moves: 4 coalesceable: 4 coalesced: 4 498 moves: 208 coalesceable: 121 coalesced: 117 499 moves: 4 coalesceable: 4 coalesced: 4 500 moves: 419 coalesceable: 260 coalesced: 230 501 moves: 4 coalesceable: 4 coalesced: 4 502 moves: 21 coalesceable: 14 coalesced: 13 503 moves: 6 coalesceable: 6 coalesced: 6 504 moves: 188 coalesceable: 117 coalesced: 112 505 moves: 6 coalesceable: 6 coalesced: 6 506 moves: 161 coalesceable: 117 coalesced: 95 507 moves: 4 coalesceable: 4 coalesced: 4 508 moves: 156 coalesceable: 103 coalesced: 98 509 moves: 4 coalesceable: 4 coalesced: 4 510 moves: 138 coalesceable: 92 coalesced: 88 511 moves: 4 coalesceable: 4 coalesced: 4 512 moves: 4 coalesceable: 4 coalesced: 4 513 moves: 4 coalesceable: 4 coalesced: 4 514 moves: 100 coalesceable: 64 coalesced: 61 515 moves: 6 coalesceable: 6 coalesced: 6 516 moves: 7 coalesceable: 7 coalesced: 7 517 moves: 10 coalesceable: 10 coalesced: 10 518 moves: 70 coalesceable: 61 coalesced: 55 519 moves: 4 coalesceable: 4 coalesced: 4 520 moves: 174 coalesceable: 110 coalesced: 105 521 moves: 4 coalesceable: 4 coalesced: 4 522 moves: 23 coalesceable: 15 coalesced: 14 523 moves: 9 coalesceable: 9 coalesced: 9 524 moves: 6 coalesceable: 6 coalesced: 6 525 moves: 232 coalesceable: 126 coalesced: 117 526 moves: 37 coalesceable: 23 coalesced: 20 527 moves: 4 coalesceable: 4 coalesced: 4 528 moves: 25 coalesceable: 16 coalesced: 14 529 moves: 10 coalesceable: 10 coalesced: 10 530 moves: 224 coalesceable: 128 coalesced: 94 531 moves: 8 coalesceable: 8 coalesced: 8 532 moves: 282 coalesceable: 163 coalesced: 151 533 moves: 8 coalesceable: 8 coalesced: 8 534 moves: 52 coalesceable: 37 coalesced: 31 535 moves: 6 coalesceable: 6 coalesced: 6 536 moves: 8 coalesceable: 8 coalesced: 6 537 moves: 6 coalesceable: 6 coalesced: 6 538 moves: 11 coalesceable: 11 coalesced: 9 539 moves: 10 coalesceable: 10 coalesced: 10 540 moves: 405 coalesceable: 209 coalesced: 162 541 moves: 10 coalesceable: 10 coalesced: 10 542 moves: 1186 coalesceable: 706 coalesced: 410 543 moves: 10 coalesceable: 10 coalesced: 10 544 moves: 96 coalesceable: 62 coalesced: 53 545 moves: 6 coalesceable: 6 coalesced: 6 546 moves: 24 coalesceable: 16 coalesced: 13 547 moves: 4 coalesceable: 4 coalesced: 4 548 moves: 36 coalesceable: 24 coalesced: 23 549 moves: 6 coalesceable: 6 coalesced: 6 550 moves: 24 coalesceable: 16 coalesced: 13 551 moves: 4 coalesceable: 4 coalesced: 4 552 moves: 147 coalesceable: 73 coalesced: 54 553 moves: 4 coalesceable: 4 coalesced: 4 554 moves: 89 coalesceable: 54 coalesced: 47 555 moves: 4 coalesceable: 4 coalesced: 4 556 moves: 22 coalesceable: 14 coalesced: 13 557 moves: 6 coalesceable: 6 coalesced: 6 558 moves: 40 coalesceable: 23 coalesced: 19 559 moves: 8 coalesceable: 8 coalesced: 8 560 moves: 64 coalesceable: 35 coalesced: 33 561 moves: 6 coalesceable: 6 coalesced: 6 562 moves: 24 coalesceable: 16 coalesced: 13 563 moves: 4 coalesceable: 4 coalesced: 4 564 moves: 59 coalesceable: 34 coalesced: 31 565 moves: 4 coalesceable: 4 coalesced: 4 566 moves: 252 coalesceable: 137 coalesced: 115 567 moves: 4 coalesceable: 4 coalesced: 4 568 moves: 18 coalesceable: 10 coalesced: 10 569 moves: 6 coalesceable: 6 coalesced: 6 570 moves: 148 coalesceable: 60 coalesced: 56 571 moves: 6 coalesceable: 6 coalesced: 6 572 moves: 112 coalesceable: 76 coalesced: 72 573 moves: 4 coalesceable: 4 coalesced: 4 574 moves: 6 coalesceable: 6 coalesced: 6 575 moves: 4 coalesceable: 4 coalesced: 4 576 moves: 6 coalesceable: 6 coalesced: 6 577 moves: 4 coalesceable: 4 coalesced: 4 578 moves: 6 coalesceable: 6 coalesced: 6 579 moves: 4 coalesceable: 4 coalesced: 4 580 moves: 6 coalesceable: 6 coalesced: 6 581 moves: 4 coalesceable: 4 coalesced: 4 582 moves: 6 coalesceable: 6 coalesced: 6 583 moves: 4 coalesceable: 4 coalesced: 4 584 moves: 6 coalesceable: 6 coalesced: 6 585 moves: 8 coalesceable: 8 coalesced: 8 586 moves: 96 coalesceable: 69 coalesced: 66 587 moves: 6 coalesceable: 6 coalesced: 6 588 moves: 12 coalesceable: 12 coalesced: 12 589 moves: 6 coalesceable: 6 coalesced: 6 590 moves: 76 coalesceable: 44 coalesced: 42 591 moves: 4 coalesceable: 4 coalesced: 4 592 moves: 25 coalesceable: 19 coalesced: 19 593 moves: 6 coalesceable: 6 coalesced: 6 594 moves: 86 coalesceable: 55 coalesced: 53 595 moves: 6 coalesceable: 6 coalesced: 6 596 moves: 77 coalesceable: 49 coalesced: 44 597 moves: 4 coalesceable: 4 coalesced: 4 598 moves: 21 coalesceable: 14 coalesced: 13 599 moves: 4 coalesceable: 4 coalesced: 4 600 moves: 21 coalesceable: 14 coalesced: 13 601 moves: 10 coalesceable: 10 coalesced: 8 602 moves: 3049 coalesceable: 1593 coalesced: 1296 603 moves: 4 coalesceable: 4 coalesced: 4 604 moves: 10 coalesceable: 9 coalesced: 9 605 moves: 6 coalesceable: 6 coalesced: 6 606 moves: 40 coalesceable: 25 coalesced: 24 607 moves: 18 coalesceable: 18 coalesced: 18 608 moves: 91 coalesceable: 53 coalesced: 37 609 moves: 4 coalesceable: 4 coalesced: 4 610 moves: 18 coalesceable: 16 coalesced: 16 611 moves: 4 coalesceable: 4 coalesced: 4 612 moves: 158 coalesceable: 90 coalesced: 87 613 moves: 4 coalesceable: 4 coalesced: 4 614 moves: 111 coalesceable: 80 coalesced: 77 615 moves: 4 coalesceable: 4 coalesced: 4 616 moves: 30 coalesceable: 19 coalesced: 18 617 moves: 4 coalesceable: 4 coalesced: 4 618 moves: 17 coalesceable: 15 coalesced: 15 619 moves: 4 coalesceable: 4 coalesced: 4 620 moves: 12 coalesceable: 11 coalesced: 11 621 moves: 4 coalesceable: 4 coalesced: 4 622 moves: 69 coalesceable: 40 coalesced: 39 623 moves: 6 coalesceable: 6 coalesced: 6 624 moves: 3 coalesceable: 3 coalesced: 2 625 moves: 6 coalesceable: 6 coalesced: 6 626 moves: 37 coalesceable: 22 coalesced: 21 627 moves: 6 coalesceable: 6 coalesced: 6 628 moves: 3 coalesceable: 3 coalesced: 3 629 moves: 6 coalesceable: 6 coalesced: 6 630 moves: 37 coalesceable: 22 coalesced: 21 631 moves: 4 coalesceable: 4 coalesced: 4 632 moves: 55 coalesceable: 35 coalesced: 31 633 moves: 6 coalesceable: 6 coalesced: 6 634 moves: 23 coalesceable: 21 coalesced: 21 635 moves: 4 coalesceable: 4 coalesced: 4 636 moves: 25 coalesceable: 17 coalesced: 16 637 moves: 4 coalesceable: 4 coalesced: 4 638 moves: 77 coalesceable: 51 coalesced: 48 639 moves: 6 coalesceable: 6 coalesced: 6 640 moves: 20 coalesceable: 18 coalesced: 14 641 moves: 38 coalesceable: 25 coalesced: 24 642 moves: 79 coalesceable: 50 coalesced: 47 643 moves: 6 coalesceable: 6 coalesced: 6 644 moves: 85 coalesceable: 57 coalesced: 54 645 moves: 4 coalesceable: 4 coalesced: 4 646 moves: 40 coalesceable: 25 coalesced: 24 647 moves: 6 coalesceable: 6 coalesced: 6 648 moves: 26 coalesceable: 19 coalesced: 19 649 moves: 4 coalesceable: 4 coalesced: 4 650 moves: 21 coalesceable: 14 coalesced: 13 651 moves: 4 coalesceable: 4 coalesced: 4 652 moves: 53 coalesceable: 34 coalesced: 32 653 moves: 167 coalesceable: 107 coalesced: 107 654 moves: 37 coalesceable: 26 coalesced: 25 655 moves: 6 coalesceable: 6 coalesced: 6 656 moves: 34 coalesceable: 23 coalesced: 21 657 moves: 4 coalesceable: 4 coalesced: 4 658 moves: 5 coalesceable: 5 coalesced: 5 659 moves: 38 coalesceable: 25 coalesced: 24 660 moves: 110 coalesceable: 74 coalesced: 72 661 moves: 6 coalesceable: 6 coalesced: 6 662 moves: 34 coalesceable: 23 coalesced: 21 663 moves: 32 coalesceable: 22 coalesced: 22 664 moves: 102 coalesceable: 69 coalesced: 67 665 moves: 6 coalesceable: 6 coalesced: 6 666 moves: 34 coalesceable: 23 coalesced: 21 667 moves: 4 coalesceable: 4 coalesced: 4 668 moves: 5 coalesceable: 5 coalesced: 5 669 moves: 4 coalesceable: 4 coalesced: 4 670 moves: 21 coalesceable: 14 coalesced: 13 671 moves: 4 coalesceable: 4 coalesced: 4 672 moves: 132 coalesceable: 89 coalesced: 80 673 moves: 4 coalesceable: 4 coalesced: 4 674 moves: 88 coalesceable: 59 coalesced: 56 675 moves: 4 coalesceable: 4 coalesced: 4 676 moves: 29 coalesceable: 23 coalesced: 21 677 moves: 4 coalesceable: 4 coalesced: 4 678 moves: 49 coalesceable: 37 coalesced: 37 679 moves: 4 coalesceable: 4 coalesced: 4 680 moves: 5 coalesceable: 5 coalesced: 5 681 moves: 4 coalesceable: 4 coalesced: 4 682 moves: 49 coalesceable: 37 coalesced: 37 683 moves: 4 coalesceable: 4 coalesced: 4 684 moves: 5 coalesceable: 5 coalesced: 5 685 moves: 4 coalesceable: 4 coalesced: 4 686 moves: 5 coalesceable: 5 coalesced: 5 687 moves: 4 coalesceable: 4 coalesced: 4 688 moves: 5 coalesceable: 5 coalesced: 5 689 moves: 4 coalesceable: 4 coalesced: 4 690 moves: 5 coalesceable: 5 coalesced: 5 691 moves: 4 coalesceable: 4 coalesced: 4 692 moves: 5 coalesceable: 5 coalesced: 5 693 moves: 4 coalesceable: 4 coalesced: 4 694 moves: 5 coalesceable: 5 coalesced: 5 695 moves: 4 coalesceable: 4 coalesced: 4 696 moves: 49 coalesceable: 29 coalesced: 28 697 moves: 4 coalesceable: 4 coalesced: 4 698 moves: 116 coalesceable: 73 coalesced: 65 699 moves: 8 coalesceable: 8 coalesced: 8 700 moves: 99 coalesceable: 51 coalesced: 48 701 moves: 4 coalesceable: 4 coalesced: 4 702 moves: 266 coalesceable: 170 coalesced: 166 703 moves: 6 coalesceable: 6 coalesced: 6 704 moves: 503 coalesceable: 392 coalesced: 384 705 moves: 125 coalesceable: 50 coalesced: 45 706 moves: 4 coalesceable: 4 coalesced: 4 707 moves: 210 coalesceable: 128 coalesced: 124 708 moves: 6 coalesceable: 6 coalesced: 6 709 moves: 14 coalesceable: 12 coalesced: 12 710 moves: 6 coalesceable: 6 coalesced: 6 711 moves: 35 coalesceable: 25 coalesced: 22 712 moves: 38 coalesceable: 28 coalesced: 23 713 moves: 4 coalesceable: 4 coalesced: 4 714 moves: 302 coalesceable: 186 coalesced: 181 runtime: 11m14s, gctime: 1.0s, systime: 6.2s. external oracle real: 11m20s external oracle size: 569362 apply colour (par) eval: runtime: 11m28s, gctime: 41.6s, systime: 42.7s. apply colour (par) real: 5m16s apply colour (par) size: 2183303 check colour eval: runtime: 30.8s, gctime: 1.6s, systime: 0.77314s. check colour real: 31.5s check colour size: 2184019 word_to_stack eval: runtime: 6m24s, gctime: 7.8s, systime: 7.7s. word_to_stack real: 6m32s word_to_stack size: 1708852 stack_rawcall eval: runtime: 3m47s, gctime: 3.3s, systime: 4.5s. stack_rawcall real: 3m51s stack_rawcall size: 1695515 stack_alloc (par) eval: runtime: 5m32s, gctime: 4.3s, systime: 15.9s. stack_alloc (par) real: 2m04s stack_alloc (par) size: 1711964 expand stack_remove_def eval: runtime: 0.07623s, gctime: 0.00000s, systime: 0.00000s. expand stack_remove_def real: 0.07627s expand stack_remove_def size: 3014 stack_remove (par) eval: runtime: 6m54s, gctime: 5.9s, systime: 12.9s. stack_remove (par) real: 2m08s stack_remove (par) size: 2813880 stack_names (par) eval: runtime: 3m52s, gctime: 5.6s, systime: 6.3s. stack_names (par) real: 1m25s stack_names (par) size: 2907898 stack_to_lab (par) eval: runtime: 8m25s, gctime: 36.2s, systime: 15.0s. stack_to_lab (par) real: 3m22s stack_to_lab (par) size: 3548641 lab_to_target eval: runtime: 18m50s, gctime: 1m46s, systime: 21.6s. lab_to_target real: 19m12s lab_to_target size: 5501916 export: runtime: 1.3s, gctime: 0.00000s, systime: 0.03663s. Saved theorem _____ "grep_compiled" Exporting theory "grepCompile" ... done. Theory "grepCompile" took 2h05m21s to build cc grep.S /root/regression/cakeml-1635/basis/basis_ffi.o -o cake_grep Linking /root/regression/cakeml-1635/examples/compilation/x64/helloCompileScript.uo to produce theory-builder executable /root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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-1635/compiler/compilationLib.sml:711: 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: 47.7s, gctime: 1.1s, systime: 1.1s. to_flat real: 48.8s to_flat size: 91230 Saved definition __ "flat_conf_def" Saved definition __ "flat_prog_def" to_clos eval: runtime: 0.37255s, gctime: 0.00000s, systime: 0.00330s. to_clos real: 0.37574s to_clos size: 34782 Saved definition __ "clos_prog_def" to_bvl eval: runtime: 8.6s, gctime: 0.27665s, systime: 0.04321s. to_bvl real: 8.6s to_bvl size: 56508 Saved definition __ "bvl_conf_def" Saved definition __ "bvl_prog_def" Saved definition __ "bvl_names_def" to_bvi eval: runtime: 1m25s, gctime: 0.63273s, systime: 0.67973s. to_bvi real: 1m26s to_bvi size: 64384 Saved definition __ "bvi_conf_def" Saved definition __ "bvi_prog_def" Saved definition __ "bvi_names_def" to_data eval: runtime: 20.7s, gctime: 0.90798s, systime: 0.28316s. to_data real: 21.0s to_data size: 112704 Saved theorem _____ "to_data_thm" data_to_word eval: runtime: 28.8s, gctime: 1.0s, systime: 0.32347s. data_to_word real: 29.1s data_to_word size: 388693 Saved definition __ "word_to_word_fn_def" inst,ssa,two-reg (par) eval: runtime: 2m03s, gctime: 5.1s, systime: 8.1s. inst,ssa,two-reg (par) real: 1m09s inst,ssa,two-reg (par) size: 1202030 Saved definition __ "clash_fn_def" get_clash (par) eval: runtime: 1m18s, gctime: 23.8s, systime: 5.0s. get_clash (par) real: 43.9s get_clash (par) size: 1871370 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: 960 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: 19.7s, gctime: 0.05420s, systime: 0.17975s. external oracle real: 19.8s external oracle size: 134303 apply colour (par) eval: runtime: 2m35s, gctime: 5.5s, systime: 18.7s. apply colour (par) real: 1m49s apply colour (par) size: 594449 check colour eval: runtime: 2.0s, gctime: 0.35306s, systime: 0.08991s. check colour real: 2.1s check colour size: 594640 word_to_stack eval: runtime: 2m00s, gctime: 3.2s, systime: 1.7s. word_to_stack real: 2m02s word_to_stack size: 488695 stack_rawcall eval: runtime: 1m04s, gctime: 1.3s, systime: 0.90944s. stack_rawcall real: 1m05s stack_rawcall size: 482597 stack_alloc (par) eval: runtime: 1m29s, gctime: 1.5s, systime: 7.7s. stack_alloc (par) real: 49.1s stack_alloc (par) size: 483879 expand stack_remove_def eval: runtime: 0.08367s, gctime: 0.00000s, systime: 0.00335s. expand stack_remove_def real: 0.08706s expand stack_remove_def size: 3014 stack_remove (par) eval: runtime: 2m04s, gctime: 2.6s, systime: 8.9s. stack_remove (par) real: 1m18s stack_remove (par) size: 828886 stack_names (par) eval: runtime: 1m01s, gctime: 1.6s, systime: 2.9s. stack_names (par) real: 32.3s stack_names (par) size: 855449 stack_to_lab (par) eval: runtime: 2m05s, gctime: 3.3s, systime: 7.4s. stack_to_lab (par) real: 1m06s stack_to_lab (par) size: 1038464 lab_to_target eval: runtime: 7m01s, gctime: 18.9s, systime: 10.3s. lab_to_target real: 7m11s lab_to_target size: 1736663 export: runtime: 0.81599s, gctime: 0.10464s, systime: 0.02679s. Saved theorem _____ "hello_compiled" Exporting theory "helloCompile" ... done. Theory "helloCompile" took 28m04s to build cc hello.S /root/regression/cakeml-1635/basis/basis_ffi.o -o cake_hello Linking /root/regression/cakeml-1635/examples/compilation/x64/helloErrCompileScript.uo to produce theory-builder executable /root/regression/HOL-7e1cdab63fa78a67a3fabc28a9f2a909e65b6921/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-1635/compiler/compilationLib.sml:711: 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: 0.97835s, systime: 0.98057s. to_flat real: 48.5s to_flat size: 92261 Saved definition __ "flat_conf_def" Saved definition __ "flat_prog_def" to_clos eval: runtime: 0.39027s, gctime: 0.00000s, systime: 0.00001s. to_clos real: 0.39024s to_clos size: 35437 Saved definition __ "clos_prog_def" to_bvl eval: runtime: 8.2s, gctime: 0.24939s, systime: 0.04673s. to_bvl real: 8.2s to_bvl size: 58153 Saved definition __ "bvl_conf_def" Saved definition __ "bvl_prog_def" Saved definition __ "bvl_names_def" to_bvi eval: runtime: 1m27s, gctime: 0.60220s, systime: 0.74319s. to_bvi real: 1m28s to_bvi size: 65979 Saved definition __ "bvi_conf_def" Saved definition __ "bvi_prog_def" Saved definition __ "bvi_names_def" to_data eval: runtime: 20.7s, gctime: 0.88591s, systime: 0.27670s. to_data real: 21.0s to_data size: 114735 Saved theorem _____ "to_data_thm" data_to_word eval: runtime: 28.9s, gctime: 1.0s, systime: 0.25005s. data_to_word real: 29.1s data_to_word size: 392905 Saved definition __ "word_to_word_fn_def" inst,ssa,two-reg (par) eval: runtime: 2m01s, gctime: 4.8s, systime: 6.2s. inst,ssa,two-reg (par) real: 1m07s inst,ssa,two-reg (par) size: 1209945 Saved definition __ "clash_fn_def" get_clash (par) eval: runtime: 1m19s, gctime: 22.4s, systime: 5.9s. get_clash (par) real: 41.9s get_clash (par) size: 1882211 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: 960 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.6s, gctime: 0.06248s, systime: 0.29009s. external oracle real: 18.9s external oracle size: 135446 apply colour (par) eval: runtime: 2m32s, gctime: 6.2s, systime: 10.0s. apply colour (par) real: 1m39s apply colour (par) size: 599534 check colour eval: runtime: 1.7s, gctime: 0.00000s, systime: 0.00009s. check colour real: 1.7s check colour size: 599732 word_to_stack eval: runtime: 2m02s, gctime: 3.9s, systime: 2.3s. word_to_stack real: 2m04s word_to_stack size: 492392 stack_rawcall eval: runtime: 1m04s, gctime: 1.2s, systime: 0.50325s. stack_rawcall real: 1m05s stack_rawcall size: 486205 stack_alloc (par) eval: runtime: 1m27s, gctime: 1.6s, systime: 4.1s. stack_alloc (par) real: 45.2s stack_alloc (par) size: 487547 expand stack_remove_def eval: runtime: 0.07762s, gctime: 0.00000s, systime: 0.00000s. expand stack_remove_def real: 0.07766s expand stack_remove_def size: 3014 stack_remove (par) eval: runtime: 2m04s, gctime: 3.0s, systime: 8.9s. stack_remove (par) real: 1m17s stack_remove (par) size: 834357 stack_names (par) eval: runtime: 1m04s, gctime: 2.0s, systime: 7.7s. stack_names (par) real: 36.5s stack_names (par) size: 861142 stack_to_lab (par) eval: runtime: 2m06s, gctime: 3.8s, systime: 4.8s. stack_to_lab (par) real: 1m05s stack_to_lab (par) size: 1045559 lab_to_target eval: runtime: 7m09s, gctime: 26.0s, systime: 4.7s. lab_to_target real: 7m14s lab_to_target size: 1749099 export: runtime: 0.91272s, gctime: 0.19738s, systime: 0.02648s. Saved theorem _____ "helloErr_compiled" Exporting theory "helloErrCompile" ... Run out of store - interrupting threads Failure while writing theory! error in quse /root/regression/cakeml-1635/examples/compilation/x64/helloErrCompileScript.sml : Interrupt error in load /root/regression/cakeml-1635/examples/compilation/x64/helloErrCompileScript : Interrupt Uncaught exception: Interrupt Failed script build for /root/regression/cakeml-1635/examples/compilation/x64/helloErrCompileScript - exited with code 1