OverviewCakeML:920bd6bbef687529958f58b39940a95e8ebefafb
Add serialiser to build-sequence
#835 (enc-dec)
Merging into:1cfcd59d4f8168f639ea94c4020ba0249898078a
Merge pull request #833 from CakeML/parse-err
HOL:424885cd3abe129d536c979db549b5efe69b23fa
Fix Unicode violation in topologyScript.sml
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 133MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 263MB
Starting semantics
Finished semantics 1m31s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m39s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 9s 357MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m11s 1GB
Starting basis/pure
Finished basis/pure 2m52s 863MB
Starting translator
Finished translator 3m14s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m10s 3GB
Starting characteristic
Finished characteristic 5m42s 1GB
Starting translator/monadic
Finished translator/monadic 1m42s 1GB
Starting basis
Finished basis 43m49s 16GB
Starting compiler/inference
Finished compiler/inference 1m14s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m07s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m31s 2GB
Starting compiler/backend
Finished compiler/backend 4m57s 4GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 23s 698MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 1m01s 1GB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 2m02s 1GB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 38s 949MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 1m28s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 1m47s 991MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 18s 635MB
Starting compiler/backend/x64
Finished compiler/backend/x64 19s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 22s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 20s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 21s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 20s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m09s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 6m51s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m30s 1GB
Starting compiler/backend/semantics
Finished compiler/backend/semantics 28m21s 2GB
Starting compiler/backend/reg_alloc/proofs
Finished compiler/backend/reg_alloc/proofs 3m30s 828MB
Starting compiler/backend/proofs
Finished compiler/backend/proofs 51m11s 16GB
Starting compiler/backend/serialiser
Finished compiler/backend/serialiser 1m09s 1GB
Starting compiler/encoders/x64/proofs
Finished compiler/encoders/x64/proofs 9m34s 4GB
Starting compiler/encoders/arm7/proofs
Finished compiler/encoders/arm7/proofs 13m04s 7GB
Starting compiler/encoders/arm8/proofs
Finished compiler/encoders/arm8/proofs 6m48s 1GB
Starting compiler/encoders/mips/proofs
Finished compiler/encoders/mips/proofs 9m55s 3GB
Starting compiler/encoders/riscv/proofs
Finished compiler/encoders/riscv/proofs 8m52s 1GB
Starting compiler/encoders/ag32/proofs
Finished compiler/encoders/ag32/proofs 2m32s 895MB
Starting compiler/backend/x64/proofs
Finished compiler/backend/x64/proofs 21s 1GB
Starting compiler/backend/arm7/proofs
Finished compiler/backend/arm7/proofs 23s 1GB
Starting compiler/backend/arm8/proofs
Finished compiler/backend/arm8/proofs 22s 1GB
Starting compiler/backend/mips/proofs
Finished compiler/backend/mips/proofs 23s 1GB
Starting compiler/backend/riscv/proofs
Finished compiler/backend/riscv/proofs 22s 1GB
Starting compiler/backend/ag32/proofs
Finished compiler/backend/ag32/proofs 12m16s 3GB
Starting compiler/proofs
Finished compiler/proofs 2m03s 5GB
Starting candle/set-theory
Finished candle/set-theory 29s 758MB
Starting candle/syntax-lib
Finished candle/syntax-lib 10s 704MB
Starting candle/standard/syntax
Finished candle/standard/syntax 1m50s 1GB
Starting candle/standard/semantics
Finished candle/standard/semantics 1m45s 1GB
Starting candle/standard/monadic
Finished candle/standard/monadic 1m42s 1GB
Starting candle/standard/ml_kernel
Finished candle/standard/ml_kernel 5m29s 5GB
Starting candle/overloading/syntax
Finished candle/overloading/syntax 3m09s 1GB
Starting candle/overloading/semantics
Finished candle/overloading/semantics 11m59s 4GB
Starting pancake
Finished pancake 1m51s 2GB
Starting pancake/ffi
Finished pancake/ffi 0s 8MB
Starting pancake/semantics
Finished pancake/semantics 2m15s 993MB
Starting pancake/proofs
Finished pancake/proofs 12m30s 7GB
Starting characteristic/examples
Finished characteristic/examples 1m19s 3GB
Starting tutorial/solutions
Finished tutorial/solutions 16m06s 9GB
Starting translator/monadic/examples
Finished translator/monadic/examples 3m15s 2GB
Starting examples
Finished examples 8m42s 4GB
Starting examples/compilation/x64
Finished examples/compilation/x64 2h30m33s 18GB
Starting examples/compilation/x64/proofs
Finished examples/compilation/x64/proofs 1m58s 3GB
Starting examples/compilation/ag32
FAILED: examples/compilation/ag32
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
/home/cug/hk324/cml-regression/cakeml-1585/developers/readme_gen helloCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml
Linking /home/cug/hk324/cml-regression/cakeml-1585/examples/compilation/ag32/helloCompileScript.uo to produce theory-builder executable
/home/cug/hk324/cml-regression/HOL-424885cd3abe129d536c979db549b5efe69b23fa/examples/l3-machine-code/x64/model/x64.sml:3757: warning: Matches are not exhaustive.
Found near
case (BitsN.fromBitstring ([c'2, ...], 3), p) of
(BitsN.B (0x0, ...), [... ...]) => Zfull_inst (p, (...)) |
(BitsN.B (...), [...]) => Zfull_inst (p, ...) |
(... ..., ...) => Zfull_inst (...) |
(...) => ... ... |
... => ... |
...
/home/cug/hk324/cml-regression/cakeml-1585/compiler/compilationLib.sml:706: 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: 19.5s, gctime: 0.29374s, systime: 0.30801s.
to_flat real: 19.9s
to_flat size: 89996
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
to_clos eval: runtime: 0.23300s, gctime: 0.05775s, systime: 0.00391s.
to_clos real: 0.23693s
to_clos size: 34302
Saved definition __ "clos_prog_def"
to_bvl eval: runtime: 3.5s, gctime: 0.09547s, systime: 0.00799s.
to_bvl real: 3.5s
to_bvl size: 56436
Saved definition __ "bvl_conf_def"
Saved definition __ "bvl_prog_def"
Saved definition __ "bvl_names_def"
to_bvi eval: runtime: 32.3s, gctime: 0.18882s, systime: 0.02410s.
to_bvi real: 32.3s
to_bvi size: 64204
Saved definition __ "bvi_conf_def"
Saved definition __ "bvi_prog_def"
Saved definition __ "bvi_names_def"
to_data eval: runtime: 9.5s, gctime: 0.43134s, systime: 0.02798s.
to_data real: 9.6s
to_data size: 112404
Saved theorem _____ "to_data_thm"
data_to_word eval: runtime: 9.4s, gctime: 0.33091s, systime: 0.06409s.
data_to_word real: 9.5s
data_to_word size: 368245
Saved definition __ "word_to_word_fn_def"
inst,ssa,two-reg (par) eval: runtime: 49.7s, gctime: 2.1s, systime: 0.27677s.
inst,ssa,two-reg (par) real: 26.2s
inst,ssa,two-reg (par) size: 1037351
Saved definition __ "clash_fn_def"
get_clash (par) eval: runtime: 33.4s, gctime: 8.6s, systime: 0.99472s.
get_clash (par) real: 16.8s
get_clash (par) size: 1600927
external oracle eval: Num regs: 58 Alg: IRC
0 moves: 56 coalesceable: 42 coalesced: 39
1 moves: 20 coalesceable: 18 coalesced: 17
2 moves: 56 coalesceable: 35 coalesced: 33
3 moves: 15 coalesceable: 9 coalesced: 7
4 moves: 14 coalesceable: 13 coalesced: 12
5 moves: 91 coalesceable: 59 coalesced: 56
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: 16 coalesceable: 14 coalesced: 14
12 moves: 33 coalesceable: 27 coalesced: 25
13 moves: 28 coalesceable: 17 coalesced: 14
14 moves: 43 coalesceable: 33 coalesced: 31
15 moves: 41 coalesceable: 34 coalesced: 33
16 moves: 11 coalesceable: 11 coalesced: 6
17 moves: 11 coalesceable: 6 coalesced: 6
18 moves: 17 coalesceable: 16 coalesced: 16
19 moves: 17 coalesceable: 16 coalesced: 15
20 moves: 15 coalesceable: 11 coalesced: 11
21 moves: 29 coalesceable: 23 coalesced: 19
22 moves: 30 coalesceable: 24 coalesced: 23
23 moves: 0 coalesceable: 0 coalesced: 0
24 moves: 16 coalesceable: 14 coalesced: 13
25 moves: 28 coalesceable: 24 coalesced: 20
26 moves: 17 coalesceable: 17 coalesced: 13
27 moves: 17 coalesceable: 17 coalesced: 13
28 moves: 0 coalesceable: 0 coalesced: 0
29 moves: 0 coalesceable: 0 coalesced: 0
30 moves: 262 coalesceable: 215 coalesced: 215
31 moves: 16 coalesceable: 13 coalesced: 13
32 moves: 13 coalesceable: 12 coalesced: 12
33 moves: 9 coalesceable: 8 coalesced: 8
34 moves: 17 coalesceable: 14 coalesced: 14
35 moves: 71 coalesceable: 62 coalesced: 62
36 moves: 64 coalesceable: 61 coalesced: 61
37 moves: 52 coalesceable: 49 coalesced: 49
38 moves: 78 coalesceable: 75 coalesced: 75
39 moves: 24 coalesceable: 21 coalesced: 21
40 moves: 35 coalesceable: 32 coalesced: 32
41 moves: 5 coalesceable: 4 coalesced: 4
42 moves: 17 coalesceable: 14 coalesced: 14
43 moves: 7 coalesceable: 6 coalesced: 6
44 moves: 15 coalesceable: 12 coalesced: 12
45 moves: 36 coalesceable: 33 coalesced: 33
46 moves: 5 coalesceable: 4 coalesced: 4
47 moves: 7 coalesceable: 6 coalesced: 6
48 moves: 14 coalesceable: 11 coalesced: 11
49 moves: 16 coalesceable: 13 coalesced: 13
50 moves: 10 coalesceable: 9 coalesced: 9
51 moves: 13 coalesceable: 10 coalesced: 10
52 moves: 15 coalesceable: 12 coalesced: 12
53 moves: 162 coalesceable: 92 coalesced: 80
54 moves: 80 coalesceable: 54 coalesced: 41
55 moves: 34 coalesceable: 19 coalesced: 18
56 moves: 28 coalesceable: 20 coalesced: 15
57 moves: 39 coalesceable: 26 coalesced: 21
58 moves: 57 coalesceable: 33 coalesced: 26
59 moves: 32 coalesceable: 22 coalesced: 17
60 moves: 55 coalesceable: 31 coalesced: 21
61 moves: 799 coalesceable: 469 coalesced: 363
62 moves: 960 coalesceable: 549 coalesced: 435
63 moves: 1045 coalesceable: 587 coalesced: 469
64 moves: 1134 coalesceable: 627 coalesced: 506
65 moves: 1227 coalesceable: 669 coalesced: 545
66 moves: 1324 coalesceable: 713 coalesced: 589
67 moves: 1425 coalesceable: 759 coalesced: 633
68 moves: 1530 coalesceable: 807 coalesced: 679
69 moves: 1639 coalesceable: 857 coalesced: 728
70 moves: 1752 coalesceable: 909 coalesced: 779
71 moves: 11 coalesceable: 9 coalesced: 9
72 moves: 13 coalesceable: 11 coalesced: 11
73 moves: 13 coalesceable: 10 coalesced: 9
74 moves: 15 coalesceable: 13 coalesced: 13
75 moves: 15 coalesceable: 12 coalesced: 11
76 moves: 15 coalesceable: 11 coalesced: 10
77 moves: 17 coalesceable: 15 coalesced: 15
78 moves: 17 coalesceable: 14 coalesced: 13
79 moves: 17 coalesceable: 13 coalesced: 12
80 moves: 17 coalesceable: 12 coalesced: 11
81 moves: 19 coalesceable: 17 coalesced: 17
82 moves: 19 coalesceable: 16 coalesced: 15
83 moves: 19 coalesceable: 15 coalesced: 14
84 moves: 19 coalesceable: 14 coalesced: 13
85 moves: 19 coalesceable: 13 coalesced: 12
86 moves: 21 coalesceable: 19 coalesced: 19
87 moves: 21 coalesceable: 18 coalesced: 17
88 moves: 21 coalesceable: 17 coalesced: 16
89 moves: 21 coalesceable: 16 coalesced: 15
90 moves: 21 coalesceable: 15 coalesced: 14
91 moves: 21 coalesceable: 14 coalesced: 13
92 moves: 23 coalesceable: 21 coalesced: 21
93 moves: 23 coalesceable: 20 coalesced: 19
94 moves: 23 coalesceable: 19 coalesced: 18
95 moves: 23 coalesceable: 18 coalesced: 17
96 moves: 23 coalesceable: 17 coalesced: 16
97 moves: 23 coalesceable: 16 coalesced: 15
98 moves: 23 coalesceable: 15 coalesced: 14
99 moves: 25 coalesceable: 23 coalesced: 23
100 moves: 25 coalesceable: 22 coalesced: 21
101 moves: 25 coalesceable: 21 coalesced: 20
102 moves: 25 coalesceable: 20 coalesced: 19
103 moves: 25 coalesceable: 19 coalesced: 18
104 moves: 25 coalesceable: 18 coalesced: 17
105 moves: 25 coalesceable: 17 coalesced: 16
106 moves: 25 coalesceable: 16 coalesced: 15
107 moves: 27 coalesceable: 25 coalesced: 25
108 moves: 27 coalesceable: 24 coalesced: 23
109 moves: 27 coalesceable: 23 coalesced: 22
110 moves: 27 coalesceable: 22 coalesced: 21
111 moves: 27 coalesceable: 21 coalesced: 20
112 moves: 27 coalesceable: 20 coalesced: 19
113 moves: 27 coalesceable: 19 coalesced: 18
114 moves: 27 coalesceable: 18 coalesced: 17
115 moves: 27 coalesceable: 17 coalesced: 16
116 moves: 57 coalesceable: 6 coalesced: 6
117 moves: 936 coalesceable: 2 coalesced: 2
118 moves: 11 coalesceable: 6 coalesced: 6
119 moves: 12 coalesceable: 6 coalesced: 6
120 moves: 12 coalesceable: 6 coalesced: 6
121 moves: 12 coalesceable: 6 coalesced: 6
122 moves: 12 coalesceable: 6 coalesced: 6
123 moves: 12 coalesceable: 6 coalesced: 6
124 moves: 12 coalesceable: 6 coalesced: 6
125 moves: 12 coalesceable: 6 coalesced: 6
126 moves: 12 coalesceable: 6 coalesced: 6
127 moves: 12 coalesceable: 6 coalesced: 6
128 moves: 2326 coalesceable: 524 coalesced: 524
129 moves: 12 coalesceable: 6 coalesced: 6
130 moves: 12 coalesceable: 6 coalesced: 6
131 moves: 12 coalesceable: 6 coalesced: 6
132 moves: 12 coalesceable: 6 coalesced: 6
133 moves: 12 coalesceable: 6 coalesced: 6
134 moves: 12 coalesceable: 6 coalesced: 6
135 moves: 12 coalesceable: 6 coalesced: 6
136 moves: 12 coalesceable: 6 coalesced: 6
137 moves: 10 coalesceable: 6 coalesced: 6
138 moves: 31 coalesceable: 12 coalesced: 11
139 moves: 12 coalesceable: 6 coalesced: 6
140 moves: 12 coalesceable: 6 coalesced: 6
141 moves: 12 coalesceable: 6 coalesced: 6
142 moves: 12 coalesceable: 6 coalesced: 6
143 moves: 2 coalesceable: 2 coalesced: 2
144 moves: 12 coalesceable: 6 coalesced: 6
145 moves: 5 coalesceable: 3 coalesced: 3
146 moves: 4 coalesceable: 4 coalesced: 4
147 moves: 4 coalesceable: 4 coalesced: 4
148 moves: 8 coalesceable: 8 coalesced: 8
149 moves: 114 coalesceable: 63 coalesced: 48
150 moves: 6 coalesceable: 6 coalesced: 6
151 moves: 20 coalesceable: 13 coalesced: 9
152 moves: 6 coalesceable: 6 coalesced: 6
153 moves: 20 coalesceable: 13 coalesced: 9
154 moves: 6 coalesceable: 6 coalesced: 6
155 moves: 25 coalesceable: 14 coalesced: 11
156 moves: 6 coalesceable: 6 coalesced: 6
157 moves: 30 coalesceable: 19 coalesced: 15
158 moves: 6 coalesceable: 6 coalesced: 6
159 moves: 23 coalesceable: 15 coalesced: 12
160 moves: 6 coalesceable: 6 coalesced: 6
161 moves: 23 coalesceable: 15 coalesced: 12
162 moves: 6 coalesceable: 6 coalesced: 6
163 moves: 29 coalesceable: 21 coalesced: 18
164 moves: 4 coalesceable: 4 coalesced: 4
165 moves: 25 coalesceable: 15 coalesced: 12
166 moves: 4 coalesceable: 4 coalesced: 4
167 moves: 3 coalesceable: 3 coalesced: 3
168 moves: 6 coalesceable: 6 coalesced: 6
169 moves: 10 coalesceable: 8 coalesced: 8
170 moves: 8 coalesceable: 8 coalesced: 8
171 moves: 11 coalesceable: 9 coalesced: 9
172 moves: 12 coalesceable: 12 coalesced: 12
173 moves: 199 coalesceable: 117 coalesced: 97
174 moves: 8 coalesceable: 8 coalesced: 8
175 moves: 154 coalesceable: 78 coalesced: 66
176 moves: 6 coalesceable: 6 coalesced: 6
177 moves: 82 coalesceable: 50 coalesced: 45
178 moves: 4 coalesceable: 4 coalesced: 4
179 moves: 4 coalesceable: 4 coalesced: 4
180 moves: 8 coalesceable: 8 coalesced: 8
181 moves: 105 coalesceable: 54 coalesced: 51
182 moves: 8 coalesceable: 8 coalesced: 8
183 moves: 104 coalesceable: 61 coalesced: 52
184 moves: 6 coalesceable: 6 coalesced: 6
185 moves: 391 coalesceable: 230 coalesced: 212
186 moves: 4 coalesceable: 4 coalesced: 4
187 moves: 5 coalesceable: 5 coalesced: 5
188 moves: 4 coalesceable: 4 coalesced: 4
189 moves: 25 coalesceable: 8 coalesced: 8
runtime: 8.1s, gctime: 0.01655s, systime: 0.00381s.
external oracle real: 8.1s
external oracle size: 149614
apply colour (par) eval: runtime: 1m06s, gctime: 2.2s, systime: 0.25196s.
apply colour (par) real: 43.5s
apply colour (par) size: 550934
check colour eval: runtime: 0.99284s, gctime: 0.07835s, systime: 0.01196s.
check colour real: 1.0s
check colour size: 551125
word_to_stack eval: runtime: 44.0s, gctime: 1.1s, systime: 0.15963s.
word_to_stack real: 44.2s
word_to_stack size: 401588
stack_rawcall eval: runtime: 23.5s, gctime: 0.43196s, systime: 0.03588s.
stack_rawcall real: 23.6s
stack_rawcall size: 396907
stack_alloc (par) eval: runtime: 32.0s, gctime: 0.74310s, systime: 0.08833s.
stack_alloc (par) real: 15.1s
stack_alloc (par) size: 398189
expand stack_remove_def eval: runtime: 0.05583s, gctime: 0.02550s, systime: 0.00400s.
expand stack_remove_def real: 0.05984s
expand stack_remove_def size: 3047
stack_remove (par) eval: runtime: 40.8s, gctime: 5.7s, systime: 0.43695s.
stack_remove (par) real: 22.9s
stack_remove (par) size: 615595
stack_names (par) eval: runtime: 21.7s, gctime: 0.62855s, systime: 0.11982s.
stack_names (par) real: 10.3s
stack_names (par) size: 618541
stack_to_lab (par) eval: runtime: 46.5s, gctime: 1.9s, systime: 0.23218s.
stack_to_lab (par) real: 22.4s
stack_to_lab (par) size: 780748
lab_to_target eval: runtime: 3m58s, gctime: 8.0s, systime: 1.2s.
lab_to_target real: 3m59s
lab_to_target size: 1644320
export: runtime: 0.33328s, gctime: 0.00000s, systime: 0.00001s.
error in quse /home/cug/hk324/cml-regression/cakeml-1585/examples/compilation/ag32/helloCompileScript.sml : HOL_ERR {message = "not a beta-redex", origin_function = "BETA_CONV", origin_structure = "Thm"}
error in load /home/cug/hk324/cml-regression/cakeml-1585/examples/compilation/ag32/helloCompileScript : HOL_ERR {message = "not a beta-redex", origin_function = "BETA_CONV", origin_structure = "Thm"}
Uncaught exception: HOL_ERR {message = "not a beta-redex", origin_function = "BETA_CONV", origin_structure = "Thm"}
Failed script build for /home/cug/hk324/cml-regression/cakeml-1585/examples/compilation/ag32/helloCompileScript - exited with code 1