Job 1583

CakeML:920bd6bbef687529958f58b39940a95e8ebefafb
  Add serialiser to build-sequence [Sep 17 04:52:46]
#835 (enc-dec)
Merging into:1cfcd59d4f8168f639ea94c4020ba0249898078a
  Merge pull request #833 from CakeML/parse-err [Sep 14 09:26:31]
HOL:9b9646dfe8c21bf1f359f11f3eedf37c281ac01b
  Holmake: "link-to-sigobj" now can/should be done in Holmakefiles [Sep 16 07:28:06]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Sep 17 04:57:08 Claimed job
Sep 17 04:57:16 Building HOL
Sep 17 05:09:36 Starting developers
Sep 17 05:09:38 Finished developers                                               2s 130MB
Sep 17 05:09:39 Starting developers/bin
Sep 17 05:09:45 Finished developers/bin                                           6s   1GB
Sep 17 05:09:45 Starting semantics/ffi
Sep 17 05:09:56 Finished semantics/ffi                                           10s 307MB
Sep 17 05:09:56 Starting semantics
Sep 17 05:11:33 Finished semantics                                             1m36s   1GB
Sep 17 05:11:33 Starting semantics/proofs
Sep 17 05:15:14 Finished semantics/proofs                                      3m40s   1GB
Sep 17 05:15:14 Starting semantics/alt_semantics
Sep 17 05:15:23 Finished semantics/alt_semantics                                  9s 393MB
Sep 17 05:15:23 Starting semantics/alt_semantics/proofs
Sep 17 05:17:39 Finished semantics/alt_semantics/proofs                        2m15s   1GB
Sep 17 05:17:39 Starting basis/pure
Sep 17 05:20:28 Finished basis/pure                                            2m48s   1GB
Sep 17 05:20:28 Starting translator
Sep 17 05:23:45 Finished translator                                            3m16s   2GB
Sep 17 05:23:45 Starting compiler/parsing
Sep 17 05:24:57 Finished compiler/parsing                                      1m11s   4GB
Sep 17 05:24:57 Starting characteristic
Sep 17 05:30:44 Finished characteristic                                        5m46s   3GB
Sep 17 05:30:45 Starting translator/monadic
Sep 17 05:32:34 Finished translator/monadic                                    1m49s   3GB
Sep 17 05:32:35 Starting basis
Sep 17 06:17:14 Finished basis                                                44m38s  29GB
Sep 17 06:17:14 Starting compiler/inference
Sep 17 06:18:28 Finished compiler/inference                                    1m13s   2GB
Sep 17 06:18:28 Starting compiler/backend/reg_alloc
Sep 17 06:19:36 Finished compiler/backend/reg_alloc                            1m07s   1GB
Sep 17 06:19:36 Starting compiler/backend/gc
Sep 17 06:23:16 Finished compiler/backend/gc                                   3m39s   4GB
Sep 17 06:23:16 Starting compiler/backend
Sep 17 06:28:37 Finished compiler/backend                                      5m20s   5GB
Sep 17 06:28:37 Starting compiler/encoders/asm
Sep 17 06:29:01 Finished compiler/encoders/asm                                   23s   1GB
Sep 17 06:29:01 Starting compiler/encoders/x64
Sep 17 06:30:05 Finished compiler/encoders/x64                                 1m03s   1GB
Sep 17 06:30:05 Starting compiler/encoders/arm7
Sep 17 06:32:09 Finished compiler/encoders/arm7                                2m03s   1GB
Sep 17 06:32:09 Starting compiler/encoders/arm8
Sep 17 06:32:49 Finished compiler/encoders/arm8                                  40s   1GB
Sep 17 06:32:49 Starting compiler/encoders/mips
Sep 17 06:34:15 Finished compiler/encoders/mips                                1m25s   1GB
Sep 17 06:34:15 Starting compiler/encoders/riscv
Sep 17 06:35:55 Finished compiler/encoders/riscv                               1m39s   1GB
Sep 17 06:35:56 Starting compiler/encoders/ag32
Sep 17 06:36:15 Finished compiler/encoders/ag32                                  19s 932MB
Sep 17 06:36:15 Starting compiler/backend/x64
Sep 17 06:36:36 Finished compiler/backend/x64                                    20s   1GB
Sep 17 06:36:36 Starting compiler/backend/arm7
Sep 17 06:36:59 Finished compiler/backend/arm7                                   22s   1GB
Sep 17 06:36:59 Starting compiler/backend/arm8
Sep 17 06:37:20 Finished compiler/backend/arm8                                   21s   1GB
Sep 17 06:37:21 Starting compiler/backend/mips
Sep 17 06:37:43 Finished compiler/backend/mips                                   21s   1GB
Sep 17 06:37:43 Starting compiler/backend/riscv
Sep 17 06:38:05 Finished compiler/backend/riscv                                  22s   1GB
Sep 17 06:38:05 Starting compiler/backend/ag32
Sep 17 06:39:19 Finished compiler/backend/ag32                                 1m13s   2GB
Sep 17 06:39:19 Starting compiler/parsing/proofs
Sep 17 06:46:05 Finished compiler/parsing/proofs                               6m45s   2GB
Sep 17 06:46:05 Starting compiler/inference/proofs
Sep 17 06:48:39 Finished compiler/inference/proofs                             2m33s   1GB
Sep 17 06:48:39 Starting compiler/backend/semantics
Sep 17 07:16:32 Finished compiler/backend/semantics                           27m52s   4GB
Sep 17 07:16:32 Starting compiler/backend/reg_alloc/proofs
Sep 17 07:24:18 Finished compiler/backend/reg_alloc/proofs                     7m43s   1GB
Sep 17 07:24:18 Starting compiler/backend/proofs
Sep 17 08:57:13 Finished compiler/backend/proofs                            1h32m55s  32GB
Sep 17 08:57:14 Starting compiler/backend/serialiser
Sep 17 08:58:25 Finished compiler/backend/serialiser                           1m11s   2GB
Sep 17 08:58:25 Starting compiler/encoders/x64/proofs
Sep 17 09:08:38 Finished compiler/encoders/x64/proofs                         10m12s   6GB
Sep 17 09:08:38 Starting compiler/encoders/arm7/proofs
Sep 17 09:22:08 Finished compiler/encoders/arm7/proofs                        13m29s  10GB
Sep 17 09:22:08 Starting compiler/encoders/arm8/proofs
Sep 17 09:29:06 Finished compiler/encoders/arm8/proofs                         6m57s   3GB
Sep 17 09:29:06 Starting compiler/encoders/mips/proofs
Sep 17 09:39:26 Finished compiler/encoders/mips/proofs                        10m19s   5GB
Sep 17 09:39:26 Starting compiler/encoders/riscv/proofs
Sep 17 09:48:14 Finished compiler/encoders/riscv/proofs                        8m47s   3GB
Sep 17 09:48:14 Starting compiler/encoders/ag32/proofs
Sep 17 09:50:45 Finished compiler/encoders/ag32/proofs                         2m30s   1GB
Sep 17 09:50:45 Starting compiler/backend/x64/proofs
Sep 17 09:51:10 Finished compiler/backend/x64/proofs                             24s   2GB
Sep 17 09:51:10 Starting compiler/backend/arm7/proofs
Sep 17 09:51:36 Finished compiler/backend/arm7/proofs                            26s   2GB
Sep 17 09:51:37 Starting compiler/backend/arm8/proofs
Sep 17 09:52:00 Finished compiler/backend/arm8/proofs                            23s   1GB
Sep 17 09:52:01 Starting compiler/backend/mips/proofs
Sep 17 09:52:25 Finished compiler/backend/mips/proofs                            24s   1GB
Sep 17 09:52:25 Starting compiler/backend/riscv/proofs
Sep 17 09:52:52 Finished compiler/backend/riscv/proofs                           26s   2GB
Sep 17 09:52:52 Starting compiler/backend/ag32/proofs
Sep 17 10:05:38 Finished compiler/backend/ag32/proofs                         12m45s   3GB
Sep 17 10:05:38 Starting compiler/proofs
Sep 17 10:07:44 Finished compiler/proofs                                       2m05s   6GB
Sep 17 10:07:44 Starting candle/set-theory
Sep 17 10:08:14 Finished candle/set-theory                                       29s   1GB
Sep 17 10:08:14 Starting candle/syntax-lib
Sep 17 10:08:26 Finished candle/syntax-lib                                       11s 841MB
Sep 17 10:08:26 Starting candle/standard/syntax
Sep 17 10:10:21 Finished candle/standard/syntax                                1m54s   1GB
Sep 17 10:10:21 Starting candle/standard/semantics
Sep 17 10:12:11 Finished candle/standard/semantics                             1m50s   2GB
Sep 17 10:12:11 Starting candle/standard/monadic
Sep 17 10:13:55 Finished candle/standard/monadic                               1m43s   1GB
Sep 17 10:13:55 Starting candle/standard/ml_kernel
Sep 17 10:19:29 Finished candle/standard/ml_kernel                             5m33s   6GB
Sep 17 10:19:29 Starting candle/overloading/syntax
Sep 17 10:22:43 Finished candle/overloading/syntax                             3m13s   1GB
Sep 17 10:22:43 Starting candle/overloading/semantics
Sep 17 10:34:51 Finished candle/overloading/semantics                         12m07s   8GB
Sep 17 10:34:52 Starting pancake
Sep 17 10:36:55 Finished pancake                                               2m03s   3GB
Sep 17 10:36:55 Starting pancake/ffi
Sep 17 10:36:56 Finished pancake/ffi                                              0s   6MB
Sep 17 10:36:56 Starting pancake/semantics
Sep 17 10:39:11 Finished pancake/semantics                                     2m15s   2GB
Sep 17 10:39:11 Starting pancake/proofs
Sep 17 10:51:56 Finished pancake/proofs                                       12m44s   7GB
Sep 17 10:51:56 Starting characteristic/examples
Sep 17 10:53:18 Finished characteristic/examples                               1m21s   5GB
Sep 17 10:53:19 Starting tutorial/solutions
Sep 17 11:10:05 Finished tutorial/solutions                                   16m45s  12GB
Sep 17 11:10:05 Starting translator/monadic/examples
Sep 17 11:13:33 Finished translator/monadic/examples                           3m27s   3GB
Sep 17 11:13:33 Starting examples
Sep 17 11:23:04 Finished examples                                              9m30s   6GB
Sep 17 11:23:04 Starting examples/compilation/x64
Sep 17 13:55:42 Finished examples/compilation/x64                           2h32m37s  25GB
Sep 17 13:55:42 Starting examples/compilation/x64/proofs
Sep 17 13:57:47 Finished examples/compilation/x64/proofs                       2m04s   3GB
Sep 17 13:57:47 Starting examples/compilation/ag32
Sep 17 14:08:08 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/myreen/regression/cakeml-1583/developers/readme_gen helloCompileScript.sml sortCompileScript.sml wordcountCompileScript.sml  
Linking /home/myreen/regression/cakeml-1583/examples/compilation/ag32/helloCompileScript.uo to produce theory-builder executable
/home/myreen/regression/HOL-9b9646dfe8c21bf1f359f11f3eedf37c281ac01b/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/myreen/regression/cakeml-1583/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: 21.7s,    gctime: 2.7s,     systime: 0.88417s.
                to_flat real: 22.6s
                to_flat size: 89996
Saved definition __ "flat_conf_def"
Saved definition __ "flat_prog_def"
                to_clos eval: runtime: 0.17498s,    gctime: 0.00000s,     systime: 0.00000s.
                to_clos real: 0.17499s
                to_clos size: 34302
Saved definition __ "clos_prog_def"
                 to_bvl eval: runtime: 3.4s,    gctime: 0.12040s,     systime: 0.03987s.
                 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.15984s,     systime: 0.03196s.
                 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.2s,    gctime: 0.36395s,     systime: 0.02405s.
                to_data real: 9.2s
                to_data size: 112404
Saved theorem _____ "to_data_thm"
           data_to_word eval: runtime: 9.2s,    gctime: 0.47926s,     systime: 0.05602s.
           data_to_word real: 9.2s
           data_to_word size: 368245
Saved definition __ "word_to_word_fn_def"
 inst,ssa,two-reg (par) eval: runtime: 49.5s,    gctime: 1.8s,     systime: 0.22000s.
 inst,ssa,two-reg (par) real: 25.5s
 inst,ssa,two-reg (par) size: 1037351
Saved definition __ "clash_fn_def"
        get_clash (par) eval: runtime: 30.7s,    gctime: 2.1s,     systime: 0.18395s.
        get_clash (par) real: 10.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: 7.8s,    gctime: 0.00785s,     systime: 0.00003s.
        external oracle real: 7.8s
        external oracle size: 149614
     apply colour (par) eval: runtime: 1m07s,    gctime: 2.1s,     systime: 0.22829s.
     apply colour (par) real: 43.6s
     apply colour (par) size: 550934
           check colour eval: runtime: 1.2s,    gctime: 0.15382s,     systime: 0.01597s.
           check colour real: 1.2s
           check colour size: 551125
          word_to_stack eval: runtime: 50.5s,    gctime: 8.7s,     systime: 1.0s.
          word_to_stack real: 51.6s
          word_to_stack size: 401588
          stack_rawcall eval: runtime: 26.3s,    gctime: 3.9s,     systime: 0.98002s.
          stack_rawcall real: 27.3s
          stack_rawcall size: 396907
      stack_alloc (par) eval: runtime: 30.9s,    gctime: 0.39589s,     systime: 0.29622s.
      stack_alloc (par) real: 14.4s
      stack_alloc (par) size: 398189
expand stack_remove_def eval: runtime: 0.03183s,    gctime: 0.00000s,     systime: 0.00000s.
expand stack_remove_def real: 0.03185s
expand stack_remove_def size: 3047
     stack_remove (par) eval: runtime: 34.2s,    gctime: 0.45361s,     systime: 0.05622s.
     stack_remove (par) real: 16.6s
     stack_remove (par) size: 615595
      stack_names (par) eval: runtime: 20.3s,    gctime: 0.38475s,     systime: 0.04799s.
      stack_names (par) real: 9.5s
      stack_names (par) size: 618541
     stack_to_lab (par) eval: runtime: 44.4s,    gctime: 0.79066s,     systime: 0.08830s.
     stack_to_lab (par) real: 20.7s
     stack_to_lab (par) size: 780748
          lab_to_target eval: runtime: 4m13s,    gctime: 28.6s,     systime: 3.1s.
          lab_to_target real: 4m16s
          lab_to_target size: 1644320
                      export: runtime: 0.36423s,    gctime: 0.00000s,     systime: 0.00000s.
error in quse /home/myreen/regression/cakeml-1583/examples/compilation/ag32/helloCompileScript.sml : HOL_ERR {message = "not a beta-redex", origin_function = "BETA_CONV", origin_structure = "Thm"}
error in load /home/myreen/regression/cakeml-1583/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/myreen/regression/cakeml-1583/examples/compilation/ag32/helloCompileScript - exited with code 1