Job 1342

CakeML:85ff1d236459082c90c94fdde129f366318304e5
  riscv: Simplify/optimize FFI jumps [Sep 12 17:49:47]
#752 (rv_fixes)
Merging into: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:oven3s 5.7.19 x86_64 GNU/Linux

Sep 18 14:06:59 Claimed job
Sep 18 14:07:00 Reusing HOL
Sep 18 14:15:13 Starting developers
Sep 18 14:15:16 Finished developers                                               1s 156MB
Sep 18 14:15:16 Starting developers/bin
Sep 18 14:15:24 Finished developers/bin                                           7s   1GB
Sep 18 14:15:24 Starting semantics/ffi
Sep 18 14:15:33 Finished semantics/ffi                                            8s   1GB
Sep 18 14:15:33 Starting semantics
Sep 18 14:16:53 Finished semantics                                             1m19s   2GB
Sep 18 14:16:53 Starting semantics/proofs
Sep 18 14:19:56 Finished semantics/proofs                                      3m02s   2GB
Sep 18 14:19:56 Starting semantics/alt_semantics
Sep 18 14:20:03 Finished semantics/alt_semantics                                  6s   1GB
Sep 18 14:20:04 Starting semantics/alt_semantics/proofs
Sep 18 14:22:04 Finished semantics/alt_semantics/proofs                        1m59s   2GB
Sep 18 14:22:04 Starting basis/pure
Sep 18 14:24:24 Finished basis/pure                                            2m19s   2GB
Sep 18 14:24:24 Starting translator
Sep 18 14:26:51 Finished translator                                            2m26s   3GB
Sep 18 14:26:52 Starting compiler/parsing
Sep 18 14:27:51 Finished compiler/parsing                                        58s   5GB
Sep 18 14:27:51 Starting characteristic
Sep 18 14:33:23 Finished characteristic                                        5m31s   5GB
Sep 18 14:33:23 Starting translator/monadic
Sep 18 14:34:58 Finished translator/monadic                                    1m34s   3GB
Sep 18 14:34:58 Starting basis
Sep 18 15:06:31 Finished basis                                                31m32s  28GB
Sep 18 15:06:32 Starting compiler/inference
Sep 18 15:07:34 Finished compiler/inference                                    1m01s   3GB
Sep 18 15:07:34 Starting compiler/backend/reg_alloc
Sep 18 15:08:26 Finished compiler/backend/reg_alloc                              52s   2GB
Sep 18 15:08:27 Starting compiler/backend/gc
Sep 18 15:11:28 Finished compiler/backend/gc                                   3m00s   5GB
Sep 18 15:11:28 Starting compiler/backend
Sep 18 15:15:38 Finished compiler/backend                                      4m08s   5GB
Sep 18 15:15:38 Starting compiler/encoders/asm
Sep 18 15:15:59 Finished compiler/encoders/asm                                   20s   1GB
Sep 18 15:16:00 Starting compiler/encoders/x64
Sep 18 15:16:57 Finished compiler/encoders/x64                                   57s   1GB
Sep 18 15:16:57 Starting compiler/encoders/arm7
Sep 18 15:18:52 Finished compiler/encoders/arm7                                1m54s   2GB
Sep 18 15:18:52 Starting compiler/encoders/arm8
Sep 18 15:19:27 Finished compiler/encoders/arm8                                  34s   1GB
Sep 18 15:19:27 Starting compiler/encoders/mips
Sep 18 15:20:44 Finished compiler/encoders/mips                                1m16s   2GB
Sep 18 15:20:45 Starting compiler/encoders/riscv
Sep 18 15:22:10 Finished compiler/encoders/riscv                               1m25s   2GB
Sep 18 15:22:11 Starting compiler/encoders/ag32
Sep 18 15:22:27 Finished compiler/encoders/ag32                                  16s   1GB
Sep 18 15:22:28 Starting compiler/backend/x64
Sep 18 15:22:46 Finished compiler/backend/x64                                    18s   1GB
Sep 18 15:22:47 Starting compiler/backend/arm7
Sep 18 15:23:07 Finished compiler/backend/arm7                                   19s   2GB
Sep 18 15:23:07 Starting compiler/backend/arm8
Sep 18 15:23:25 Finished compiler/backend/arm8                                   17s   2GB
Sep 18 15:23:25 Starting compiler/backend/mips
Sep 18 15:23:43 Finished compiler/backend/mips                                   18s   2GB
Sep 18 15:23:44 Starting compiler/backend/riscv
Sep 18 15:24:03 Finished compiler/backend/riscv                                  18s   2GB
Sep 18 15:24:03 Starting compiler/backend/ag32
Sep 18 15:25:04 Finished compiler/backend/ag32                                 1m01s   2GB
Sep 18 15:25:05 Starting compiler/parsing/proofs
Sep 18 15:29:32 Finished compiler/parsing/proofs                               4m27s   2GB
Sep 18 15:29:33 Starting compiler/inference/proofs
Sep 18 15:31:47 Finished compiler/inference/proofs                             2m13s   2GB
Sep 18 15:31:47 Starting compiler/backend/semantics
Sep 18 15:55:06 Finished compiler/backend/semantics                           23m16s   6GB
Sep 18 15:55:06 Starting compiler/backend/reg_alloc/proofs
Sep 18 15:58:05 Finished compiler/backend/reg_alloc/proofs                     2m58s   2GB
Sep 18 15:58:06 Starting compiler/backend/proofs
Sep 18 16:45:15 Finished compiler/backend/proofs                              47m08s  23GB
Sep 18 16:45:15 Starting compiler/encoders/x64/proofs
Sep 18 16:54:27 Finished compiler/encoders/x64/proofs                          9m12s   5GB
Sep 18 16:54:28 Starting compiler/encoders/arm7/proofs
Sep 18 17:06:32 Finished compiler/encoders/arm7/proofs                        12m03s  10GB
Sep 18 17:06:32 Starting compiler/encoders/arm8/proofs
Sep 18 17:12:48 Finished compiler/encoders/arm8/proofs                         6m15s   3GB
Sep 18 17:12:48 Starting compiler/encoders/mips/proofs
Sep 18 17:22:29 Finished compiler/encoders/mips/proofs                         9m40s   5GB
Sep 18 17:22:29 Starting compiler/encoders/riscv/proofs
Sep 18 17:30:27 Finished compiler/encoders/riscv/proofs                        7m57s   3GB
Sep 18 17:30:27 Starting compiler/encoders/ag32/proofs
Sep 18 17:32:44 Finished compiler/encoders/ag32/proofs                         2m15s   2GB
Sep 18 17:32:44 Starting compiler/backend/x64/proofs
Sep 18 17:33:04 Finished compiler/backend/x64/proofs                             19s   2GB
Sep 18 17:33:04 Starting compiler/backend/arm7/proofs
Sep 18 17:33:25 Finished compiler/backend/arm7/proofs                            20s   2GB
Sep 18 17:33:25 Starting compiler/backend/arm8/proofs
Sep 18 17:33:45 Finished compiler/backend/arm8/proofs                            18s   2GB
Sep 18 17:33:45 Starting compiler/backend/mips/proofs
Sep 18 17:34:06 Finished compiler/backend/mips/proofs                            20s   2GB
Sep 18 17:34:06 Starting compiler/backend/riscv/proofs
Sep 18 17:34:26 Finished compiler/backend/riscv/proofs                           20s   2GB
Sep 18 17:34:27 Starting compiler/backend/ag32/proofs
Sep 18 17:45:53 Finished compiler/backend/ag32/proofs                         11m20s   6GB
Sep 18 17:45:53 Starting compiler/proofs
Sep 18 17:47:39 Finished compiler/proofs                                       1m45s   5GB
Sep 18 17:47:39 Starting candle/set-theory
Sep 18 17:48:05 Finished candle/set-theory                                       25s   1GB
Sep 18 17:48:05 Starting candle/syntax-lib
Sep 18 17:48:15 Finished candle/syntax-lib                                        9s   1GB
Sep 18 17:48:16 Starting candle/standard/syntax
Sep 18 17:49:54 Finished candle/standard/syntax                                1m38s   2GB
Sep 18 17:49:55 Starting candle/standard/semantics
Sep 18 17:51:34 Finished candle/standard/semantics                             1m39s   3GB
Sep 18 17:51:34 Starting candle/standard/monadic
Sep 18 17:53:06 Finished candle/standard/monadic                               1m31s   2GB
Sep 18 17:53:06 Starting candle/standard/ml_kernel
Sep 18 17:57:59 Finished candle/standard/ml_kernel                             4m52s   6GB
Sep 18 17:57:59 Starting candle/overloading/syntax
Sep 18 18:00:45 Finished candle/overloading/syntax                             2m45s   3GB
Sep 18 18:00:45 Starting candle/overloading/semantics
Sep 18 18:12:17 Finished candle/overloading/semantics                         11m31s   8GB
Sep 18 18:12:17 Starting characteristic/examples
Sep 18 18:13:30 Finished characteristic/examples                               1m11s   5GB
Sep 18 18:13:30 Starting tutorial/solutions
Sep 18 18:27:08 Finished tutorial/solutions                                   13m37s  21GB
Sep 18 18:27:08 Starting translator/monadic/examples
Sep 18 18:29:51 Finished translator/monadic/examples                           2m42s   4GB
Sep 18 18:29:51 Starting examples
Sep 18 18:37:00 Finished examples                                              7m08s  10GB
Sep 18 18:37:00 Starting examples/compilation/x64
Sep 18 20:42:30 Finished examples/compilation/x64                           2h05m29s  33GB
Sep 18 20:42:31 Starting examples/compilation/x64/proofs
Sep 18 20:44:09 Finished examples/compilation/x64/proofs                       1m37s   3GB
Sep 18 20:44:09 Starting examples/compilation/ag32
Sep 18 21:13:06 Finished examples/compilation/ag32                            28m55s  13GB
Sep 18 21:13:06 Starting examples/compilation/ag32/proofs
Sep 18 21:13:37 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