Job 1597

CakeML:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
  Merge pull request #839 from CakeML/lpr_transform [Oct 03 11:04:50]
HOL:15ffb68bca5fbedbdf77e12384dffc33ecc2606b
  Fix generateBuildSummary to cope with lines without [ [Oct 01 04:59:11]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Oct 03 11:15:37 Claimed job
Oct 03 11:15:41 Building HOL
Oct 03 11:27:17 Starting developers
Oct 03 11:27:22 Finished developers                                               4s 119MB
Oct 03 11:27:22 Starting developers/bin
Oct 03 11:27:28 Finished developers/bin                                           6s   1GB
Oct 03 11:27:28 Starting semantics/ffi
Oct 03 11:27:39 Finished semantics/ffi                                           10s 262MB
Oct 03 11:27:39 Starting semantics
Oct 03 11:29:12 Finished semantics                                             1m32s   1GB
Oct 03 11:29:12 Starting semantics/proofs
Oct 03 11:32:50 Finished semantics/proofs                                      3m37s   1GB
Oct 03 11:32:50 Starting semantics/alt_semantics
Oct 03 11:33:02 Finished semantics/alt_semantics                                 11s 364MB
Oct 03 11:33:02 Starting semantics/alt_semantics/proofs
Oct 03 11:35:33 Finished semantics/alt_semantics/proofs                        2m31s 762MB
Oct 03 11:35:33 Starting basis/pure
Oct 03 11:38:24 Finished basis/pure                                            2m50s 940MB
Oct 03 11:38:24 Starting translator
Oct 03 11:41:38 Finished translator                                            3m13s   1GB
Oct 03 11:41:38 Starting compiler/parsing
Oct 03 11:42:51 Finished compiler/parsing                                      1m12s   2GB
Oct 03 11:42:51 Starting characteristic
Oct 03 11:48:35 Finished characteristic                                        5m43s   1GB
Oct 03 11:48:35 Starting translator/monadic
Oct 03 11:50:20 Finished translator/monadic                                    1m45s   1GB
Oct 03 11:50:20 Starting basis
Oct 03 12:35:54 Finished basis                                                45m31s  26GB
Oct 03 12:35:54 Starting compiler/inference
Oct 03 12:37:09 Finished compiler/inference                                    1m15s   1GB
Oct 03 12:37:09 Starting compiler/backend/reg_alloc
Oct 03 12:38:19 Finished compiler/backend/reg_alloc                            1m09s   1GB
Oct 03 12:38:19 Starting compiler/backend/gc
Oct 03 12:41:50 Finished compiler/backend/gc                                   3m30s   2GB
Oct 03 12:41:50 Starting compiler/backend
Oct 03 12:46:51 Finished compiler/backend                                      5m01s   3GB
Oct 03 12:46:51 Starting compiler/encoders/asm
Oct 03 12:47:15 Finished compiler/encoders/asm                                   23s 658MB
Oct 03 12:47:15 Starting compiler/encoders/x64
Oct 03 12:48:17 Finished compiler/encoders/x64                                 1m02s   1GB
Oct 03 12:48:18 Starting compiler/encoders/arm7
Oct 03 12:50:18 Finished compiler/encoders/arm7                                2m00s   1GB
Oct 03 12:50:19 Starting compiler/encoders/arm8
Oct 03 12:50:56 Finished compiler/encoders/arm8                                  37s 640MB
Oct 03 12:50:56 Starting compiler/encoders/mips
Oct 03 12:52:24 Finished compiler/encoders/mips                                1m27s   1GB
Oct 03 12:52:25 Starting compiler/encoders/riscv
Oct 03 12:54:07 Finished compiler/encoders/riscv                               1m42s   1GB
Oct 03 12:54:07 Starting compiler/encoders/ag32
Oct 03 12:54:26 Finished compiler/encoders/ag32                                  18s 929MB
Oct 03 12:54:26 Starting compiler/backend/x64
Oct 03 12:54:45 Finished compiler/backend/x64                                    19s   1GB
Oct 03 12:54:45 Starting compiler/backend/arm7
Oct 03 12:55:07 Finished compiler/backend/arm7                                   21s   1GB
Oct 03 12:55:07 Starting compiler/backend/arm8
Oct 03 12:55:27 Finished compiler/backend/arm8                                   20s   1GB
Oct 03 12:55:27 Starting compiler/backend/mips
Oct 03 12:55:48 Finished compiler/backend/mips                                   20s   1GB
Oct 03 12:55:48 Starting compiler/backend/riscv
Oct 03 12:56:09 Finished compiler/backend/riscv                                  20s   1GB
Oct 03 12:56:09 Starting compiler/backend/ag32
Oct 03 12:57:20 Finished compiler/backend/ag32                                 1m10s   1GB
Oct 03 12:57:20 Starting compiler/parsing/proofs
Oct 03 13:03:59 Finished compiler/parsing/proofs                               6m39s   1GB
Oct 03 13:03:59 Starting compiler/inference/proofs
Oct 03 13:06:30 Finished compiler/inference/proofs                             2m29s   1GB
Oct 03 13:06:30 Starting compiler/backend/semantics
Oct 03 13:33:50 Finished compiler/backend/semantics                           27m20s   2GB
Oct 03 13:33:50 Starting compiler/backend/reg_alloc/proofs
Oct 03 13:37:20 Finished compiler/backend/reg_alloc/proofs                     3m28s 922MB
Oct 03 13:37:20 Starting compiler/backend/proofs
Oct 03 14:28:46 Finished compiler/backend/proofs                              51m25s  16GB
Oct 03 14:28:46 Starting compiler/backend/serialiser
Oct 03 14:29:54 Finished compiler/backend/serialiser                           1m08s   1GB
Oct 03 14:29:54 Starting compiler/encoders/x64/proofs
Oct 03 14:39:35 Finished compiler/encoders/x64/proofs                          9m39s   4GB
Oct 03 14:39:35 Starting compiler/encoders/arm7/proofs
Oct 03 14:52:42 Finished compiler/encoders/arm7/proofs                        13m06s   7GB
Oct 03 14:52:42 Starting compiler/encoders/arm8/proofs
Oct 03 14:59:24 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Oct 03 14:59:24 Starting compiler/encoders/mips/proofs
Oct 03 15:09:30 Finished compiler/encoders/mips/proofs                        10m05s   1GB
Oct 03 15:09:30 Starting compiler/encoders/riscv/proofs
Oct 03 15:18:29 Finished compiler/encoders/riscv/proofs                        8m59s   1GB
Oct 03 15:18:29 Starting compiler/encoders/ag32/proofs
Oct 03 15:21:04 Finished compiler/encoders/ag32/proofs                         2m34s 712MB
Oct 03 15:21:04 Starting compiler/backend/x64/proofs
Oct 03 15:21:27 Finished compiler/backend/x64/proofs                             22s   1GB
Oct 03 15:21:27 Starting compiler/backend/arm7/proofs
Oct 03 15:21:51 Finished compiler/backend/arm7/proofs                            23s   1GB
Oct 03 15:21:51 Starting compiler/backend/arm8/proofs
Oct 03 15:22:13 Finished compiler/backend/arm8/proofs                            21s   1GB
Oct 03 15:22:13 Starting compiler/backend/mips/proofs
Oct 03 15:22:36 Finished compiler/backend/mips/proofs                            22s   1GB
Oct 03 15:22:36 Starting compiler/backend/riscv/proofs
Oct 03 15:22:58 Finished compiler/backend/riscv/proofs                           22s   1GB
Oct 03 15:22:58 Starting compiler/backend/ag32/proofs
Oct 03 15:35:43 Finished compiler/backend/ag32/proofs                         12m44s   2GB
Oct 03 15:35:43 Starting compiler/proofs
Oct 03 15:37:46 Finished compiler/proofs                                       2m02s   2GB
Oct 03 15:37:46 Starting candle/set-theory
Oct 03 15:38:16 Finished candle/set-theory                                       29s 787MB
Oct 03 15:38:16 Starting candle/syntax-lib
Oct 03 15:38:27 Finished candle/syntax-lib                                       10s 514MB
Oct 03 15:38:27 Starting candle/standard/syntax
Oct 03 15:40:20 Finished candle/standard/syntax                                1m51s 959MB
Oct 03 15:40:20 Starting candle/standard/semantics
Oct 03 15:42:04 Finished candle/standard/semantics                             1m43s   1GB
Oct 03 15:42:04 Starting candle/standard/monadic
Oct 03 15:43:47 Finished candle/standard/monadic                               1m42s   1GB
Oct 03 15:43:47 Starting candle/standard/ml_kernel
Oct 03 15:49:24 Finished candle/standard/ml_kernel                             5m36s   5GB
Oct 03 15:49:24 Starting candle/overloading/syntax
Oct 03 15:52:33 Finished candle/overloading/syntax                             3m08s   1GB
Oct 03 15:52:33 Starting candle/overloading/semantics
Oct 03 16:04:49 Finished candle/overloading/semantics                         12m15s   3GB
Oct 03 16:04:49 Starting pancake
Oct 03 16:06:39 Finished pancake                                               1m50s   2GB
Oct 03 16:06:39 Starting pancake/ffi
Oct 03 16:06:40 Finished pancake/ffi                                              0s   8MB
Oct 03 16:06:40 Starting pancake/semantics
Oct 03 16:08:58 Finished pancake/semantics                                     2m18s   1GB
Oct 03 16:08:59 Starting pancake/proofs
Oct 03 16:21:23 Finished pancake/proofs                                       12m23s   7GB
Oct 03 16:21:23 Starting characteristic/examples
Oct 03 16:22:45 Finished characteristic/examples                               1m22s   3GB
Oct 03 16:22:45 Starting tutorial/solutions
Oct 03 16:38:54 Finished tutorial/solutions                                   16m08s   7GB
Oct 03 16:38:54 Starting translator/monadic/examples
Oct 03 16:42:08 Finished translator/monadic/examples                           3m12s   3GB
Oct 03 16:42:08 Starting examples
Oct 03 16:51:10 Finished examples                                              9m01s   3GB
Oct 03 16:51:10 Starting examples/compilation/x64
Oct 03 19:20:04 Finished examples/compilation/x64                           2h28m50s  19GB
Oct 03 19:20:05 Starting examples/compilation/x64/proofs
Oct 03 19:21:54 Finished examples/compilation/x64/proofs                       1m48s   3GB
Oct 03 19:21:54 Starting examples/compilation/ag32
Oct 03 19:56:11 Finished examples/compilation/ag32                            34m16s   9GB
Oct 03 19:56:11 Starting examples/compilation/ag32/proofs
Oct 03 19:57:02 Finished examples/compilation/ag32/proofs                        51s   4GB
Oct 03 19:57:02 Starting examples/cost
Oct 03 20:51:12 Finished examples/cost                                        54m08s   8GB
Oct 03 20:51:12 Starting examples/lpr_checker
Oct 03 20:52:00 Finished examples/lpr_checker                                    47s   1GB
Oct 03 20:52:00 Starting examples/lpr_checker/array
Oct 03 21:19:38 Finished examples/lpr_checker/array                           27m37s   6GB
Oct 03 21:19:38 Starting examples/lpr_checker/array/compilation
Oct 03 22:40:48 Finished examples/lpr_checker/array/compilation             1h21m07s  35GB
Oct 03 22:40:48 Starting examples/lpr_checker/array/compilation/proofs
Oct 03 22:42:01 Finished examples/lpr_checker/array/compilation/proofs         1m12s   6GB
Oct 03 22:42:01 Starting examples/opentheory
Oct 03 22:51:51 Finished examples/opentheory                                   9m49s   6GB
Oct 03 22:51:51 Starting examples/opentheory
Oct 03 22:51:52 Finished examples/opentheory                                      1s  35MB
Oct 03 22:51:52 Starting examples/opentheory/compilation
Oct 03 23:27:23 Finished examples/opentheory/compilation                      35m30s  29GB
Oct 03 23:27:24 Starting examples/opentheory/compilation/proofs
Oct 03 23:28:09 Finished examples/opentheory/compilation/proofs                  45s   3GB
Oct 03 23:28:09 Starting examples/opentheory/compilation/ag32
Oct 04 00:05:53 Finished examples/opentheory/compilation/ag32                 37m41s  29GB
Oct 04 00:05:53 Starting examples/opentheory/compilation/ag32/proofs
Oct 04 00:07:29 Finished examples/opentheory/compilation/ag32/proofs           1m35s   5GB
Oct 04 00:07:29 Starting examples/sat_encodings
Oct 04 00:09:18 Finished examples/sat_encodings                                1m48s 965MB
Oct 04 00:09:18 Starting examples/sat_encodings/case_studies
Oct 04 00:10:50 Finished examples/sat_encodings/case_studies                   1m32s 786MB
Oct 04 00:10:51 Starting examples/sat_encodings/translation
Oct 04 00:16:30 Finished examples/sat_encodings/translation                    5m39s   5GB
Oct 04 00:16:31 Starting examples/sat_encodings/translation/compilation
Oct 04 01:04:56 Finished examples/sat_encodings/translation/compilation       48m25s  18GB
Oct 04 01:04:56 Starting translator/okasaki-examples
Oct 04 01:09:25 Finished translator/okasaki-examples                           4m27s   1GB
Oct 04 01:09:26 Starting translator/other-examples
Oct 04 01:11:27 Finished translator/other-examples                             2m00s   1GB
Oct 04 01:11:27 Starting compiler/parsing/tests
Oct 04 01:11:56 Finished compiler/parsing/tests                                  29s 627MB
Oct 04 01:11:56 Starting compiler/inference/tests
Oct 04 01:20:03 Finished compiler/inference/tests                              8m07s   3GB
Oct 04 01:20:03 Starting compiler/bootstrap/translation
Oct 04 03:51:23 Finished compiler/bootstrap/translation                     2h31m16s  29GB
Oct 04 03:51:23 Starting unverified/sexpr-bootstrap/x64/64
Oct 04 04:03:41 Finished unverified/sexpr-bootstrap/x64/64                    12m16s   8GB
Oct 04 04:03:41 Starting unverified/sexpr-bootstrap/x64/32
Oct 04 04:14:16 Finished unverified/sexpr-bootstrap/x64/32                    10m34s   8GB
Oct 04 04:14:16 Starting compiler/benchmarks
Oct 04 04:14:18 Finished compiler/benchmarks                                      2s  35MB
Oct 04 04:14:18 Starting compiler/bootstrap/compilation/x64/64
Oct 04 16:34:45 Finished compiler/bootstrap/compilation/x64/64             12h20m25s  64GB
Oct 04 16:34:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 04 16:37:57 Finished compiler/bootstrap/compilation/x64/64/proofs          3m11s  13GB
Oct 04 16:37:57 Starting compiler/bootstrap/compilation/x64/32
Oct 05 03:41:38 Finished compiler/bootstrap/compilation/x64/32             11h03m39s  64GB
Oct 05 03:41:38 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 05 03:44:32 Finished compiler/bootstrap/compilation/x64/32/proofs          2m53s  11GB
Oct 05 03:44:32 Starting compiler/bootstrap/compilation/ag32/32
Oct 05 14:57:50 FAILED: compiler/bootstrap/compilation/ag32/32
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$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Starting work on README.md
Starting work on to_dataBootstrapTheory
README.md                                                                                                                                                                       (0s)     OK
to_dataBootstrapTheory                                                                                                                                                         (68m)     OK
Starting work on to_lab_ag32BootstrapTheory
to_lab_ag32BootstrapTheory                                                                                                                                                    (848m)     OK
Starting work on ag32BootstrapTheory
ag32BootstrapTheory                                                                                                                                                           (205m)FAIL<Signal 9>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL warning: Type.mk_vartype: non-standard syntax>>
 <<HOL message: Created theory "ag32Bootstrap">>
           lab_to_target eval: runtime: 3h17m31s,    gctime: 48m05s,     systime: 1m07s.
           lab_to_target real: 3h18m36s
           lab_to_target size: 118853916