Job 1146

CakeML:6fcd4caed1429ae9e0c79b82f12a588023670be4
  Update build-sequence [Jan 14 11:47:53]
#718 (lpr)
Merging into:6f499a68f2500e7f937b3254c9da6f93a9b62670
  Merge pull request #716 from CakeML/stack-opt-2 [Jan 09 03:33:21]
HOL:29f6ddb65bb5d84c26f87faa6eeae514e3413406
  Fix HOLsexp selftest given change to API (fromList -> List) [Jan 13 07:30:16]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 14 11:49:14 Claimed job
Jan 14 11:49:21 Building HOL
Jan 14 11:59:00 Starting developers
Jan 14 11:59:01 Finished developers                                               0s  21MB
Jan 14 11:59:01 Starting developers/bin
Jan 14 11:59:05 Finished developers/bin                                           3s 238MB
Jan 14 11:59:05 Starting semantics/ffi
Jan 14 11:59:13 Finished semantics/ffi                                            7s 228MB
Jan 14 11:59:13 Starting semantics
Jan 14 12:00:39 Finished semantics                                             1m25s   1GB
Jan 14 12:00:39 Starting semantics/proofs
Jan 14 12:03:50 Finished semantics/proofs                                      3m10s   1GB
Jan 14 12:03:50 Starting semantics/alt_semantics
Jan 14 12:03:57 Finished semantics/alt_semantics                                  6s 276MB
Jan 14 12:03:57 Starting semantics/alt_semantics/proofs
Jan 14 12:05:59 Finished semantics/alt_semantics/proofs                        2m01s 797MB
Jan 14 12:05:59 Starting basis/pure
Jan 14 12:08:51 Finished basis/pure                                            2m51s 810MB
Jan 14 12:08:51 Starting translator
Jan 14 12:11:22 Finished translator                                            2m30s   1GB
Jan 14 12:11:23 Starting compiler/parsing
Jan 14 12:12:29 Finished compiler/parsing                                      1m06s   2GB
Jan 14 12:12:29 Starting characteristic
Jan 14 12:18:02 Finished characteristic                                        5m31s   1GB
Jan 14 12:18:02 Starting translator/monadic
Jan 14 12:19:30 Finished translator/monadic                                    1m28s   1GB
Jan 14 12:19:31 Starting basis
Jan 14 12:52:28 Finished basis                                                32m56s  28GB
Jan 14 12:52:28 Starting compiler/inference
Jan 14 12:54:35 Finished compiler/inference                                    2m06s   2GB
Jan 14 12:54:35 Starting compiler/backend/reg_alloc
Jan 14 12:55:35 Finished compiler/backend/reg_alloc                              58s   1GB
Jan 14 12:55:35 Starting compiler/backend/gc
Jan 14 12:58:51 Finished compiler/backend/gc                                   3m15s   2GB
Jan 14 12:58:51 Starting compiler/backend
Jan 14 13:03:21 Finished compiler/backend                                      4m29s   3GB
Jan 14 13:03:21 Starting compiler/encoders/asm
Jan 14 13:03:42 Finished compiler/encoders/asm                                   20s 821MB
Jan 14 13:03:42 Starting compiler/encoders/x64
Jan 14 13:04:35 Finished compiler/encoders/x64                                   52s 912MB
Jan 14 13:04:35 Starting compiler/encoders/arm7
Jan 14 13:06:14 Finished compiler/encoders/arm7                                1m39s   1GB
Jan 14 13:06:15 Starting compiler/encoders/arm8
Jan 14 13:06:44 Finished compiler/encoders/arm8                                  29s 880MB
Jan 14 13:06:45 Starting compiler/encoders/mips
Jan 14 13:07:50 Finished compiler/encoders/mips                                1m05s 778MB
Jan 14 13:07:50 Starting compiler/encoders/riscv
Jan 14 13:09:09 Finished compiler/encoders/riscv                               1m18s   1GB
Jan 14 13:09:09 Starting compiler/encoders/ag32
Jan 14 13:09:25 Finished compiler/encoders/ag32                                  15s 793MB
Jan 14 13:09:25 Starting compiler/backend/x64
Jan 14 13:09:42 Finished compiler/backend/x64                                    16s   1GB
Jan 14 13:09:42 Starting compiler/backend/arm7
Jan 14 13:10:01 Finished compiler/backend/arm7                                   18s   1GB
Jan 14 13:10:01 Starting compiler/backend/arm8
Jan 14 13:10:18 Finished compiler/backend/arm8                                   16s   1GB
Jan 14 13:10:19 Starting compiler/backend/mips
Jan 14 13:10:37 Finished compiler/backend/mips                                   17s   1GB
Jan 14 13:10:37 Starting compiler/backend/riscv
Jan 14 13:10:55 Finished compiler/backend/riscv                                  17s   1GB
Jan 14 13:10:56 Starting compiler/backend/ag32
Jan 14 13:12:03 Finished compiler/backend/ag32                                 1m07s   1GB
Jan 14 13:12:03 Starting compiler/parsing/proofs
Jan 14 13:17:35 Finished compiler/parsing/proofs                               5m31s 913MB
Jan 14 13:17:35 Starting compiler/inference/proofs
Jan 14 13:20:23 Finished compiler/inference/proofs                             2m47s   1GB
Jan 14 13:20:23 Starting compiler/backend/semantics
Jan 14 13:47:17 Finished compiler/backend/semantics                           26m53s   2GB
Jan 14 13:47:18 Starting compiler/backend/reg_alloc/proofs
Jan 14 13:50:33 Finished compiler/backend/reg_alloc/proofs                     3m14s 823MB
Jan 14 13:50:33 Starting compiler/backend/proofs
Jan 14 14:50:38 Finished compiler/backend/proofs                            1h00m04s  17GB
Jan 14 14:50:38 Starting compiler/encoders/x64/proofs
Jan 14 14:59:59 Finished compiler/encoders/x64/proofs                          9m20s   4GB
Jan 14 14:59:59 Starting compiler/encoders/arm7/proofs
Jan 14 15:12:25 Finished compiler/encoders/arm7/proofs                        12m25s   3GB
Jan 14 15:12:25 Starting compiler/encoders/arm8/proofs
Jan 14 15:18:48 Finished compiler/encoders/arm8/proofs                         6m22s   1GB
Jan 14 15:18:48 Starting compiler/encoders/mips/proofs
Jan 14 15:28:24 Finished compiler/encoders/mips/proofs                         9m36s   2GB
Jan 14 15:28:25 Starting compiler/encoders/riscv/proofs
Jan 14 15:36:48 Finished compiler/encoders/riscv/proofs                        8m22s   1GB
Jan 14 15:36:48 Starting compiler/encoders/ag32/proofs
Jan 14 15:39:13 Finished compiler/encoders/ag32/proofs                         2m24s 859MB
Jan 14 15:39:13 Starting compiler/backend/x64/proofs
Jan 14 15:39:31 Finished compiler/backend/x64/proofs                             17s   1GB
Jan 14 15:39:31 Starting compiler/backend/arm7/proofs
Jan 14 15:39:52 Finished compiler/backend/arm7/proofs                            20s 856MB
Jan 14 15:39:52 Starting compiler/backend/arm8/proofs
Jan 14 15:40:10 Finished compiler/backend/arm8/proofs                            17s   1GB
Jan 14 15:40:10 Starting compiler/backend/mips/proofs
Jan 14 15:40:28 Finished compiler/backend/mips/proofs                            17s   1GB
Jan 14 15:40:28 Starting compiler/backend/riscv/proofs
Jan 14 15:40:46 Finished compiler/backend/riscv/proofs                           17s   1GB
Jan 14 15:40:47 Starting compiler/backend/ag32/proofs
Jan 14 15:49:51 Finished compiler/backend/ag32/proofs                          9m04s   2GB
Jan 14 15:49:52 Starting compiler/proofs
Jan 14 15:51:30 Finished compiler/proofs                                       1m38s   3GB
Jan 14 15:51:30 Starting candle/set-theory
Jan 14 15:51:57 Finished candle/set-theory                                       26s 841MB
Jan 14 15:51:58 Starting candle/syntax-lib
Jan 14 15:52:07 Finished candle/syntax-lib                                        9s 652MB
Jan 14 15:52:07 Starting candle/standard/syntax
Jan 14 15:53:50 Finished candle/standard/syntax                                1m42s   1GB
Jan 14 15:53:50 Starting candle/standard/semantics
Jan 14 15:55:26 Finished candle/standard/semantics                             1m35s   1GB
Jan 14 15:55:27 Starting candle/standard/monadic
Jan 14 15:57:00 Finished candle/standard/monadic                               1m33s   1GB
Jan 14 15:57:01 Starting candle/standard/ml_kernel
Jan 14 16:01:59 Finished candle/standard/ml_kernel                             4m57s   5GB
Jan 14 16:02:00 Starting candle/standard/opentheory
Jan 14 16:11:20 Finished candle/standard/opentheory                            9m18s   4GB
Jan 14 16:11:20 Starting candle/standard/opentheory/compilation
Jan 14 16:44:24 Finished candle/standard/opentheory/compilation               33m03s  16GB
Jan 14 16:44:24 Starting candle/standard/opentheory/compilation/proofs
Jan 14 16:45:01 Finished candle/standard/opentheory/compilation/proofs           36s   3GB
Jan 14 16:45:02 Starting characteristic/examples
Jan 14 16:46:35 Finished characteristic/examples                               1m32s   1GB
Jan 14 16:46:35 Starting tutorial/solutions
Jan 14 17:00:35 Finished tutorial/solutions                                   13m59s   6GB
Jan 14 17:00:35 Starting translator/monadic/examples
Jan 14 17:03:35 Finished translator/monadic/examples                           2m59s   3GB
Jan 14 17:03:36 Starting examples
Jan 14 17:13:03 Finished examples                                              9m26s   3GB
Jan 14 17:13:03 Starting examples/compilation/x64
Jan 14 19:25:49 Finished examples/compilation/x64                           2h12m45s  12GB
Jan 14 19:25:49 Starting examples/compilation/x64/proofs
Jan 14 19:27:46 Finished examples/compilation/x64/proofs                       1m56s   2GB
Jan 14 19:27:46 Starting examples/compilation/ag32
Jan 14 19:58:35 Finished examples/compilation/ag32                            30m47s   5GB
Jan 14 19:58:35 Starting examples/compilation/ag32/proofs
Jan 14 19:59:28 Finished examples/compilation/ag32/proofs                        52s   2GB
Jan 14 19:59:28 Starting examples/cost
Jan 14 20:27:12 Finished examples/cost                                        27m43s   7GB
Jan 14 20:27:13 Starting examples/lpr_checker
Jan 14 20:30:47 Finished examples/lpr_checker                                  3m34s   3GB
Jan 14 20:30:48 Starting examples/lpr_checker/compilation
Jan 14 20:48:06 Finished examples/lpr_checker/compilation                     17m17s   8GB
Jan 14 20:48:06 Starting examples/lpr_checker/compilation/proofs
Jan 14 20:48:52 Finished examples/lpr_checker/compilation/proofs                 44s   2GB
Jan 14 20:48:52 Starting examples/lpr_checker/array
Jan 14 20:58:07 Finished examples/lpr_checker/array                            9m15s   3GB
Jan 14 20:58:07 Starting examples/lpr_checker/array/compilation
Jan 14 21:13:30 Finished examples/lpr_checker/array/compilation               15m22s   9GB
Jan 14 21:13:30 Starting examples/lpr_checker/array/compilation/proofs
Jan 14 21:14:20 Finished examples/lpr_checker/array/compilation/proofs           49s   2GB
Jan 14 21:14:21 Starting translator/okasaki-examples
Jan 14 21:18:37 Finished translator/okasaki-examples                           4m16s   1GB
Jan 14 21:18:37 Starting translator/other-examples
Jan 14 21:20:24 Finished translator/other-examples                             1m46s   1GB
Jan 14 21:20:24 Starting compiler/parsing/tests
Jan 14 21:20:49 Finished compiler/parsing/tests                                  24s 505MB
Jan 14 21:20:49 Starting compiler/inference/tests
Jan 14 21:25:19 Finished compiler/inference/tests                              4m29s   6GB
Jan 14 21:25:19 Starting compiler/bootstrap/translation
Jan 15 01:05:12 Finished compiler/bootstrap/translation                     3h39m52s  44GB
Jan 15 01:05:13 Starting unverified/sexpr-bootstrap/x64/64
Jan 15 01:08:27 FAILED: unverified/sexpr-bootstrap/x64/64
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[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/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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[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/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[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/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/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
Scanning [1m$(CAKEMLDIR)/developers/bin[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Starting work on cake-sexpr-x64-64
cake-sexpr-x64-64                                                             real:  128s  user:  124s     OK
Starting work on cake.S
cake.S                                                                        real:   61s  user:   61sFAIL<1>