Job 1345

CakeML:aced251f056eb8714178746a7df203a936cc6991
  Fix compiler/parsing/Holmakefile to make parsingComputeLib build [Sep 18 08:05:26]
HOL:2f42c306fae86f050b635244d83cad0953433259
  kolmogorov: work on Lbiased invariant preserved by code-tree insertion [Sep 15 05:48:51]
Machine:oven4s 5.7.19 x86_64 GNU/Linux

Sep 18 14:15:48 Claimed job
Sep 18 14:15:50 Building HOL
Sep 18 14:27:39 Starting developers
Sep 18 14:27:41 Finished developers                                               1s 148MB
Sep 18 14:27:41 Starting developers/bin
Sep 18 14:27:50 Finished developers/bin                                           8s   1GB
Sep 18 14:27:50 Starting semantics/ffi
Sep 18 14:27:58 Finished semantics/ffi                                            8s   1GB
Sep 18 14:27:59 Starting semantics
Sep 18 14:29:17 Finished semantics                                             1m17s   2GB
Sep 18 14:29:17 Starting semantics/proofs
Sep 18 14:32:21 Finished semantics/proofs                                      3m03s   2GB
Sep 18 14:32:21 Starting semantics/alt_semantics
Sep 18 14:32:29 Finished semantics/alt_semantics                                  6s   1GB
Sep 18 14:32:29 Starting semantics/alt_semantics/proofs
Sep 18 14:34:28 Finished semantics/alt_semantics/proofs                        1m58s   2GB
Sep 18 14:34:29 Starting basis/pure
Sep 18 14:36:49 Finished basis/pure                                            2m20s   2GB
Sep 18 14:36:50 Starting translator
Sep 18 14:39:17 Finished translator                                            2m26s   3GB
Sep 18 14:39:17 Starting compiler/parsing
Sep 18 14:40:17 Finished compiler/parsing                                        59s   5GB
Sep 18 14:40:17 Starting characteristic
Sep 18 14:45:50 Finished characteristic                                        5m32s   5GB
Sep 18 14:45:50 Starting translator/monadic
Sep 18 14:47:26 Finished translator/monadic                                    1m35s   3GB
Sep 18 14:47:26 Starting basis
Sep 18 15:19:08 Finished basis                                                31m41s  34GB
Sep 18 15:19:09 Starting compiler/inference
Sep 18 15:20:11 Finished compiler/inference                                    1m02s   3GB
Sep 18 15:20:11 Starting compiler/backend/reg_alloc
Sep 18 15:21:04 Finished compiler/backend/reg_alloc                              52s   2GB
Sep 18 15:21:04 Starting compiler/backend/gc
Sep 18 15:24:06 Finished compiler/backend/gc                                   3m01s   4GB
Sep 18 15:24:07 Starting compiler/backend
Sep 18 15:28:14 Finished compiler/backend                                      4m06s   5GB
Sep 18 15:28:14 Starting compiler/encoders/asm
Sep 18 15:28:36 Finished compiler/encoders/asm                                   20s   1GB
Sep 18 15:28:36 Starting compiler/encoders/x64
Sep 18 15:29:33 Finished compiler/encoders/x64                                   56s   1GB
Sep 18 15:29:34 Starting compiler/encoders/arm7
Sep 18 15:31:29 Finished compiler/encoders/arm7                                1m55s   2GB
Sep 18 15:31:29 Starting compiler/encoders/arm8
Sep 18 15:32:05 Finished compiler/encoders/arm8                                  35s   1GB
Sep 18 15:32:05 Starting compiler/encoders/mips
Sep 18 15:33:25 Finished compiler/encoders/mips                                1m19s   2GB
Sep 18 15:33:26 Starting compiler/encoders/riscv
Sep 18 15:34:54 Finished compiler/encoders/riscv                               1m28s   2GB
Sep 18 15:34:55 Starting compiler/encoders/ag32
Sep 18 15:35:11 Finished compiler/encoders/ag32                                  16s   1GB
Sep 18 15:35:12 Starting compiler/backend/x64
Sep 18 15:35:31 Finished compiler/backend/x64                                    18s   1GB
Sep 18 15:35:31 Starting compiler/backend/arm7
Sep 18 15:35:52 Finished compiler/backend/arm7                                   20s   2GB
Sep 18 15:35:52 Starting compiler/backend/arm8
Sep 18 15:36:12 Finished compiler/backend/arm8                                   18s   1GB
Sep 18 15:36:12 Starting compiler/backend/mips
Sep 18 15:36:30 Finished compiler/backend/mips                                   18s   2GB
Sep 18 15:36:31 Starting compiler/backend/riscv
Sep 18 15:36:50 Finished compiler/backend/riscv                                  19s   2GB
Sep 18 15:36:51 Starting compiler/backend/ag32
Sep 18 15:37:55 Finished compiler/backend/ag32                                 1m04s   2GB
Sep 18 15:37:55 Starting compiler/parsing/proofs
Sep 18 15:42:20 Finished compiler/parsing/proofs                               4m23s   2GB
Sep 18 15:42:20 Starting compiler/inference/proofs
Sep 18 15:44:34 Finished compiler/inference/proofs                             2m13s   2GB
Sep 18 15:44:34 Starting compiler/backend/semantics
Sep 18 16:08:23 Finished compiler/backend/semantics                           23m48s   4GB
Sep 18 16:08:23 Starting compiler/backend/reg_alloc/proofs
Sep 18 16:11:30 Finished compiler/backend/reg_alloc/proofs                     3m05s   2GB
Sep 18 16:11:30 Starting compiler/backend/proofs
Sep 18 16:58:11 Finished compiler/backend/proofs                              46m40s  31GB
Sep 18 16:58:11 Starting compiler/encoders/x64/proofs
Sep 18 17:07:23 Finished compiler/encoders/x64/proofs                          9m10s   5GB
Sep 18 17:07:23 Starting compiler/encoders/arm7/proofs
Sep 18 17:19:27 Finished compiler/encoders/arm7/proofs                        12m03s   8GB
Sep 18 17:19:28 Starting compiler/encoders/arm8/proofs
Sep 18 17:25:46 Finished compiler/encoders/arm8/proofs                         6m17s   3GB
Sep 18 17:25:46 Starting compiler/encoders/mips/proofs
Sep 18 17:35:21 Finished compiler/encoders/mips/proofs                         9m34s   6GB
Sep 18 17:35:21 Starting compiler/encoders/riscv/proofs
Sep 18 17:42:58 Finished compiler/encoders/riscv/proofs                        7m36s   3GB
Sep 18 17:42:58 Starting compiler/encoders/ag32/proofs
Sep 18 17:45:12 Finished compiler/encoders/ag32/proofs                         2m12s   2GB
Sep 18 17:45:12 Starting compiler/backend/x64/proofs
Sep 18 17:45:31 Finished compiler/backend/x64/proofs                             18s   2GB
Sep 18 17:45:31 Starting compiler/backend/arm7/proofs
Sep 18 17:45:54 Finished compiler/backend/arm7/proofs                            21s   2GB
Sep 18 17:45:54 Starting compiler/backend/arm8/proofs
Sep 18 17:46:13 Finished compiler/backend/arm8/proofs                            18s   2GB
Sep 18 17:46:13 Starting compiler/backend/mips/proofs
Sep 18 17:46:33 Finished compiler/backend/mips/proofs                            19s   2GB
Sep 18 17:46:34 Starting compiler/backend/riscv/proofs
Sep 18 17:46:54 Finished compiler/backend/riscv/proofs                           19s   2GB
Sep 18 17:46:54 Starting compiler/backend/ag32/proofs
Sep 18 17:58:16 Finished compiler/backend/ag32/proofs                         11m21s   4GB
Sep 18 17:58:17 Starting compiler/proofs
Sep 18 18:00:02 Finished compiler/proofs                                       1m44s   5GB
Sep 18 18:00:02 Starting candle/set-theory
Sep 18 18:00:28 Finished candle/set-theory                                       25s   1GB
Sep 18 18:00:28 Starting candle/syntax-lib
Sep 18 18:00:38 Finished candle/syntax-lib                                        9s   1GB
Sep 18 18:00:39 Starting candle/standard/syntax
Sep 18 18:02:17 Finished candle/standard/syntax                                1m37s   3GB
Sep 18 18:02:17 Starting candle/standard/semantics
Sep 18 18:03:56 Finished candle/standard/semantics                             1m38s   3GB
Sep 18 18:03:56 Starting candle/standard/monadic
Sep 18 18:05:29 Finished candle/standard/monadic                               1m32s   2GB
Sep 18 18:05:29 Starting candle/standard/ml_kernel
Sep 18 18:10:21 Finished candle/standard/ml_kernel                             4m51s   6GB
Sep 18 18:10:21 Starting candle/overloading/syntax
Sep 18 18:13:11 Finished candle/overloading/syntax                             2m49s   2GB
Sep 18 18:13:12 Starting candle/overloading/semantics
Sep 18 18:24:42 Finished candle/overloading/semantics                         11m30s   8GB
Sep 18 18:24:43 Starting characteristic/examples
Sep 18 18:25:55 Finished characteristic/examples                               1m12s   5GB
Sep 18 18:25:56 Starting tutorial/solutions
Sep 18 18:39:54 Finished tutorial/solutions                                   13m58s  13GB
Sep 18 18:39:55 Starting translator/monadic/examples
Sep 18 18:42:33 Finished translator/monadic/examples                           2m37s   4GB
Sep 18 18:42:33 Starting examples
Sep 18 18:49:27 Finished examples                                              6m53s   8GB
Sep 18 18:49:27 Starting examples/compilation/x64
Sep 18 20:53:58 Finished examples/compilation/x64                           2h04m30s  54GB
Sep 18 20:53:59 Starting examples/compilation/x64/proofs
Sep 18 20:55:39 Finished examples/compilation/x64/proofs                       1m39s   3GB
Sep 18 20:55:39 Starting examples/compilation/ag32
Sep 18 21:24:18 Finished examples/compilation/ag32                            28m38s  11GB
Sep 18 21:24:18 Starting examples/compilation/ag32/proofs
Sep 18 21:24:48 FAILED: examples/compilation/ag32/proofs
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/machine-code/decompiler
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 $(CAKEMLDIR)/examples
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)/examples/compilation/ag32
Starting work on README.md
Starting work on helloProofTheory
Starting work on sortProofTheory
Starting work on wordcountProofTheory
README.md                                       real:    0s  user:    0s     OK
sortProofTheory                                 real:   28s  user:   21sFAIL<1>
 Run out of store - interrupting threads
 Failed to recover - exiting
helloProofTheory                                                        M-KILLED
wordcountProofTheory                                                    M-KILLED