Job 1359

CakeML:aced251f056eb8714178746a7df203a936cc6991
  Fix compiler/parsing/Holmakefile to make parsingComputeLib build [Sep 18 08:05:26]
HOL:412fb6454a8fa37864443db29a5d354d425a0a78
  emacs-mode: add indentation after Unicode iff symbol [Sep 18 07:22:36]
Machine:oven4s 5.7.19 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

Sep 22 22:41:15 Claimed job
Sep 22 22:41:16 Reusing HOL
Sep 22 22:41:26 Starting developers
Sep 22 22:41:29 Finished developers                                               1s 161MB
Sep 22 22:41:29 Starting developers/bin
Sep 22 22:41:37 Finished developers/bin                                           8s   1GB
Sep 22 22:41:38 Starting semantics/ffi
Sep 22 22:41:47 Finished semantics/ffi                                            9s   2GB
Sep 22 22:41:48 Starting semantics
Sep 22 22:42:56 Finished semantics                                             1m08s   4GB
Sep 22 22:42:57 Starting semantics/proofs
Sep 22 22:45:57 Finished semantics/proofs                                      3m00s   5GB
Sep 22 22:45:58 Starting semantics/alt_semantics
Sep 22 22:46:06 Finished semantics/alt_semantics                                  7s   4GB
Sep 22 22:46:06 Starting semantics/alt_semantics/proofs
Sep 22 22:48:03 Finished semantics/alt_semantics/proofs                        1m56s   4GB
Sep 22 22:48:04 Starting basis/pure
Sep 22 22:48:48 Finished basis/pure                                              43s   4GB
Sep 22 22:48:48 Starting translator
Sep 22 22:51:09 Finished translator                                            2m20s   7GB
Sep 22 22:51:09 Starting compiler/parsing
Sep 22 22:52:09 Finished compiler/parsing                                        59s   6GB
Sep 22 22:52:09 Starting characteristic
Sep 22 22:57:40 Finished characteristic                                        5m30s   5GB
Sep 22 22:57:40 Starting translator/monadic
Sep 22 22:59:08 Finished translator/monadic                                    1m27s   4GB
Sep 22 22:59:08 Starting basis
Sep 22 23:30:34 Finished basis                                                31m25s  39GB
Sep 22 23:30:34 Starting compiler/inference
Sep 22 23:31:29 Finished compiler/inference                                      54s   4GB
Sep 22 23:31:29 Starting compiler/backend/reg_alloc
Sep 22 23:32:18 Finished compiler/backend/reg_alloc                              48s   4GB
Sep 22 23:32:18 Starting compiler/backend/gc
Sep 22 23:35:01 Finished compiler/backend/gc                                   2m42s   6GB
Sep 22 23:35:01 Starting compiler/backend
Sep 22 23:39:07 Finished compiler/backend                                      4m05s   7GB
Sep 22 23:39:07 Starting compiler/encoders/asm
Sep 22 23:39:27 Finished compiler/encoders/asm                                   19s   4GB
Sep 22 23:39:28 Starting compiler/encoders/x64
Sep 22 23:39:50 Finished compiler/encoders/x64                                   22s   4GB
Sep 22 23:39:51 Starting compiler/encoders/arm7
Sep 22 23:40:38 Finished compiler/encoders/arm7                                  47s   4GB
Sep 22 23:40:39 Starting compiler/encoders/arm8
Sep 22 23:40:50 Finished compiler/encoders/arm8                                  10s   4GB
Sep 22 23:40:50 Starting compiler/encoders/mips
Sep 22 23:41:07 Finished compiler/encoders/mips                                  16s   4GB
Sep 22 23:41:07 Starting compiler/encoders/riscv
Sep 22 23:41:21 Finished compiler/encoders/riscv                                 13s   4GB
Sep 22 23:41:22 Starting compiler/encoders/ag32
Sep 22 23:41:38 Finished compiler/encoders/ag32                                  15s   4GB
Sep 22 23:41:38 Starting compiler/backend/x64
Sep 22 23:41:56 Finished compiler/backend/x64                                    17s   4GB
Sep 22 23:41:56 Starting compiler/backend/arm7
Sep 22 23:42:15 Finished compiler/backend/arm7                                   18s   4GB
Sep 22 23:42:15 Starting compiler/backend/arm8
Sep 22 23:42:33 Finished compiler/backend/arm8                                   17s   4GB
Sep 22 23:42:34 Starting compiler/backend/mips
Sep 22 23:42:52 Finished compiler/backend/mips                                   18s   4GB
Sep 22 23:42:52 Starting compiler/backend/riscv
Sep 22 23:43:11 Finished compiler/backend/riscv                                  18s   4GB
Sep 22 23:43:11 Starting compiler/backend/ag32
Sep 22 23:44:14 Finished compiler/backend/ag32                                 1m01s   4GB
Sep 22 23:44:14 Starting compiler/parsing/proofs
Sep 22 23:48:50 Finished compiler/parsing/proofs                               4m35s   4GB
Sep 22 23:48:50 Starting compiler/inference/proofs
Sep 22 23:51:02 Finished compiler/inference/proofs                             2m11s   4GB
Sep 22 23:51:02 Starting compiler/backend/semantics
Sep 23 00:13:48 Finished compiler/backend/semantics                           22m45s   8GB
Sep 23 00:13:48 Starting compiler/backend/reg_alloc/proofs
Sep 23 00:16:46 Finished compiler/backend/reg_alloc/proofs                     2m56s   4GB
Sep 23 00:16:46 Starting compiler/backend/proofs
Sep 23 01:06:24 Finished compiler/backend/proofs                              49m38s  22GB
Sep 23 01:06:25 Starting compiler/encoders/x64/proofs
Sep 23 01:15:32 Finished compiler/encoders/x64/proofs                          9m06s  10GB
Sep 23 01:15:33 Starting compiler/encoders/arm7/proofs
Sep 23 01:27:43 Finished compiler/encoders/arm7/proofs                        12m10s  13GB
Sep 23 01:27:43 Starting compiler/encoders/arm8/proofs
Sep 23 01:33:46 Finished compiler/encoders/arm8/proofs                         6m02s   5GB
Sep 23 01:33:46 Starting compiler/encoders/mips/proofs
Sep 23 01:43:30 Finished compiler/encoders/mips/proofs                         9m43s   6GB
Sep 23 01:43:30 Starting compiler/encoders/riscv/proofs
Sep 23 01:51:01 Finished compiler/encoders/riscv/proofs                        7m30s   8GB
Sep 23 01:51:02 Starting compiler/encoders/ag32/proofs
Sep 23 01:53:17 Finished compiler/encoders/ag32/proofs                         2m15s   4GB
Sep 23 01:53:17 Starting compiler/backend/x64/proofs
Sep 23 01:53:38 Finished compiler/backend/x64/proofs                             19s   4GB
Sep 23 01:53:38 Starting compiler/backend/arm7/proofs
Sep 23 01:54:00 Finished compiler/backend/arm7/proofs                            21s   4GB
Sep 23 01:54:00 Starting compiler/backend/arm8/proofs
Sep 23 01:54:20 Finished compiler/backend/arm8/proofs                            19s   4GB
Sep 23 01:54:21 Starting compiler/backend/mips/proofs
Sep 23 01:54:41 Finished compiler/backend/mips/proofs                            20s   4GB
Sep 23 01:54:42 Starting compiler/backend/riscv/proofs
Sep 23 01:55:02 Finished compiler/backend/riscv/proofs                           20s   4GB
Sep 23 01:55:03 Starting compiler/backend/ag32/proofs
Sep 23 02:06:25 Finished compiler/backend/ag32/proofs                         11m22s  11GB
Sep 23 02:06:26 Starting compiler/proofs
Sep 23 02:07:59 Finished compiler/proofs                                       1m33s   7GB
Sep 23 02:08:00 Starting candle/set-theory
Sep 23 02:08:24 Finished candle/set-theory                                       23s   4GB
Sep 23 02:08:24 Starting candle/syntax-lib
Sep 23 02:08:34 Finished candle/syntax-lib                                        9s   4GB
Sep 23 02:08:34 Starting candle/standard/syntax
Sep 23 02:10:10 Finished candle/standard/syntax                                1m35s   4GB
Sep 23 02:10:10 Starting candle/standard/semantics
Sep 23 02:11:49 Finished candle/standard/semantics                             1m38s   5GB
Sep 23 02:11:49 Starting candle/standard/monadic
Sep 23 02:13:22 Finished candle/standard/monadic                               1m32s   4GB
Sep 23 02:13:22 Starting candle/standard/ml_kernel
Sep 23 02:18:14 Finished candle/standard/ml_kernel                             4m51s  10GB
Sep 23 02:18:14 Starting candle/overloading/syntax
Sep 23 02:21:12 Finished candle/overloading/syntax                             2m56s   5GB
Sep 23 02:21:12 Starting candle/overloading/semantics
Sep 23 02:33:07 Finished candle/overloading/semantics                         11m54s   9GB
Sep 23 02:33:08 Starting characteristic/examples
Sep 23 02:34:25 Finished characteristic/examples                               1m16s  10GB
Sep 23 02:34:25 Starting tutorial/solutions
Sep 23 02:48:03 Finished tutorial/solutions                                   13m37s  14GB
Sep 23 02:48:03 Starting translator/monadic/examples
Sep 23 02:50:51 Finished translator/monadic/examples                           2m47s   7GB
Sep 23 02:50:51 Starting examples
Sep 23 02:58:29 Finished examples                                              7m36s  11GB
Sep 23 02:58:29 Starting examples/compilation/x64
Sep 23 05:15:14 Finished examples/compilation/x64                           2h16m44s  57GB
Sep 23 05:15:14 Starting examples/compilation/x64/proofs
Sep 23 05:17:04 Finished examples/compilation/x64/proofs                       1m49s   5GB
Sep 23 05:17:04 Starting examples/compilation/ag32
Sep 23 05:47:17 Finished examples/compilation/ag32                            30m12s  11GB
Sep 23 05:47:17 Starting examples/compilation/ag32/proofs
Sep 23 05:47:59 Finished examples/compilation/ag32/proofs                        41s   6GB
Sep 23 05:47:59 Starting examples/cost
Sep 23 06:30:11 Finished examples/cost                                        42m10s  17GB
Sep 23 06:30:11 Starting examples/lpr_checker
Sep 23 06:34:27 Finished examples/lpr_checker                                  4m15s  11GB
Sep 23 06:34:28 Starting examples/lpr_checker/compilation
Sep 23 06:51:20 Finished examples/lpr_checker/compilation                     16m52s  17GB
Sep 23 06:51:21 Starting examples/lpr_checker/compilation/proofs
Sep 23 06:51:58 Finished examples/lpr_checker/compilation/proofs                 36s   5GB
Sep 23 06:51:58 Starting examples/lpr_checker/array
Sep 23 07:03:51 Finished examples/lpr_checker/array                           11m52s  10GB
Sep 23 07:03:52 Starting examples/lpr_checker/array/compilation
Sep 23 07:20:48 Finished examples/lpr_checker/array/compilation               16m55s  27GB
Sep 23 07:20:48 Starting examples/lpr_checker/array/compilation/proofs
Sep 23 07:21:31 Finished examples/lpr_checker/array/compilation/proofs           42s   6GB
Sep 23 07:21:32 Starting examples/opentheory
Sep 23 07:30:02 Finished examples/opentheory                                   8m30s  11GB
Sep 23 07:30:03 Starting examples/opentheory
Sep 23 07:30:03 Finished examples/opentheory                                      0s  47MB
Sep 23 07:30:04 Starting examples/opentheory/compilation
Sep 23 07:58:59 Finished examples/opentheory/compilation                      28m54s  37GB
Sep 23 07:58:59 Starting examples/opentheory/compilation/proofs
Sep 23 07:59:37 Finished examples/opentheory/compilation/proofs                  36s   5GB
Sep 23 07:59:37 Starting examples/opentheory/compilation/ag32
Sep 23 08:29:59 Finished examples/opentheory/compilation/ag32                 30m21s  30GB
Sep 23 08:29:59 Starting examples/opentheory/compilation/ag32/proofs
Sep 23 08:31:26 Finished examples/opentheory/compilation/ag32/proofs           1m26s  10GB
Sep 23 08:31:27 Starting translator/okasaki-examples
Sep 23 08:35:10 Finished translator/okasaki-examples                           3m43s   8GB
Sep 23 08:35:11 Starting translator/other-examples
Sep 23 08:35:48 Finished translator/other-examples                               36s   5GB
Sep 23 08:35:48 Starting compiler/parsing/tests
Sep 23 08:36:10 Finished compiler/parsing/tests                                  21s   4GB
Sep 23 08:36:10 Starting compiler/inference/tests
Sep 23 08:40:08 Finished compiler/inference/tests                              3m57s   8GB
Sep 23 08:40:08 Starting compiler/bootstrap/translation
Sep 23 11:09:52 Finished compiler/bootstrap/translation                     2h29m43s  80GB
Sep 23 11:09:52 Starting unverified/sexpr-bootstrap/x64/64
Sep 23 11:18:54 Finished unverified/sexpr-bootstrap/x64/64                     8m57s   8GB
Sep 23 11:18:55 Starting unverified/sexpr-bootstrap/x64/32
Sep 23 11:26:22 Finished unverified/sexpr-bootstrap/x64/32                     7m23s   8GB
Sep 23 11:26:22 Starting compiler/benchmarks
Sep 23 11:26:23 Finished compiler/benchmarks                                      0s  50MB
Sep 23 11:26:23 Starting compiler/bootstrap/compilation/x64/64
Sep 24 04:33:54 Finished compiler/bootstrap/compilation/x64/64             17h07m27s  92GB
Sep 24 04:33:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 24 04:47:35 Finished compiler/bootstrap/compilation/x64/64/proofs         13m39s  14GB
Sep 24 04:47:36 Starting compiler/bootstrap/compilation/x64/32
Sep 24 17:52:30 Finished compiler/bootstrap/compilation/x64/32             13h04m50s 107GB
Sep 24 17:52:31 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 24 17:54:55 Finished compiler/bootstrap/compilation/x64/32/proofs          2m23s  20GB
Sep 24 17:54:55 Starting compiler/bootstrap/compilation/ag32/32
Sep 25 10:36:58 Finished compiler/bootstrap/compilation/ag32/32            16h42m02s 107GB
Sep 25 10:36:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 25 10:38:00 FAILED: compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/balanced_bst
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 $(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 $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
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/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Starting work on README.md
Starting work on ag32BootstrapProofTheory
README.md                                       real:    0s  user:    0s     OK
ag32BootstrapProofTheory                        real:   59s  user:   55sFAIL<1>
 Heap: Resizing from 6.09G to 7.12G.  Estimated ratio 5.59
 GC: Completed with insufficient space
 Heap: Full GC (after) Major heap used 2.27G of 2.27G (100%). Alloc space used 153.86M of 2.57G (6%). Total space 7.12G 34% full.
 Heap: Local spaces 4689, permanent spaces 29, code spaces 71, stack spaces 2
 Heap: Code area: total 564.00K occupied: 229.39K
 Heap: Stack area: total 1.00M
 Uncaught exception: Interrupt
 GC (Total): Non-GC time: CPU user: 30.756 system: 3.528 real: 34.299
 GC (Total): GC time: CPU user: 24.262 system: 1.097 real: 25.359
 Heap: Total CPU GC time 25.359secs,  Non-GC 34.284secs, ratio 0.740