Job 1283

CakeML:dfd2c9125161aefeefc13a87a248474c55bfc5a2
  Shorten a misc proof [Jun 21 19:04:21]
#738 (export_update)
Merging into:6f71ec748c056d9a784b0d01d2b96d77b6e006ca
  Fix some scripts in response to changes in HOL [Jun 18 15:12:28]
HOL:3ff35dffbddfa8da7a80738e9d3f3c67d7b0cf5f
  Fix Unicode violation in src/ [Jun 20 06:25:34]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 22 04:36:45 Claimed job
Jun 22 04:36:52 Building HOL
Jun 22 04:49:04 Starting developers
Jun 22 04:49:05 Finished developers                                               0s  29MB
Jun 22 04:49:05 Starting developers/bin
Jun 22 04:49:13 Finished developers/bin                                           7s   1GB
Jun 22 04:49:13 Starting semantics/ffi
Jun 22 04:49:22 Finished semantics/ffi                                            8s 254MB
Jun 22 04:49:22 Starting semantics
Jun 22 04:50:50 Finished semantics                                             1m27s   1GB
Jun 22 04:50:50 Starting semantics/proofs
Jun 22 04:54:05 Finished semantics/proofs                                      3m15s   1GB
Jun 22 04:54:06 Starting semantics/alt_semantics
Jun 22 04:54:14 Finished semantics/alt_semantics                                  7s 334MB
Jun 22 04:54:14 Starting semantics/alt_semantics/proofs
Jun 22 04:56:18 Finished semantics/alt_semantics/proofs                        2m03s 934MB
Jun 22 04:56:18 Starting basis/pure
Jun 22 04:59:09 Finished basis/pure                                            2m51s 948MB
Jun 22 04:59:10 Starting translator
Jun 22 05:01:44 Finished translator                                            2m34s   1GB
Jun 22 05:01:44 Starting compiler/parsing
Jun 22 05:02:53 Finished compiler/parsing                                      1m08s   2GB
Jun 22 05:02:53 Starting characteristic
Jun 22 05:08:40 Finished characteristic                                        5m47s   2GB
Jun 22 05:08:41 Starting translator/monadic
Jun 22 05:10:16 Finished translator/monadic                                    1m35s   1GB
Jun 22 05:10:16 Starting basis
Jun 22 05:41:32 Finished basis                                                31m15s  17GB
Jun 22 05:41:32 Starting compiler/inference
Jun 22 05:42:37 Finished compiler/inference                                    1m04s 935MB
Jun 22 05:42:37 Starting compiler/backend/reg_alloc
Jun 22 05:43:41 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jun 22 05:43:41 Starting compiler/backend/gc
Jun 22 05:47:03 Finished compiler/backend/gc                                   3m22s   2GB
Jun 22 05:47:04 Starting compiler/backend
Jun 22 05:51:40 Finished compiler/backend                                      4m36s   3GB
Jun 22 05:51:40 Starting compiler/encoders/asm
Jun 22 05:52:02 Finished compiler/encoders/asm                                   21s 719MB
Jun 22 05:52:02 Starting compiler/encoders/x64
Jun 22 05:52:59 Finished compiler/encoders/x64                                   56s 715MB
Jun 22 05:52:59 Starting compiler/encoders/arm7
Jun 22 05:54:47 Finished compiler/encoders/arm7                                1m47s   1GB
Jun 22 05:54:47 Starting compiler/encoders/arm8
Jun 22 05:55:21 Finished compiler/encoders/arm8                                  33s 932MB
Jun 22 05:55:21 Starting compiler/encoders/mips
Jun 22 05:56:36 Finished compiler/encoders/mips                                1m14s   1GB
Jun 22 05:56:36 Starting compiler/encoders/riscv
Jun 22 05:58:03 Finished compiler/encoders/riscv                               1m26s   1GB
Jun 22 05:58:03 Starting compiler/encoders/ag32
Jun 22 05:58:20 Finished compiler/encoders/ag32                                  16s 887MB
Jun 22 05:58:20 Starting compiler/backend/x64
Jun 22 05:58:36 Finished compiler/backend/x64                                    16s 873MB
Jun 22 05:58:36 Starting compiler/backend/arm7
Jun 22 05:58:56 Finished compiler/backend/arm7                                   19s   1GB
Jun 22 05:58:56 Starting compiler/backend/arm8
Jun 22 05:59:15 Finished compiler/backend/arm8                                   18s   1GB
Jun 22 05:59:15 Starting compiler/backend/mips
Jun 22 05:59:34 Finished compiler/backend/mips                                   19s   1GB
Jun 22 05:59:35 Starting compiler/backend/riscv
Jun 22 05:59:54 Finished compiler/backend/riscv                                  18s   1GB
Jun 22 05:59:54 Starting compiler/backend/ag32
Jun 22 06:01:02 Finished compiler/backend/ag32                                 1m08s   1GB
Jun 22 06:01:02 Starting compiler/parsing/proofs
Jun 22 06:06:39 Finished compiler/parsing/proofs                               5m36s   1GB
Jun 22 06:06:40 Starting compiler/inference/proofs
Jun 22 06:09:01 Finished compiler/inference/proofs                             2m21s   1GB
Jun 22 06:09:01 Starting compiler/backend/semantics
Jun 22 06:36:15 Finished compiler/backend/semantics                           27m13s   3GB
Jun 22 06:36:15 Starting compiler/backend/reg_alloc/proofs
Jun 22 06:39:34 Finished compiler/backend/reg_alloc/proofs                     3m19s 965MB
Jun 22 06:39:35 Starting compiler/backend/proofs
Jun 22 07:32:28 Finished compiler/backend/proofs                              52m53s  17GB
Jun 22 07:32:28 Starting compiler/encoders/x64/proofs
Jun 22 07:41:50 Finished compiler/encoders/x64/proofs                          9m21s   4GB
Jun 22 07:41:50 Starting compiler/encoders/arm7/proofs
Jun 22 07:54:21 Finished compiler/encoders/arm7/proofs                        12m30s   3GB
Jun 22 07:54:21 Starting compiler/encoders/arm8/proofs
Jun 22 08:00:42 Finished compiler/encoders/arm8/proofs                         6m21s   1GB
Jun 22 08:00:43 Starting compiler/encoders/mips/proofs
Jun 22 08:10:12 Finished compiler/encoders/mips/proofs                         9m28s   3GB
Jun 22 08:10:12 Starting compiler/encoders/riscv/proofs
Jun 22 08:18:48 Finished compiler/encoders/riscv/proofs                        8m35s   1GB
Jun 22 08:18:48 Starting compiler/encoders/ag32/proofs
Jun 22 08:21:12 Finished compiler/encoders/ag32/proofs                         2m24s 814MB
Jun 22 08:21:13 Starting compiler/backend/x64/proofs
Jun 22 08:21:32 Finished compiler/backend/x64/proofs                             19s   1GB
Jun 22 08:21:32 Starting compiler/backend/arm7/proofs
Jun 22 08:21:54 Finished compiler/backend/arm7/proofs                            21s 892MB
Jun 22 08:21:54 Starting compiler/backend/arm8/proofs
Jun 22 08:22:14 Finished compiler/backend/arm8/proofs                            19s   1GB
Jun 22 08:22:14 Starting compiler/backend/mips/proofs
Jun 22 08:22:33 Finished compiler/backend/mips/proofs                            19s   1GB
Jun 22 08:22:34 Starting compiler/backend/riscv/proofs
Jun 22 08:22:53 Finished compiler/backend/riscv/proofs                           19s   1GB
Jun 22 08:22:53 Starting compiler/backend/ag32/proofs
Jun 22 08:35:16 Finished compiler/backend/ag32/proofs                         12m22s   2GB
Jun 22 08:35:17 Starting compiler/proofs
Jun 22 08:36:58 Finished compiler/proofs                                       1m41s   2GB
Jun 22 08:36:58 Starting candle/set-theory
Jun 22 08:37:26 Finished candle/set-theory                                       27s 744MB
Jun 22 08:37:27 Starting candle/syntax-lib
Jun 22 08:37:37 Finished candle/syntax-lib                                       10s 672MB
Jun 22 08:37:37 Starting candle/standard/syntax
Jun 22 08:39:24 Finished candle/standard/syntax                                1m47s 972MB
Jun 22 08:39:24 Starting candle/standard/semantics
Jun 22 08:41:04 Finished candle/standard/semantics                             1m39s   1GB
Jun 22 08:41:04 Starting candle/standard/monadic
Jun 22 08:42:41 Finished candle/standard/monadic                               1m36s   1GB
Jun 22 08:42:41 Starting candle/standard/ml_kernel
Jun 22 08:47:58 Finished candle/standard/ml_kernel                             5m16s   3GB
Jun 22 08:47:58 Starting candle/standard/opentheory
Jun 22 08:57:02 Finished candle/standard/opentheory                            9m03s   6GB
Jun 22 08:57:02 Starting candle/standard/opentheory/compilation
Jun 22 09:28:26 Finished candle/standard/opentheory/compilation               31m24s  20GB
Jun 22 09:28:27 Starting candle/standard/opentheory/compilation/proofs
Jun 22 09:29:05 Finished candle/standard/opentheory/compilation/proofs           38s   3GB
Jun 22 09:29:05 Starting candle/overloading/syntax
Jun 22 09:32:03 Finished candle/overloading/syntax                             2m58s   1GB
Jun 22 09:32:04 Starting candle/overloading/semantics
Jun 22 09:38:51 Finished candle/overloading/semantics                          6m46s   2GB
Jun 22 09:38:51 Starting characteristic/examples
Jun 22 09:40:09 Finished characteristic/examples                               1m17s   3GB
Jun 22 09:40:09 Starting tutorial/solutions
Jun 22 09:54:47 Finished tutorial/solutions                                   14m38s   6GB
Jun 22 09:54:47 Starting translator/monadic/examples
Jun 22 09:57:57 Finished translator/monadic/examples                           3m09s   2GB
Jun 22 09:57:57 Starting examples
Jun 22 10:06:13 Finished examples                                              8m15s   3GB
Jun 22 10:06:13 Starting examples/compilation/x64
Jun 22 12:19:18 Finished examples/compilation/x64                           2h13m04s  18GB
Jun 22 12:19:18 Starting examples/compilation/x64/proofs
Jun 22 12:20:52 Finished examples/compilation/x64/proofs                       1m33s   2GB
Jun 22 12:20:53 Starting examples/compilation/ag32
Jun 22 12:51:21 Finished examples/compilation/ag32                            30m28s   6GB
Jun 22 12:51:21 Starting examples/compilation/ag32/proofs
Jun 22 12:52:02 Finished examples/compilation/ag32/proofs                        40s   3GB
Jun 22 12:52:03 Starting examples/cost
Jun 22 13:37:52 Finished examples/cost                                        45m48s   8GB
Jun 22 13:37:52 Starting examples/lpr_checker
Jun 22 13:41:40 Finished examples/lpr_checker                                  3m47s   3GB
Jun 22 13:41:40 Starting examples/lpr_checker/compilation
Jun 22 13:59:16 Finished examples/lpr_checker/compilation                     17m35s   8GB
Jun 22 13:59:16 Starting examples/lpr_checker/compilation/proofs
Jun 22 13:59:53 Finished examples/lpr_checker/compilation/proofs                 36s   2GB
Jun 22 13:59:53 Starting examples/lpr_checker/array
Jun 22 14:09:32 Finished examples/lpr_checker/array                            9m39s   2GB
Jun 22 14:09:32 Starting examples/lpr_checker/array/compilation
Jun 22 14:27:35 Finished examples/lpr_checker/array/compilation               18m02s  11GB
Jun 22 14:27:35 Starting examples/lpr_checker/array/compilation/proofs
Jun 22 14:28:19 Finished examples/lpr_checker/array/compilation/proofs           44s   3GB
Jun 22 14:28:19 Starting translator/okasaki-examples
Jun 22 14:32:28 Finished translator/okasaki-examples                           4m08s   2GB
Jun 22 14:32:28 Starting translator/other-examples
Jun 22 14:34:26 Finished translator/other-examples                             1m57s   1GB
Jun 22 14:34:26 Starting compiler/parsing/tests
Jun 22 14:34:50 Finished compiler/parsing/tests                                  24s 606MB
Jun 22 14:34:50 Starting compiler/inference/tests
Jun 22 14:39:16 Finished compiler/inference/tests                              4m24s   5GB
Jun 22 14:39:16 Starting compiler/bootstrap/translation
Jun 22 17:13:43 Finished compiler/bootstrap/translation                     2h34m27s  43GB
Jun 22 17:13:44 Starting unverified/sexpr-bootstrap/x64/64
Jun 22 17:16:04 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/pattern_matching[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:  105s  user:   97s     OK
Starting work on cake.S
cake.S                                                                        real:   32s  user:   32sFAIL<1>
 CakeML heap space exhausted.