Job 1602

CakeML:e7a5c005596708fcf02ba333f849a5ae1eefdf8a
  Merge pull request #839 from CakeML/lpr_transform [Oct 03 11:04:50]
HOL:109bb797367d22a4178d8009554291248f170c63
  More fiddling with holfoot Holmakefiles to get deps right [Oct 12 10:05:04]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Oct 18 08:22:26 Claimed job
Oct 18 08:22:30 Building HOL
Oct 18 08:44:14 Starting developers
Oct 18 08:44:19 Finished developers                                               4s  96MB
Oct 18 08:44:19 Starting developers/bin
Oct 18 08:44:31 Finished developers/bin                                          11s   1GB
Oct 18 08:44:31 Starting semantics/ffi
Oct 18 08:44:47 Finished semantics/ffi                                           16s 311MB
Oct 18 08:44:47 Starting semantics
Oct 18 08:47:03 Finished semantics                                             2m15s   1GB
Oct 18 08:47:03 Starting semantics/proofs
Oct 18 08:51:23 Finished semantics/proofs                                      4m20s   1GB
Oct 18 08:51:24 Starting semantics/alt_semantics
Oct 18 08:51:35 Finished semantics/alt_semantics                                 11s 528MB
Oct 18 08:51:36 Starting semantics/alt_semantics/proofs
Oct 18 08:54:05 Finished semantics/alt_semantics/proofs                        2m29s   1GB
Oct 18 08:54:06 Starting basis/pure
Oct 18 08:57:02 Finished basis/pure                                            2m56s   1GB
Oct 18 08:57:03 Starting translator
Oct 18 09:00:47 Finished translator                                            3m44s   4GB
Oct 18 09:00:47 Starting compiler/parsing
Oct 18 09:02:18 Finished compiler/parsing                                      1m30s   2GB
Oct 18 09:02:18 Starting characteristic
Oct 18 09:08:30 Finished characteristic                                        6m12s   3GB
Oct 18 09:08:30 Starting translator/monadic
Oct 18 09:10:27 Finished translator/monadic                                    1m56s   2GB
Oct 18 09:10:27 Starting basis
Oct 18 09:57:59 Finished basis                                                47m32s  34GB
Oct 18 09:58:00 Starting compiler/inference
Oct 18 09:59:14 Finished compiler/inference                                    1m13s   2GB
Oct 18 09:59:14 Starting compiler/backend/reg_alloc
Oct 18 10:00:22 Finished compiler/backend/reg_alloc                            1m07s   1GB
Oct 18 10:00:22 Starting compiler/backend/gc
Oct 18 10:04:03 Finished compiler/backend/gc                                   3m40s   3GB
Oct 18 10:04:03 Starting compiler/backend
Oct 18 10:09:26 Finished compiler/backend                                      5m22s   4GB
Oct 18 10:09:26 Starting compiler/encoders/asm
Oct 18 10:09:49 Finished compiler/encoders/asm                                   22s   1GB
Oct 18 10:09:49 Starting compiler/encoders/x64
Oct 18 10:10:54 Finished compiler/encoders/x64                                 1m04s   1GB
Oct 18 10:10:54 Starting compiler/encoders/arm7
Oct 18 10:13:02 Finished compiler/encoders/arm7                                2m07s   1GB
Oct 18 10:13:03 Starting compiler/encoders/arm8
Oct 18 10:13:44 Finished compiler/encoders/arm8                                  41s   1GB
Oct 18 10:13:44 Starting compiler/encoders/mips
Oct 18 10:15:13 Finished compiler/encoders/mips                                1m28s   1GB
Oct 18 10:15:13 Starting compiler/encoders/riscv
Oct 18 10:16:55 Finished compiler/encoders/riscv                               1m41s   1GB
Oct 18 10:16:55 Starting compiler/encoders/ag32
Oct 18 10:17:15 Finished compiler/encoders/ag32                                  19s 976MB
Oct 18 10:17:15 Starting compiler/backend/x64
Oct 18 10:17:35 Finished compiler/backend/x64                                    19s   1GB
Oct 18 10:17:35 Starting compiler/backend/arm7
Oct 18 10:17:59 Finished compiler/backend/arm7                                   23s   1GB
Oct 18 10:17:59 Starting compiler/backend/arm8
Oct 18 10:18:20 Finished compiler/backend/arm8                                   21s   1GB
Oct 18 10:18:21 Starting compiler/backend/mips
Oct 18 10:18:43 Finished compiler/backend/mips                                   22s   1GB
Oct 18 10:18:43 Starting compiler/backend/riscv
Oct 18 10:19:05 Finished compiler/backend/riscv                                  21s   1GB
Oct 18 10:19:05 Starting compiler/backend/ag32
Oct 18 10:20:17 Finished compiler/backend/ag32                                 1m11s   2GB
Oct 18 10:20:18 Starting compiler/parsing/proofs
Oct 18 10:22:53 Finished compiler/parsing/proofs                               2m34s   2GB
Oct 18 10:22:53 Starting compiler/inference/proofs
Oct 18 10:25:22 Finished compiler/inference/proofs                             2m28s   1GB
Oct 18 10:25:22 Starting compiler/backend/semantics
Oct 18 10:52:46 Finished compiler/backend/semantics                           27m23s   4GB
Oct 18 10:52:46 Starting compiler/backend/reg_alloc/proofs
Oct 18 10:56:06 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
Oct 18 10:56:06 Starting compiler/backend/proofs
Oct 18 11:48:40 Finished compiler/backend/proofs                              52m33s  27GB
Oct 18 11:48:40 Starting compiler/backend/serialiser
Oct 18 11:49:49 Finished compiler/backend/serialiser                           1m08s   2GB
Oct 18 11:49:50 Starting compiler/encoders/x64/proofs
Oct 18 11:59:16 Finished compiler/encoders/x64/proofs                          9m26s   7GB
Oct 18 11:59:16 Starting compiler/encoders/arm7/proofs
Oct 18 12:12:21 Finished compiler/encoders/arm7/proofs                        13m04s   5GB
Oct 18 12:12:21 Starting compiler/encoders/arm8/proofs
Oct 18 12:19:07 Finished compiler/encoders/arm8/proofs                         6m45s   3GB
Oct 18 12:19:07 Starting compiler/encoders/mips/proofs
Oct 18 12:29:00 Finished compiler/encoders/mips/proofs                         9m52s   4GB
Oct 18 12:29:00 Starting compiler/encoders/riscv/proofs
Oct 18 12:37:24 Finished compiler/encoders/riscv/proofs                        8m23s   3GB
Oct 18 12:37:24 Starting compiler/encoders/ag32/proofs
Oct 18 12:39:45 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Oct 18 12:39:45 Starting compiler/backend/x64/proofs
Oct 18 12:40:08 Finished compiler/backend/x64/proofs                             23s   1GB
Oct 18 12:40:08 Starting compiler/backend/arm7/proofs
Oct 18 12:40:35 Finished compiler/backend/arm7/proofs                            26s   2GB
Oct 18 12:40:35 Starting compiler/backend/arm8/proofs
Oct 18 12:40:57 Finished compiler/backend/arm8/proofs                            21s   1GB
Oct 18 12:40:57 Starting compiler/backend/mips/proofs
Oct 18 12:41:21 Finished compiler/backend/mips/proofs                            23s   1GB
Oct 18 12:41:21 Starting compiler/backend/riscv/proofs
Oct 18 12:41:46 Finished compiler/backend/riscv/proofs                           25s   2GB
Oct 18 12:41:47 Starting compiler/backend/ag32/proofs
Oct 18 12:53:54 Finished compiler/backend/ag32/proofs                         12m07s   4GB
Oct 18 12:53:54 Starting compiler/proofs
Oct 18 12:56:02 Finished compiler/proofs                                       2m07s   6GB
Oct 18 12:56:02 Starting candle/set-theory
Oct 18 12:56:33 Finished candle/set-theory                                       30s   1GB
Oct 18 12:56:33 Starting candle/syntax-lib
Oct 18 12:56:45 Finished candle/syntax-lib                                       12s 816MB
Oct 18 12:56:45 Starting candle/standard/syntax
Oct 18 12:58:40 Finished candle/standard/syntax                                1m54s   1GB
Oct 18 12:58:40 Starting candle/standard/semantics
Oct 18 13:00:28 Finished candle/standard/semantics                             1m47s   2GB
Oct 18 13:00:28 Starting candle/standard/monadic
Oct 18 13:02:10 Finished candle/standard/monadic                               1m42s   1GB
Oct 18 13:02:10 Starting candle/standard/ml_kernel
Oct 18 13:07:43 Finished candle/standard/ml_kernel                             5m31s   5GB
Oct 18 13:07:43 Starting candle/overloading/syntax
Oct 18 13:10:57 Finished candle/overloading/syntax                             3m14s   2GB
Oct 18 13:10:58 Starting candle/overloading/semantics
Oct 18 13:22:12 Finished candle/overloading/semantics                         11m14s   6GB
Oct 18 13:22:12 Starting pancake
Oct 18 13:24:17 Finished pancake                                               2m04s   3GB
Oct 18 13:24:17 Starting pancake/ffi
Oct 18 13:24:17 Finished pancake/ffi                                              0s   6MB
Oct 18 13:24:17 Starting pancake/semantics
Oct 18 13:26:36 Finished pancake/semantics                                     2m18s   2GB
Oct 18 13:26:36 Starting pancake/proofs
Oct 18 13:37:56 Finished pancake/proofs                                       11m19s   9GB
Oct 18 13:37:56 Starting characteristic/examples
Oct 18 13:39:20 Finished characteristic/examples                               1m23s   4GB
Oct 18 13:39:20 Starting tutorial/solutions
Oct 18 13:55:40 Finished tutorial/solutions                                   16m19s  15GB
Oct 18 13:55:40 Starting translator/monadic/examples
Oct 18 13:59:09 Finished translator/monadic/examples                           3m28s   4GB
Oct 18 13:59:10 Starting examples
Oct 18 14:09:09 Finished examples                                              9m59s   6GB
Oct 18 14:09:10 Starting examples/compilation/x64
Oct 18 16:39:58 Finished examples/compilation/x64                           2h30m47s  28GB
Oct 18 16:39:58 Starting examples/compilation/x64/proofs
Oct 18 16:41:23 FAILED: examples/compilation/x64/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[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)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/topology[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/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/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples/compilation/x64[0m
Starting work on README.md
Starting work on catProofTheory
Starting work on diffProofTheory
Starting work on echoProofTheory
README.md                                                                                                                                                     (0s)     OK
Starting work on grepProofTheory
echoProofTheory                                                                                                                                              (39s)     OK
Starting work on helloErrProofTheory
diffProofTheory                                                                                                                                              (39s)     OK
Starting work on helloProofTheory
catProofTheory                                                                                                                                               (40s)     OK
Starting work on iocatProofTheory
grepProofTheory                                                                                                                                              (44s)     OK
Starting work on patchProofTheory
helloProofTheory                                                                                                                                             (32s)FAIL<1>
 Run out of store - interrupting threads
 Failed to recover - exiting
helloErrProofTheory                                                                                                                                          (37s)MKILLED
iocatProofTheory                                                                                                                                             (36s)MKILLED
patchProofTheory                                                                                                                                             (33s)MKILLED