Job 1366

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 26 05:46:32 Claimed job
Sep 26 05:46:36 Building HOL
Sep 26 05:59:50 Starting developers
Sep 26 05:59:52 Finished developers                                               1s 120MB
Sep 26 05:59:53 Starting developers/bin
Sep 26 06:00:01 Finished developers/bin                                           8s   1GB
Sep 26 06:00:02 Starting semantics/ffi
Sep 26 06:00:14 Finished semantics/ffi                                           11s   4GB
Sep 26 06:00:15 Starting semantics
Sep 26 06:02:18 Finished semantics                                             2m02s   8GB
Sep 26 06:02:18 Starting semantics/proofs
Sep 26 06:08:08 Finished semantics/proofs                                      5m49s   8GB
Sep 26 06:08:08 Starting semantics/alt_semantics
Sep 26 06:08:22 Finished semantics/alt_semantics                                 13s   4GB
Sep 26 06:08:22 Starting semantics/alt_semantics/proofs
Sep 26 06:11:33 Finished semantics/alt_semantics/proofs                        3m10s   8GB
Sep 26 06:11:34 Starting basis/pure
Sep 26 06:15:44 Finished basis/pure                                            4m09s   8GB
Sep 26 06:15:44 Starting translator
Sep 26 06:19:20 Finished translator                                            3m35s   8GB
Sep 26 06:19:21 Starting compiler/parsing
Sep 26 06:20:45 Finished compiler/parsing                                      1m24s   9GB
Sep 26 06:20:46 Starting characteristic
Sep 26 06:26:14 Finished characteristic                                        5m28s   8GB
Sep 26 06:26:15 Starting translator/monadic
Sep 26 06:27:44 Finished translator/monadic                                    1m29s   8GB
Sep 26 06:27:45 Starting basis
Sep 26 06:59:39 Finished basis                                                31m53s  29GB
Sep 26 06:59:39 Starting compiler/inference
Sep 26 07:00:45 Finished compiler/inference                                    1m05s   8GB
Sep 26 07:00:45 Starting compiler/backend/reg_alloc
Sep 26 07:01:37 Finished compiler/backend/reg_alloc                              50s   8GB
Sep 26 07:01:37 Starting compiler/backend/gc
Sep 26 07:04:39 Finished compiler/backend/gc                                   3m01s   8GB
Sep 26 07:04:39 Starting compiler/backend
Sep 26 07:08:40 Finished compiler/backend                                      3m59s   8GB
Sep 26 07:08:40 Starting compiler/encoders/asm
Sep 26 07:09:02 Finished compiler/encoders/asm                                   21s   8GB
Sep 26 07:09:02 Starting compiler/encoders/x64
Sep 26 07:10:03 Finished compiler/encoders/x64                                 1m00s   8GB
Sep 26 07:10:03 Starting compiler/encoders/arm7
Sep 26 07:12:02 Finished compiler/encoders/arm7                                1m58s   8GB
Sep 26 07:12:02 Starting compiler/encoders/arm8
Sep 26 07:12:41 Finished compiler/encoders/arm8                                  38s   8GB
Sep 26 07:12:41 Starting compiler/encoders/mips
Sep 26 07:14:05 Finished compiler/encoders/mips                                1m23s   8GB
Sep 26 07:14:05 Starting compiler/encoders/riscv
Sep 26 07:15:35 Finished compiler/encoders/riscv                               1m29s   8GB
Sep 26 07:15:35 Starting compiler/encoders/ag32
Sep 26 07:15:53 Finished compiler/encoders/ag32                                  17s   8GB
Sep 26 07:15:53 Starting compiler/backend/x64
Sep 26 07:16:10 Finished compiler/backend/x64                                    16s   8GB
Sep 26 07:16:11 Starting compiler/backend/arm7
Sep 26 07:16:28 Finished compiler/backend/arm7                                   17s   8GB
Sep 26 07:16:29 Starting compiler/backend/arm8
Sep 26 07:16:46 Finished compiler/backend/arm8                                   16s   8GB
Sep 26 07:16:46 Starting compiler/backend/mips
Sep 26 07:17:04 Finished compiler/backend/mips                                   17s   8GB
Sep 26 07:17:04 Starting compiler/backend/riscv
Sep 26 07:17:22 Finished compiler/backend/riscv                                  17s   8GB
Sep 26 07:17:22 Starting compiler/backend/ag32
Sep 26 07:18:22 Finished compiler/backend/ag32                                   58s   8GB
Sep 26 07:18:22 Starting compiler/parsing/proofs
Sep 26 07:23:04 Finished compiler/parsing/proofs                               4m41s   8GB
Sep 26 07:23:04 Starting compiler/inference/proofs
Sep 26 07:25:17 Finished compiler/inference/proofs                             2m12s   8GB
Sep 26 07:25:17 Starting compiler/backend/semantics
Sep 26 07:49:22 Finished compiler/backend/semantics                           24m04s  11GB
Sep 26 07:49:22 Starting compiler/backend/reg_alloc/proofs
Sep 26 07:52:46 Finished compiler/backend/reg_alloc/proofs                     3m23s   8GB
Sep 26 07:52:47 Starting compiler/backend/proofs
Sep 26 08:41:48 Finished compiler/backend/proofs                              49m00s  17GB
Sep 26 08:41:48 Starting compiler/encoders/x64/proofs
Sep 26 08:50:40 Finished compiler/encoders/x64/proofs                          8m51s  16GB
Sep 26 08:50:40 Starting compiler/encoders/arm7/proofs
Sep 26 09:03:21 Finished compiler/encoders/arm7/proofs                        12m40s  13GB
Sep 26 09:03:22 Starting compiler/encoders/arm8/proofs
Sep 26 09:09:59 Finished compiler/encoders/arm8/proofs                         6m37s  12GB
Sep 26 09:10:00 Starting compiler/encoders/mips/proofs
Sep 26 09:20:36 Finished compiler/encoders/mips/proofs                        10m35s  13GB
Sep 26 09:20:37 Starting compiler/encoders/riscv/proofs
Sep 26 09:28:59 Finished compiler/encoders/riscv/proofs                        8m22s   8GB
Sep 26 09:28:59 Starting compiler/encoders/ag32/proofs
Sep 26 09:31:29 Finished compiler/encoders/ag32/proofs                         2m28s   8GB
Sep 26 09:31:29 Starting compiler/backend/x64/proofs
Sep 26 09:31:51 Finished compiler/backend/x64/proofs                             21s   8GB
Sep 26 09:31:52 Starting compiler/backend/arm7/proofs
Sep 26 09:32:15 Finished compiler/backend/arm7/proofs                            22s   8GB
Sep 26 09:32:15 Starting compiler/backend/arm8/proofs
Sep 26 09:32:36 Finished compiler/backend/arm8/proofs                            21s   8GB
Sep 26 09:32:37 Starting compiler/backend/mips/proofs
Sep 26 09:32:59 Finished compiler/backend/mips/proofs                            21s   8GB
Sep 26 09:32:59 Starting compiler/backend/riscv/proofs
Sep 26 09:33:20 Finished compiler/backend/riscv/proofs                           21s   8GB
Sep 26 09:33:21 Starting compiler/backend/ag32/proofs
Sep 26 09:44:52 Finished compiler/backend/ag32/proofs                         11m30s  16GB
Sep 26 09:44:52 Starting compiler/proofs
Sep 26 09:46:41 Finished compiler/proofs                                       1m48s  10GB
Sep 26 09:46:41 Starting candle/set-theory
Sep 26 09:47:06 Finished candle/set-theory                                       24s   8GB
Sep 26 09:47:07 Starting candle/syntax-lib
Sep 26 09:47:17 Finished candle/syntax-lib                                       10s   8GB
Sep 26 09:47:18 Starting candle/standard/syntax
Sep 26 09:48:54 Finished candle/standard/syntax                                1m36s   8GB
Sep 26 09:48:55 Starting candle/standard/semantics
Sep 26 09:50:34 Finished candle/standard/semantics                             1m38s   8GB
Sep 26 09:50:34 Starting candle/standard/monadic
Sep 26 09:52:07 Finished candle/standard/monadic                               1m33s   8GB
Sep 26 09:52:08 Starting candle/standard/ml_kernel
Sep 26 09:57:02 Finished candle/standard/ml_kernel                             4m54s  16GB
Sep 26 09:57:03 Starting candle/overloading/syntax
Sep 26 09:59:44 Finished candle/overloading/syntax                             2m41s   8GB
Sep 26 09:59:45 Starting candle/overloading/semantics
Sep 26 10:11:14 Finished candle/overloading/semantics                         11m28s   8GB
Sep 26 10:11:14 Starting characteristic/examples
Sep 26 10:12:29 Finished characteristic/examples                               1m14s  13GB
Sep 26 10:12:29 Starting tutorial/solutions
Sep 26 10:25:52 Finished tutorial/solutions                                   13m22s  20GB
Sep 26 10:25:52 Starting translator/monadic/examples
Sep 26 10:28:37 Finished translator/monadic/examples                           2m45s  12GB
Sep 26 10:28:38 Starting examples
Sep 26 10:35:35 Finished examples                                              6m56s  16GB
Sep 26 10:35:35 Starting examples/compilation/x64
Sep 26 12:35:37 Finished examples/compilation/x64                           2h00m01s  37GB
Sep 26 12:35:37 Starting examples/compilation/x64/proofs
Sep 26 12:37:07 Finished examples/compilation/x64/proofs                       1m29s   9GB
Sep 26 12:37:08 Starting examples/compilation/ag32
Sep 26 13:04:42 Finished examples/compilation/ag32                            27m33s  19GB
Sep 26 13:04:42 Starting examples/compilation/ag32/proofs
Sep 26 13:05:24 Finished examples/compilation/ag32/proofs                        41s   9GB
Sep 26 13:05:25 Starting examples/cost
Sep 26 13:45:48 Finished examples/cost                                        40m23s  23GB
Sep 26 13:45:49 Starting examples/lpr_checker
Sep 26 13:49:23 Finished examples/lpr_checker                                  3m33s  16GB
Sep 26 13:49:23 Starting examples/lpr_checker/compilation
Sep 26 14:03:59 Finished examples/lpr_checker/compilation                     14m35s  21GB
Sep 26 14:03:59 Starting examples/lpr_checker/compilation/proofs
Sep 26 14:04:37 Finished examples/lpr_checker/compilation/proofs                 37s   8GB
Sep 26 14:32:10 Resuming examples/lpr_checker/array
Sep 26 14:45:02 Finished examples/lpr_checker/array                           12m51s  16GB
Sep 26 14:45:02 Starting examples/lpr_checker/array/compilation
Sep 26 15:02:31 Finished examples/lpr_checker/array/compilation               17m28s  24GB
Sep 26 15:02:31 Starting examples/lpr_checker/array/compilation/proofs
Sep 26 15:03:17 Finished examples/lpr_checker/array/compilation/proofs           45s   9GB
Sep 26 15:03:17 Starting examples/opentheory
Sep 26 15:11:50 Finished examples/opentheory                                   8m31s  16GB
Sep 26 15:11:51 Starting examples/opentheory
Sep 26 15:11:52 Finished examples/opentheory                                      0s  57MB
Sep 26 15:11:52 Starting examples/opentheory/compilation
Sep 26 15:42:25 Finished examples/opentheory/compilation                      30m32s  52GB
Sep 26 15:42:25 Starting examples/opentheory/compilation/proofs
Sep 26 15:43:03 Finished examples/opentheory/compilation/proofs                  37s   9GB
Sep 26 15:43:04 Starting examples/opentheory/compilation/ag32
Sep 26 16:13:59 Finished examples/opentheory/compilation/ag32                 30m55s  33GB
Sep 26 16:14:00 Starting examples/opentheory/compilation/ag32/proofs
Sep 26 16:15:28 Finished examples/opentheory/compilation/ag32/proofs           1m27s  15GB
Sep 26 16:15:28 Starting translator/okasaki-examples
Sep 26 16:19:10 Finished translator/okasaki-examples                           3m41s   8GB
Sep 26 16:19:11 Starting translator/other-examples
Sep 26 16:20:56 Finished translator/other-examples                             1m45s   8GB
Sep 26 16:20:57 Starting compiler/parsing/tests
Sep 26 16:21:19 Finished compiler/parsing/tests                                  22s   8GB
Sep 26 16:21:20 Starting compiler/inference/tests
Sep 26 16:25:15 Finished compiler/inference/tests                              3m55s   8GB
Sep 26 16:25:16 Starting compiler/bootstrap/translation
Sep 26 18:53:02 Finished compiler/bootstrap/translation                     2h27m45s  82GB
Sep 26 18:53:02 Starting unverified/sexpr-bootstrap/x64/64
Sep 26 19:01:58 Finished unverified/sexpr-bootstrap/x64/64                     8m54s  12GB
Sep 26 19:01:58 Starting unverified/sexpr-bootstrap/x64/32
Sep 26 19:09:23 Finished unverified/sexpr-bootstrap/x64/32                     7m24s  11GB
Sep 26 19:09:23 Starting compiler/benchmarks
Sep 26 19:09:24 Finished compiler/benchmarks                                      1s  58MB
Sep 26 19:09:25 Starting compiler/bootstrap/compilation/x64/64
Sep 26 20:07:36 FAILED: compiler/bootstrap/compilation/x64/64
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$(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/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$(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/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)/unverified/sexpr-bootstrap[0m
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:   67s  user:   60s     OK
cake-sexpr-64                                                                                                                                                                                                                                  real:   71s  user:   63s     OK
to_dataBootstrapTheory                                                                                                                                                                                                                         real: 3413s  user: 3353s     OK
Starting work on to_lab_x64BootstrapTheory
to_lab_x64BootstrapTheory                                                                                                                                                                                                                      real:   75s  user:   69sFAIL<1>
 Heap: Resizing from 20.92G to 20.92G.  Estimated ratio 7.68
 GC: Completed with insufficient space
 Heap: Full GC (after) Major heap used 2.74G of 2.75G (100%). Alloc space used 379.71M of 6.36G (6%). Total space 20.92G 15% full.
 Heap: Local spaces 8990, permanent spaces 31, code spaces 740, stack spaces 2
 Heap: Code area: total 4.74M occupied: 3.34M
 Heap: Stack area: total 4.00M
 Uncaught exception: Interrupt
 GC (Total): Non-GC time: CPU user: 41.304 system: 5.122 real: 46.532
 GC (Total): GC time: CPU user: 27.708 system: 1.295 real: 29.006
 Heap: Total CPU GC time 29.003secs,  Non-GC 46.427secs, ratio 0.625