Job 2332

CakeML:e61fd9aa6cacf38d710f03a1e062c6b261bd37fc
  update a few more installed in examples/ for shared memory [Mar 11 04:49:36]
#977 (share_mem_new2)
Merging into:98d0d03c9e52b27a9895186563d385583deb75a2
  Merge pull request #984 from CakeML/compression [Mar 10 14:36:06]
HOL:772a64a23fab01445886a113b810bd3c02930e63
  Tweak tailrecLib to allow function terms that are composite [Mar 04 00:41:36]
Machine:pavlova

Mar 11 08:02:00 Claimed job
Mar 11 08:02:05 Reusing HOL
Mar 11 08:02:14 Starting developers
Mar 11 08:02:18 Finished developers                                               2s 220MB
Mar 11 08:02:19 Starting developers/bin
Mar 11 08:02:48 Finished developers/bin                                          27s   1GB
Mar 11 08:02:49 Starting compiler/proofs
Mar 11 09:53:21 Finished compiler/proofs                                    1h50m31s  35GB
Mar 11 09:53:22 Starting compiler/bootstrap/translation
Mar 11 17:55:49 Finished compiler/bootstrap/translation                     8h02m26s  74GB
Mar 11 17:55:50 Starting semantics/ffi
Mar 11 17:55:58 Finished semantics/ffi                                            7s 575MB
Mar 11 17:55:59 Starting semantics
Mar 11 17:56:00 Finished semantics                                                0s  66MB
Mar 11 17:56:01 Starting semantics/proofs
Mar 11 17:56:35 Finished semantics/proofs                                        33s   1GB
Mar 11 17:56:36 Starting semantics/alt_semantics
Mar 11 17:57:15 Finished semantics/alt_semantics                                 37s   1GB
Mar 11 17:57:16 Starting semantics/alt_semantics/proofs
Mar 11 18:08:10 Finished semantics/alt_semantics/proofs                       10m52s   4GB
Mar 11 18:08:10 Starting basis/pure
Mar 11 18:08:12 Finished basis/pure                                               0s  69MB
Mar 11 18:08:13 Starting translator
Mar 11 18:09:55 Finished translator                                            1m41s   3GB
Mar 11 18:09:55 Starting compiler/parsing
Mar 11 18:09:57 Finished compiler/parsing                                         0s  67MB
Mar 11 18:09:58 Starting characteristic
Mar 11 18:09:59 Finished characteristic                                           0s  88MB
Mar 11 18:10:00 Starting translator/monadic
Mar 11 18:10:02 Finished translator/monadic                                       0s  91MB
Mar 11 18:10:03 Starting basis
Mar 11 18:13:41 Finished basis                                                 3m37s   4GB
Mar 11 18:13:42 Starting compiler/inference
Mar 11 18:13:44 Finished compiler/inference                                       0s  81MB
Mar 11 18:13:45 Starting compiler/backend/reg_alloc
Mar 11 18:13:46 Finished compiler/backend/reg_alloc                               0s  67MB
Mar 11 18:13:47 Starting compiler/backend/gc
Mar 11 18:13:49 Finished compiler/backend/gc                                      0s 141MB
Mar 11 18:13:49 Starting compiler/backend
Mar 11 18:14:07 Finished compiler/backend                                        16s   1GB
Mar 11 18:14:08 Starting compiler/encoders/asm
Mar 11 18:14:09 Finished compiler/encoders/asm                                    0s  92MB
Mar 11 18:14:10 Starting compiler/encoders/x64
Mar 11 18:14:11 Finished compiler/encoders/x64                                    0s  94MB
Mar 11 18:14:12 Starting compiler/encoders/arm7
Mar 11 18:14:14 Finished compiler/encoders/arm7                                   0s  93MB
Mar 11 18:14:15 Starting compiler/encoders/arm8
Mar 11 18:14:16 Finished compiler/encoders/arm8                                   0s  93MB
Mar 11 18:14:17 Starting compiler/encoders/arm8_asl
Mar 11 18:16:34 Finished compiler/encoders/arm8_asl                            2m16s   1GB
Mar 11 18:16:35 Starting compiler/encoders/mips
Mar 11 18:16:37 Finished compiler/encoders/mips                                   0s  93MB
Mar 11 18:16:38 Starting compiler/encoders/riscv
Mar 11 18:16:39 Finished compiler/encoders/riscv                                  0s  94MB
Mar 11 18:16:40 Starting compiler/encoders/ag32
Mar 11 18:16:41 Finished compiler/encoders/ag32                                   0s  92MB
Mar 11 18:16:42 Starting compiler/backend/x64
Mar 11 18:16:44 Finished compiler/backend/x64                                     0s 130MB
Mar 11 18:16:45 Starting compiler/backend/arm7
Mar 11 18:16:47 Finished compiler/backend/arm7                                    0s 126MB
Mar 11 18:16:48 Starting compiler/backend/arm8
Mar 11 18:16:49 Finished compiler/backend/arm8                                    0s 126MB
Mar 11 18:16:50 Starting compiler/backend/mips
Mar 11 18:16:52 Finished compiler/backend/mips                                    0s 126MB
Mar 11 18:16:53 Starting compiler/backend/riscv
Mar 11 18:16:55 Finished compiler/backend/riscv                                   0s 126MB
Mar 11 18:16:55 Starting compiler/backend/ag32
Mar 11 18:18:15 Finished compiler/backend/ag32                                 1m18s   3GB
Mar 11 18:18:16 Starting compiler/parsing/proofs
Mar 11 18:18:17 Finished compiler/parsing/proofs                                  0s  78MB
Mar 11 18:18:18 Starting compiler/inference/proofs
Mar 11 18:18:20 Finished compiler/inference/proofs                                0s  89MB
Mar 11 18:18:20 Starting compiler/backend/semantics
Mar 11 18:22:07 Finished compiler/backend/semantics                            3m45s   2GB
Mar 11 18:22:08 Starting compiler/backend/reg_alloc/proofs
Mar 11 18:22:09 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Mar 11 18:22:10 Starting compiler/backend/proofs
Mar 11 18:23:15 Finished compiler/backend/proofs                               1m04s   5GB
Mar 11 18:23:16 Starting compiler/backend/serialiser
Mar 11 18:23:18 Finished compiler/backend/serialiser                              1s 193MB
Mar 11 18:23:19 Starting compiler/encoders/x64/proofs
Mar 11 18:32:47 Finished compiler/encoders/x64/proofs                          9m27s   5GB
Mar 11 18:32:48 Starting compiler/encoders/arm7/proofs
Mar 11 18:45:40 Finished compiler/encoders/arm7/proofs                        12m50s  11GB
Mar 11 18:45:40 Starting compiler/encoders/arm8/proofs
Mar 11 18:52:07 Finished compiler/encoders/arm8/proofs                         6m25s   6GB
Mar 11 18:52:08 Starting compiler/encoders/arm8_asl/proofs
Mar 11 19:05:55 Finished compiler/encoders/arm8_asl/proofs                    13m45s   4GB
Mar 11 19:05:55 Starting compiler/encoders/mips/proofs
Mar 11 19:15:58 Finished compiler/encoders/mips/proofs                        10m02s   6GB
Mar 11 19:15:59 Starting compiler/encoders/riscv/proofs
Mar 11 19:24:29 Finished compiler/encoders/riscv/proofs                        8m28s   5GB
Mar 11 19:24:30 Starting compiler/encoders/ag32/proofs
Mar 11 19:26:51 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Mar 11 19:26:52 Starting compiler/backend/x64/proofs
Mar 11 19:27:35 Finished compiler/backend/x64/proofs                             41s   3GB
Mar 11 19:27:36 Starting compiler/backend/arm7/proofs
Mar 11 19:28:21 Finished compiler/backend/arm7/proofs                            44s   2GB
Mar 11 19:28:22 Starting compiler/backend/arm8/proofs
Mar 11 19:29:03 Finished compiler/backend/arm8/proofs                            40s   3GB
Mar 11 19:29:04 Starting compiler/backend/arm8_asl
Mar 11 19:29:33 Finished compiler/backend/arm8_asl                               28s   2GB
Mar 11 19:29:34 Starting compiler/backend/mips/proofs
Mar 11 19:30:18 Finished compiler/backend/mips/proofs                            42s   3GB
Mar 11 19:30:19 Starting compiler/backend/riscv/proofs
Mar 11 19:31:08 Finished compiler/backend/riscv/proofs                           48s   4GB
Mar 11 19:31:09 Starting compiler/backend/ag32/proofs
Mar 11 19:45:01 Finished compiler/backend/ag32/proofs                         13m51s   6GB
Mar 11 19:45:01 Starting candle/set-theory
Mar 11 19:45:46 Finished candle/set-theory                                       43s   1GB
Mar 11 19:45:47 Starting candle/syntax-lib
Mar 11 19:45:48 Finished candle/syntax-lib                                        0s  75MB
Mar 11 19:45:49 Starting candle/standard/syntax
Mar 11 19:46:04 Finished candle/standard/syntax                                  14s   1GB
Mar 11 19:46:05 Starting candle/standard/semantics
Mar 11 19:48:29 Finished candle/standard/semantics                             2m23s   2GB
Mar 11 19:48:30 Starting candle/standard/monadic
Mar 11 19:48:31 Finished candle/standard/monadic                                  0s  96MB
Mar 11 19:48:32 Starting candle/standard/ml_kernel
Mar 11 19:50:22 Finished candle/standard/ml_kernel                             1m49s   6GB
Mar 11 19:50:23 Starting candle/overloading/syntax
Mar 11 19:53:47 Finished candle/overloading/syntax                             3m23s   1GB
Mar 11 19:53:48 Starting candle/overloading/semantics
Mar 11 20:05:00 Finished candle/overloading/semantics                         11m10s   4GB
Mar 11 20:05:01 Starting candle/overloading/monadic
Mar 11 20:07:33 Finished candle/overloading/monadic                            2m31s   3GB
Mar 11 20:07:34 Starting candle/overloading/ml_kernel
Mar 11 20:15:06 Finished candle/overloading/ml_kernel                          7m30s   6GB
Mar 11 20:15:07 Starting candle/overloading/ml_checker
Mar 11 20:17:39 Finished candle/overloading/ml_checker                         2m31s   7GB
Mar 11 20:17:40 Starting candle/prover
Mar 11 20:27:35 Finished candle/prover                                         9m53s   5GB
Mar 11 20:27:36 Starting pancake
Mar 11 20:28:35 Finished pancake                                                 57s   1GB
Mar 11 20:28:36 Starting pancake/ffi
Mar 11 20:28:36 Finished pancake/ffi                                              0s  20MB
Mar 11 20:28:37 Starting pancake/semantics
Mar 11 20:31:20 Finished pancake/semantics                                     2m42s   2GB
Mar 11 20:31:21 Starting pancake/parser
Mar 11 20:31:48 Finished pancake/parser                                          25s   2GB
Mar 11 20:31:49 Starting pancake/proofs
Mar 11 21:02:31 Finished pancake/proofs                                       30m41s   9GB
Mar 11 21:02:32 Starting characteristic/examples
Mar 11 21:04:09 Finished characteristic/examples                               1m36s   5GB
Mar 11 21:04:10 Starting tutorial/solutions
Mar 11 21:20:14 Finished tutorial/solutions                                   16m02s  11GB
Mar 11 21:20:15 Starting translator/monadic/examples
Mar 11 21:24:02 Finished translator/monadic/examples                           3m46s   4GB
Mar 11 21:24:03 Starting examples
Mar 11 21:38:25 Finished examples                                             14m21s   7GB
Mar 11 21:38:26 Starting examples/compilation/x64
Mar 11 23:36:22 Finished examples/compilation/x64                           1h57m54s  26GB
Mar 11 23:36:23 Starting examples/compilation/x64/proofs
Mar 11 23:40:13 Finished examples/compilation/x64/proofs                       3m49s   6GB
Mar 11 23:40:14 Starting examples/compilation/ag32
Mar 12 00:09:59 Finished examples/compilation/ag32                            29m44s  13GB
Mar 12 00:10:00 Starting examples/compilation/ag32/proofs
Mar 12 00:11:20 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 README.md
Starting work on helloProofTheory
Starting work on sortProofTheory
Starting work on wordcountProofTheory
README.md                                                           (0s)     OK
wordcountProofTheory                                               (69s)FAIL<1>
   (FUNPOW Next (wordcount_startup_clock ms0 inp cl) ms0)
 
 failed.
 Failed to prove theorem wordcount_installed.
 
 Exception raised at Tactic.MATCH_MP_TAC:
 No match (THEN1 on line 134)
 error in quse /scratch/cakeml/regression/cakeml-2332/examples/compilation/ag32/proofs/wordcountProofScript.sml : HOL_ERR {message = "No match (THEN1 on line 134)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 error in load /scratch/cakeml/regression/cakeml-2332/examples/compilation/ag32/proofs/wordcountProofScript : HOL_ERR {message = "No match (THEN1 on line 134)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 134)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
helloProofTheory                                                   (68s)MKILLED
sortProofTheory                                                    (69s)MKILLED