Job 1364

CakeML:9a0180ee6a0bbcf4cc2d2aee6efc20caa0f62e95
  Add sexpr files to cake-x64-64.tar.gz artefact [Sep 24 05:41:42]
#788 (symbols)
Merging into:411c80da717a8e99b5a8e7f6519e95637ecb7225
  Merge pull request #752 from sorear/rv_fixes [Sep 24 08:22:45]
HOL:841cced433cd0e9e4913c6e9c05c9b7542e38a6b
  Handle change to Slavonic asterisk (25dec53e17) in Manual production [Sep 23 11:12:05]
Machine:oven5s2 5.7.19 x86_64 GNU/Linux

Sep 25 16:23:53 Claimed job
Sep 25 16:23:55 Reusing HOL
Sep 25 16:24:05 Starting developers
Sep 25 16:24:07 Finished developers                                               1s 153MB
Sep 25 16:24:07 Starting developers/bin
Sep 25 16:24:16 Finished developers/bin                                           8s   1GB
Sep 25 16:24:16 Starting semantics/ffi
Sep 25 16:24:26 Finished semantics/ffi                                            9s   2GB
Sep 25 16:24:26 Starting semantics
Sep 25 16:25:35 Finished semantics                                             1m08s   4GB
Sep 25 16:25:36 Starting semantics/proofs
Sep 25 16:28:31 Finished semantics/proofs                                      2m55s   4GB
Sep 25 16:28:32 Starting semantics/alt_semantics
Sep 25 16:28:40 Finished semantics/alt_semantics                                  8s   4GB
Sep 25 16:28:40 Starting semantics/alt_semantics/proofs
Sep 25 16:30:39 Finished semantics/alt_semantics/proofs                        1m58s   4GB
Sep 25 16:30:39 Starting basis/pure
Sep 25 16:31:24 Finished basis/pure                                              44s   4GB
Sep 25 16:31:24 Starting translator
Sep 25 16:33:50 Finished translator                                            2m25s   7GB
Sep 25 16:33:50 Starting compiler/parsing
Sep 25 16:34:51 Finished compiler/parsing                                      1m00s   4GB
Sep 25 16:34:51 Starting characteristic
Sep 25 16:40:23 Finished characteristic                                        5m30s   5GB
Sep 25 16:40:23 Starting translator/monadic
Sep 25 16:41:50 Finished translator/monadic                                    1m26s   4GB
Sep 25 16:41:50 Starting basis
Sep 25 17:13:43 Finished basis                                                31m52s  50GB
Sep 25 17:13:43 Starting compiler/inference
Sep 25 17:14:38 Finished compiler/inference                                      54s   4GB
Sep 25 17:14:38 Starting compiler/backend/reg_alloc
Sep 25 17:15:27 Finished compiler/backend/reg_alloc                              48s   4GB
Sep 25 17:15:28 Starting compiler/backend/gc
Sep 25 17:18:13 Finished compiler/backend/gc                                   2m44s   6GB
Sep 25 17:18:14 Starting compiler/backend
Sep 25 17:22:25 Finished compiler/backend                                      4m10s   7GB
Sep 25 17:22:25 Starting compiler/encoders/asm
Sep 25 17:22:45 Finished compiler/encoders/asm                                   19s   4GB
Sep 25 17:22:46 Starting compiler/encoders/x64
Sep 25 17:23:08 Finished compiler/encoders/x64                                   22s   4GB
Sep 25 17:23:09 Starting compiler/encoders/arm7
Sep 25 17:23:57 Finished compiler/encoders/arm7                                  47s   4GB
Sep 25 17:23:57 Starting compiler/encoders/arm8
Sep 25 17:24:10 Finished compiler/encoders/arm8                                  11s   4GB
Sep 25 17:24:10 Starting compiler/encoders/mips
Sep 25 17:24:27 Finished compiler/encoders/mips                                  16s   4GB
Sep 25 17:24:27 Starting compiler/encoders/riscv
Sep 25 17:24:42 Finished compiler/encoders/riscv                                 14s   4GB
Sep 25 17:24:42 Starting compiler/encoders/ag32
Sep 25 17:24:59 Finished compiler/encoders/ag32                                  15s   4GB
Sep 25 17:24:59 Starting compiler/backend/x64
Sep 25 17:25:17 Finished compiler/backend/x64                                    17s   4GB
Sep 25 17:25:17 Starting compiler/backend/arm7
Sep 25 17:25:33 Finished compiler/backend/arm7                                   15s   4GB
Sep 25 17:25:34 Starting compiler/backend/arm8
Sep 25 17:25:52 Finished compiler/backend/arm8                                   17s   4GB
Sep 25 17:25:52 Starting compiler/backend/mips
Sep 25 17:26:11 Finished compiler/backend/mips                                   18s   4GB
Sep 25 17:26:11 Starting compiler/backend/riscv
Sep 25 17:26:30 Finished compiler/backend/riscv                                  18s   4GB
Sep 25 17:26:30 Starting compiler/backend/ag32
Sep 25 17:27:32 Finished compiler/backend/ag32                                 1m01s   4GB
Sep 25 17:27:33 Starting compiler/parsing/proofs
Sep 25 17:32:16 Finished compiler/parsing/proofs                               4m43s   4GB
Sep 25 17:32:17 Starting compiler/inference/proofs
Sep 25 17:34:29 Finished compiler/inference/proofs                             2m12s   4GB
Sep 25 17:34:30 Starting compiler/backend/semantics
Sep 25 18:01:00 Finished compiler/backend/semantics                           26m29s   8GB
Sep 25 18:01:00 Starting compiler/backend/reg_alloc/proofs
Sep 25 18:04:02 Finished compiler/backend/reg_alloc/proofs                     3m01s   4GB
Sep 25 18:04:02 Starting compiler/backend/proofs
Sep 25 18:49:55 Finished compiler/backend/proofs                              45m52s  22GB
Sep 25 18:49:56 Starting compiler/encoders/x64/proofs
Sep 25 18:59:22 Finished compiler/encoders/x64/proofs                          9m25s  10GB
Sep 25 18:59:22 Starting compiler/encoders/arm7/proofs
Sep 25 19:12:26 Finished compiler/encoders/arm7/proofs                        13m03s  10GB
Sep 25 19:12:28 Starting compiler/encoders/arm8/proofs
Sep 25 19:18:56 Finished compiler/encoders/arm8/proofs                         6m27s   5GB
Sep 25 19:18:56 Starting compiler/encoders/mips/proofs
Sep 25 19:29:21 Finished compiler/encoders/mips/proofs                        10m23s   7GB
Sep 25 19:29:21 Starting compiler/encoders/riscv/proofs
Sep 25 19:37:31 Finished compiler/encoders/riscv/proofs                        8m09s   8GB
Sep 25 19:37:32 Starting compiler/encoders/ag32/proofs
Sep 25 19:39:44 Finished compiler/encoders/ag32/proofs                         2m12s   4GB
Sep 25 19:39:45 Starting compiler/backend/x64/proofs
Sep 25 19:40:05 Finished compiler/backend/x64/proofs                             20s   4GB
Sep 25 19:40:06 Starting compiler/backend/arm7/proofs
Sep 25 19:40:28 Finished compiler/backend/arm7/proofs                            21s   4GB
Sep 25 19:40:28 Starting compiler/backend/arm8/proofs
Sep 25 19:40:48 Finished compiler/backend/arm8/proofs                            19s   4GB
Sep 25 19:40:48 Starting compiler/backend/mips/proofs
Sep 25 19:41:09 Finished compiler/backend/mips/proofs                            20s   4GB
Sep 25 19:41:10 Starting compiler/backend/riscv/proofs
Sep 25 19:41:31 Finished compiler/backend/riscv/proofs                           20s   4GB
Sep 25 19:41:31 Starting compiler/backend/ag32/proofs
Sep 25 19:53:03 Finished compiler/backend/ag32/proofs                         11m31s  11GB
Sep 25 19:53:03 Starting compiler/proofs
Sep 25 19:54:35 Finished compiler/proofs                                       1m31s   7GB
Sep 25 19:54:35 Starting candle/set-theory
Sep 25 19:54:59 Finished candle/set-theory                                       23s   4GB
Sep 25 19:55:00 Starting candle/syntax-lib
Sep 25 19:55:10 Finished candle/syntax-lib                                        9s   4GB
Sep 25 19:55:10 Starting candle/standard/syntax
Sep 25 19:56:45 Finished candle/standard/syntax                                1m34s   4GB
Sep 25 19:56:45 Starting candle/standard/semantics
Sep 25 19:58:23 Finished candle/standard/semantics                             1m37s   5GB
Sep 25 19:58:24 Starting candle/standard/monadic
Sep 25 19:59:53 Finished candle/standard/monadic                               1m29s   4GB
Sep 25 19:59:54 Starting candle/standard/ml_kernel
Sep 25 20:04:45 Finished candle/standard/ml_kernel                             4m50s  10GB
Sep 25 20:04:46 Starting candle/overloading/syntax
Sep 25 20:07:25 Finished candle/overloading/syntax                             2m38s   4GB
Sep 25 20:07:25 Starting candle/overloading/semantics
Sep 25 20:18:45 Finished candle/overloading/semantics                         11m19s   6GB
Sep 25 20:18:46 Starting characteristic/examples
Sep 25 20:19:59 Finished characteristic/examples                               1m12s  10GB
Sep 25 20:19:59 Starting tutorial/solutions
Sep 25 20:33:09 Finished tutorial/solutions                                   13m09s  20GB
Sep 25 20:33:09 Starting translator/monadic/examples
Sep 25 20:35:46 Finished translator/monadic/examples                           2m36s   9GB
Sep 25 20:35:47 Starting examples
Sep 25 20:42:35 Finished examples                                              6m43s  11GB
Sep 25 20:42:39 Starting examples/compilation/x64
Sep 25 22:44:42 Finished examples/compilation/x64                           2h02m02s  66GB
Sep 25 22:44:42 Starting examples/compilation/x64/proofs
Sep 25 22:46:15 Finished examples/compilation/x64/proofs                       1m31s   5GB
Sep 25 22:46:15 Starting examples/compilation/ag32
Sep 25 23:15:10 Finished examples/compilation/ag32                            28m53s  12GB
Sep 25 23:15:10 Starting examples/compilation/ag32/proofs
Sep 25 23:15:52 Finished examples/compilation/ag32/proofs                        41s   6GB
Sep 25 23:15:52 Starting examples/cost
Sep 25 23:56:38 Finished examples/cost                                        40m45s  17GB
Sep 25 23:56:39 Starting examples/lpr_checker
Sep 26 00:00:11 Finished examples/lpr_checker                                  3m31s  11GB
Sep 26 00:00:12 Starting examples/lpr_checker/compilation
Sep 26 00:14:51 Finished examples/lpr_checker/compilation                     14m39s  20GB
Sep 26 00:14:51 Starting examples/lpr_checker/compilation/proofs
Sep 26 00:15:29 Finished examples/lpr_checker/compilation/proofs                 36s   5GB
Sep 26 00:15:29 Starting examples/lpr_checker/array
Sep 26 00:32:45 Finished examples/lpr_checker/array                           17m15s  10GB
Sep 26 00:32:45 Starting examples/lpr_checker/array/compilation
Sep 26 00:55:27 Finished examples/lpr_checker/array/compilation               22m41s  34GB
Sep 26 00:55:27 Starting examples/lpr_checker/array/compilation/proofs
Sep 26 00:56:12 Finished examples/lpr_checker/array/compilation/proofs           44s   6GB
Sep 26 00:56:12 Starting examples/opentheory
Sep 26 01:06:24 Finished examples/opentheory                                  10m11s  11GB
Sep 26 01:06:25 Starting examples/opentheory
Sep 26 01:06:26 Finished examples/opentheory                                      0s  47MB
Sep 26 01:06:26 Starting examples/opentheory/compilation
Sep 26 01:37:28 Finished examples/opentheory/compilation                      31m01s  51GB
Sep 26 01:37:28 Starting examples/opentheory/compilation/proofs
Sep 26 01:38:11 Finished examples/opentheory/compilation/proofs                  37s   5GB
Sep 26 01:38:12 Starting examples/opentheory/compilation/ag32
Sep 26 02:09:08 Finished examples/opentheory/compilation/ag32                 30m55s  48GB
Sep 26 02:09:09 Starting examples/opentheory/compilation/ag32/proofs
Sep 26 02:10:36 Finished examples/opentheory/compilation/ag32/proofs           1m26s  10GB
Sep 26 02:10:36 Starting translator/okasaki-examples
Sep 26 02:14:26 Finished translator/okasaki-examples                           3m49s   7GB
Sep 26 02:14:27 Starting translator/other-examples
Sep 26 02:15:07 Finished translator/other-examples                               40s   5GB
Sep 26 02:15:08 Starting compiler/parsing/tests
Sep 26 02:15:31 Finished compiler/parsing/tests                                  22s   4GB
Sep 26 02:15:31 Starting compiler/inference/tests
Sep 26 02:19:51 Finished compiler/inference/tests                              4m19s   8GB
Sep 26 02:19:51 Starting compiler/bootstrap/translation
Sep 26 04:48:19 Finished compiler/bootstrap/translation                     2h28m26s  83GB
Sep 26 04:48:20 Starting unverified/sexpr-bootstrap/x64/64
Sep 26 04:57:15 Finished unverified/sexpr-bootstrap/x64/64                     8m54s   8GB
Sep 26 04:57:15 Starting unverified/sexpr-bootstrap/x64/32
Sep 26 05:04:39 Finished unverified/sexpr-bootstrap/x64/32                     7m23s   8GB
Sep 26 05:04:40 Starting compiler/benchmarks
Sep 26 05:04:41 Finished compiler/benchmarks                                      0s  55MB
Sep 26 05:04:41 Starting compiler/bootstrap/compilation/x64/64
Sep 26 05:05:37 FAILED: compiler/bootstrap/compilation/x64/64
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/unification/triangular
Scanning $(HOLDIR)/examples/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Starting work on README.md
Starting work on cake-sexpr-32
Starting work on cake-sexpr-64
Starting work on to_dataBootstrapTheory
README.md                                       real:    0s  user:    0s     OK
cake-sexpr-32                                   real:   53s  user:   49sFAIL<1>
 Heap: Resizing from 11.67G to 11.67G.  Estimated ratio 87.86
 GC: Completed with insufficient space
 Heap: Full GC (after) Major heap used 2.13G of 2.14G (99%). Alloc space used 248.73M of 2.85G (9%). Total space 11.67G 20% full.
 Heap: Local spaces 4738, permanent spaces 30, code spaces 73, stack spaces 2
 Heap: Code area: total 572.00K occupied: 230.72K
 Heap: Stack area: total 1.00M
 Uncaught exception: Interrupt
 GC (Total): Non-GC time: CPU user: 24.206 system: 3.121 real: 27.324
 GC (Total): GC time: CPU user: 25.049 system: 1.131 real: 26.181
 Heap: Total CPU GC time 26.180secs,  Non-GC 27.327secs, ratio 0.958
cake-sexpr-64                                                           M-KILLED
to_dataBootstrapTheory                                                  M-KILLED