Job 2297

CakeML:806f5da2e637d64185fcd2d143e3acef62800f6e
  Merge remote-tracking branch 'origin/master' into alist_subst [Feb 08 07:52:47]
#981 (alist_subst)
Merging into:b76383b2a589101f171319130980075afdc90158
  Fix data_to_word_assignProof given integer$Num rewrites changes [Jan 30 06:21:36]
HOL:c5f2bc287fa6507cfb3372b4b827105b9633636b
  Other cheatsheet additions: `iff_tac`/`eq_tac` and `ExclSF` [Feb 08 23:51:55]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 12 14:26:18 Claimed job
Feb 12 14:26:27 Building HOL
Feb 12 14:43:10 Starting developers
Feb 12 14:43:11 Finished developers                                               0s  38MB
Feb 12 14:43:11 Starting developers/bin
Feb 12 14:43:18 Finished developers/bin                                           6s   1GB
Feb 12 14:43:18 Starting compiler/proofs
Feb 12 16:52:19 Finished compiler/proofs                                    2h09m01s  39GB
Feb 12 16:52:20 Starting compiler/bootstrap/translation
Feb 13 02:06:57 Finished compiler/bootstrap/translation                     9h14m37s  39GB
Feb 13 02:06:57 Starting semantics/ffi
Feb 13 02:07:06 Finished semantics/ffi                                            8s 710MB
Feb 13 02:07:06 Starting semantics
Feb 13 02:07:07 Finished semantics                                                0s  77MB
Feb 13 02:07:07 Starting semantics/proofs
Feb 13 02:07:44 Finished semantics/proofs                                        36s   1GB
Feb 13 02:07:44 Starting semantics/alt_semantics
Feb 13 02:08:27 Finished semantics/alt_semantics                                 42s   1GB
Feb 13 02:08:27 Starting semantics/alt_semantics/proofs
Feb 13 02:20:12 Finished semantics/alt_semantics/proofs                       11m44s   2GB
Feb 13 02:20:12 Starting basis/pure
Feb 13 02:20:13 Finished basis/pure                                               0s  83MB
Feb 13 02:20:13 Starting translator
Feb 13 02:22:08 Finished translator                                            1m54s   3GB
Feb 13 02:22:08 Starting compiler/parsing
Feb 13 02:22:09 Finished compiler/parsing                                         0s  85MB
Feb 13 02:22:09 Starting characteristic
Feb 13 02:22:11 Finished characteristic                                           1s 105MB
Feb 13 02:22:11 Starting translator/monadic
Feb 13 02:22:12 Finished translator/monadic                                       1s 107MB
Feb 13 02:22:12 Starting basis
Feb 13 02:26:07 Finished basis                                                 3m54s   5GB
Feb 13 02:26:07 Starting compiler/inference
Feb 13 02:26:08 Finished compiler/inference                                       0s  94MB
Feb 13 02:26:08 Starting compiler/backend/reg_alloc
Feb 13 02:26:09 Finished compiler/backend/reg_alloc                               0s  76MB
Feb 13 02:26:09 Starting compiler/backend/gc
Feb 13 02:26:11 Finished compiler/backend/gc                                      1s 146MB
Feb 13 02:26:11 Starting compiler/backend
Feb 13 02:26:30 Finished compiler/backend                                        18s   1GB
Feb 13 02:26:30 Starting compiler/encoders/asm
Feb 13 02:26:31 Finished compiler/encoders/asm                                    1s 100MB
Feb 13 02:26:31 Starting compiler/encoders/x64
Feb 13 02:26:33 Finished compiler/encoders/x64                                    1s 109MB
Feb 13 02:26:33 Starting compiler/encoders/arm7
Feb 13 02:26:34 Finished compiler/encoders/arm7                                   1s 112MB
Feb 13 02:26:34 Starting compiler/encoders/arm8
Feb 13 02:26:35 Finished compiler/encoders/arm8                                   1s 109MB
Feb 13 02:26:36 Starting compiler/encoders/arm8_asl
Feb 13 04:51:12 Finished compiler/encoders/arm8_asl                         2h24m36s  44GB
Feb 13 04:51:12 Starting compiler/encoders/mips
Feb 13 04:51:14 Finished compiler/encoders/mips                                   1s 109MB
Feb 13 04:51:14 Starting compiler/encoders/riscv
Feb 13 04:51:15 Finished compiler/encoders/riscv                                  1s 104MB
Feb 13 04:51:15 Starting compiler/encoders/ag32
Feb 13 04:51:16 Finished compiler/encoders/ag32                                   1s 100MB
Feb 13 04:51:17 Starting compiler/backend/x64
Feb 13 04:51:18 Finished compiler/backend/x64                                     1s 141MB
Feb 13 04:51:19 Starting compiler/backend/arm7
Feb 13 04:51:20 Finished compiler/backend/arm7                                    1s 141MB
Feb 13 04:51:21 Starting compiler/backend/arm8
Feb 13 04:51:22 Finished compiler/backend/arm8                                    1s 141MB
Feb 13 04:51:23 Starting compiler/backend/mips
Feb 13 04:51:24 Finished compiler/backend/mips                                    1s 141MB
Feb 13 04:51:25 Starting compiler/backend/riscv
Feb 13 04:51:26 Finished compiler/backend/riscv                                   1s 141MB
Feb 13 04:51:27 Starting compiler/backend/ag32
Feb 13 04:52:57 Finished compiler/backend/ag32                                 1m30s   1GB
Feb 13 04:52:57 Starting compiler/parsing/proofs
Feb 13 04:52:58 Finished compiler/parsing/proofs                                  0s  83MB
Feb 13 04:52:59 Starting compiler/inference/proofs
Feb 13 04:53:00 Finished compiler/inference/proofs                                0s 105MB
Feb 13 04:53:00 Starting compiler/backend/semantics
Feb 13 04:54:32 Finished compiler/backend/semantics                            1m31s   2GB
Feb 13 04:54:32 Starting compiler/backend/reg_alloc/proofs
Feb 13 04:54:33 Finished compiler/backend/reg_alloc/proofs                        1s 107MB
Feb 13 04:54:34 Starting compiler/backend/proofs
Feb 13 04:55:40 Finished compiler/backend/proofs                               1m06s   3GB
Feb 13 04:55:40 Starting compiler/backend/serialiser
Feb 13 04:55:43 Finished compiler/backend/serialiser                              2s 206MB
Feb 13 04:55:43 Starting compiler/encoders/x64/proofs
Feb 13 05:05:41 Finished compiler/encoders/x64/proofs                          9m58s   5GB
Feb 13 05:05:41 Starting compiler/encoders/arm7/proofs
Feb 13 05:19:10 Finished compiler/encoders/arm7/proofs                        13m28s   9GB
Feb 13 05:19:10 Starting compiler/encoders/arm8/proofs
Feb 13 05:25:56 Finished compiler/encoders/arm8/proofs                         6m46s   4GB
Feb 13 05:25:56 Starting compiler/encoders/arm8_asl/proofs
Feb 13 06:16:14 Finished compiler/encoders/arm8_asl/proofs                    50m17s  11GB
Feb 13 06:16:14 Starting compiler/encoders/mips/proofs
Feb 13 06:26:53 Finished compiler/encoders/mips/proofs                        10m38s   7GB
Feb 13 06:26:54 Starting compiler/encoders/riscv/proofs
Feb 13 06:35:30 Finished compiler/encoders/riscv/proofs                        8m36s   3GB
Feb 13 06:35:31 Starting compiler/encoders/ag32/proofs
Feb 13 06:37:57 Finished compiler/encoders/ag32/proofs                         2m26s   2GB
Feb 13 06:37:57 Starting compiler/backend/x64/proofs
Feb 13 06:38:41 Finished compiler/backend/x64/proofs                             43s   2GB
Feb 13 06:38:41 Starting compiler/backend/arm7/proofs
Feb 13 06:39:30 Finished compiler/backend/arm7/proofs                            47s   3GB
Feb 13 06:39:30 Starting compiler/backend/arm8/proofs
Feb 13 06:40:12 Finished compiler/backend/arm8/proofs                            42s   3GB
Feb 13 06:40:12 Starting compiler/backend/arm8_asl
Feb 13 06:40:43 Finished compiler/backend/arm8_asl                               30s   2GB
Feb 13 06:40:43 Starting compiler/backend/mips/proofs
Feb 13 06:41:32 Finished compiler/backend/mips/proofs                            49s   3GB
Feb 13 06:41:32 Starting compiler/backend/riscv/proofs
Feb 13 06:42:25 Finished compiler/backend/riscv/proofs                           52s   3GB
Feb 13 06:42:26 Starting compiler/backend/ag32/proofs
Feb 13 06:56:03 Finished compiler/backend/ag32/proofs                         13m37s   6GB
Feb 13 06:56:03 Starting candle/set-theory
Feb 13 06:56:51 Finished candle/set-theory                                       47s   1GB
Feb 13 06:56:52 Starting candle/syntax-lib
Feb 13 06:56:52 Finished candle/syntax-lib                                        0s  89MB
Feb 13 06:56:53 Starting candle/standard/syntax
Feb 13 06:57:09 Finished candle/standard/syntax                                  15s   1GB
Feb 13 06:57:09 Starting candle/standard/semantics
Feb 13 06:59:39 Finished candle/standard/semantics                             2m29s   2GB
Feb 13 06:59:39 Starting candle/standard/monadic
Feb 13 06:59:41 Finished candle/standard/monadic                                  1s 117MB
Feb 13 06:59:41 Starting candle/standard/ml_kernel
Feb 13 07:01:38 Finished candle/standard/ml_kernel                             1m56s   4GB
Feb 13 07:01:38 Starting candle/overloading/syntax
Feb 13 07:05:16 Finished candle/overloading/syntax                             3m38s   2GB
Feb 13 07:05:17 Starting candle/overloading/semantics
Feb 13 07:17:08 Finished candle/overloading/semantics                         11m50s   3GB
Feb 13 07:17:08 Starting candle/overloading/monadic
Feb 13 07:19:51 Finished candle/overloading/monadic                            2m42s   2GB
Feb 13 07:19:51 Starting candle/overloading/ml_kernel
Feb 13 07:27:54 Finished candle/overloading/ml_kernel                          8m03s   6GB
Feb 13 07:27:55 Starting candle/overloading/ml_checker
Feb 13 07:30:36 Finished candle/overloading/ml_checker                         2m41s   7GB
Feb 13 07:30:36 Starting candle/prover
Feb 13 07:41:00 Finished candle/prover                                        10m23s   5GB
Feb 13 07:41:00 Starting pancake
Feb 13 07:42:05 Finished pancake                                               1m04s   1GB
Feb 13 07:42:06 Starting pancake/ffi
Feb 13 07:42:06 Finished pancake/ffi                                              0s  24MB
Feb 13 07:42:06 Starting pancake/semantics
Feb 13 07:44:45 Finished pancake/semantics                                     2m39s   2GB
Feb 13 07:44:46 Starting pancake/parser
Feb 13 07:45:13 Finished pancake/parser                                          27s   1GB
Feb 13 07:45:14 Starting pancake/proofs
Feb 13 08:16:47 Finished pancake/proofs                                       31m33s   8GB
Feb 13 08:16:47 Starting characteristic/examples
Feb 13 08:18:34 Finished characteristic/examples                               1m46s   6GB
Feb 13 08:18:34 Starting tutorial/solutions
Feb 13 08:35:04 Finished tutorial/solutions                                   16m30s  18GB
Feb 13 08:35:05 Starting translator/monadic/examples
Feb 13 08:39:51 Finished translator/monadic/examples                           4m46s   5GB
Feb 13 08:39:51 Starting examples
Feb 13 08:57:36 Finished examples                                             17m44s   7GB
Feb 13 08:57:36 Starting examples/compilation/x64
Feb 13 11:00:51 Finished examples/compilation/x64                           2h03m13s  15GB
Feb 13 11:00:51 Starting examples/compilation/x64/proofs
Feb 13 11:05:17 Finished examples/compilation/x64/proofs                       4m25s   5GB
Feb 13 11:05:17 Starting examples/compilation/ag32
Feb 13 11:36:24 Finished examples/compilation/ag32                            31m06s   8GB
Feb 13 11:36:24 Starting examples/compilation/ag32/proofs
Feb 13 11:37:16 FAILED: examples/compilation/ag32/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/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$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/rational[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)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32/proofs[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples/compilation/ag32[0m
Scanned 87 directories
Starting work on helloProofTheory
Starting work on sortProofTheory
Starting work on wordcountProofTheory
wordcountProofTheory                                                                                                            (45s)FAIL<1>
 Run out of store - interrupting threads
 error in quse /home/myreen/regression/cakeml-2297/examples/wordcountProgTheory.sml : Interrupt
 error in load $(CAKEMLDIR)/examples/wordcountProgTheory : Interrupt
 error in load /home/myreen/regression/cakeml-2297/examples/compilation/ag32/proofs/wordcountProofScript : Interrupt
 Uncaught exception: Interrupt
helloProofTheory                                                                                                                (43s)MKILLED
sortProofTheory                                                                                                                 (44s)MKILLED