Job 1661

CakeML:3ae2206f776be03e2aeacd6d2f059c2a98cfb630
  Fix some more proofs [Nov 24 10:03:55]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
  emacs-mode: adjust holmake command to get to use ANSI magic [Nov 23 06:58:28]
Machine:oven3 4.19.67.1.amd64-smp

Nov 24 10:25:04 Claimed job
Nov 24 10:25:07 Reusing HOL
Nov 24 10:25:58 Starting developers
Nov 24 10:26:06 Finished developers                                               7s  98MB
Nov 24 10:26:06 Starting developers/bin
Nov 24 10:26:18 Finished developers/bin                                          12s   1GB
Nov 24 10:26:18 Starting semantics/ffi
Nov 24 10:26:38 Finished semantics/ffi                                           19s 256MB
Nov 24 10:26:38 Starting semantics
Nov 24 10:29:27 Finished semantics                                             2m48s   1GB
Nov 24 10:29:27 Starting semantics/proofs
Nov 24 10:37:42 Finished semantics/proofs                                      8m14s   1GB
Nov 24 10:37:42 Starting semantics/alt_semantics
Nov 24 10:38:10 Finished semantics/alt_semantics                                 27s 410MB
Nov 24 10:38:10 Starting semantics/alt_semantics/proofs
Nov 24 10:43:24 Finished semantics/alt_semantics/proofs                        5m13s   1GB
Nov 24 10:43:24 Starting basis/pure
Nov 24 10:49:36 Finished basis/pure                                            6m12s 887MB
Nov 24 10:49:36 Starting translator
Nov 24 10:55:30 Finished translator                                            5m53s   1GB
Nov 24 10:55:30 Starting compiler/parsing
Nov 24 10:58:09 Finished compiler/parsing                                      2m38s   2GB
Nov 24 10:58:09 Starting characteristic
Nov 24 11:10:09 Finished characteristic                                       11m59s   2GB
Nov 24 11:10:09 Starting translator/monadic
Nov 24 11:13:46 Finished translator/monadic                                    3m36s   1GB
Nov 24 11:13:46 Starting basis
Nov 24 12:51:46 Finished basis                                              1h37m59s  15GB
Nov 24 12:51:46 Starting compiler/inference
Nov 24 12:54:29 Finished compiler/inference                                    2m42s   1GB
Nov 24 12:54:29 Starting compiler/backend/reg_alloc
Nov 24 12:56:40 Finished compiler/backend/reg_alloc                            2m11s   1GB
Nov 24 12:56:41 Starting compiler/backend/gc
Nov 24 13:03:26 Finished compiler/backend/gc                                   6m45s   2GB
Nov 24 13:03:26 Starting compiler/backend
Nov 24 13:11:44 Finished compiler/backend                                      8m17s   2GB
Nov 24 13:11:44 Starting compiler/encoders/asm
Nov 24 13:12:34 Finished compiler/encoders/asm                                   49s 698MB
Nov 24 13:12:34 Starting compiler/encoders/x64
Nov 24 13:14:51 Finished compiler/encoders/x64                                 2m16s   1GB
Nov 24 13:14:51 Starting compiler/encoders/arm7
Nov 24 13:19:19 Finished compiler/encoders/arm7                                4m27s   1GB
Nov 24 13:19:19 Starting compiler/encoders/arm8
Nov 24 13:20:48 Finished compiler/encoders/arm8                                1m28s 944MB
Nov 24 13:20:48 Starting compiler/encoders/mips
Nov 24 13:24:02 Finished compiler/encoders/mips                                3m14s 845MB
Nov 24 13:24:03 Starting compiler/encoders/riscv
Nov 24 13:27:47 Finished compiler/encoders/riscv                               3m43s 971MB
Nov 24 13:27:47 Starting compiler/encoders/ag32
Nov 24 13:28:28 Finished compiler/encoders/ag32                                  40s 695MB
Nov 24 13:28:28 Starting compiler/backend/x64
Nov 24 13:29:10 Finished compiler/backend/x64                                    41s   1GB
Nov 24 13:29:10 Starting compiler/backend/arm7
Nov 24 13:29:57 Finished compiler/backend/arm7                                   46s   1GB
Nov 24 13:29:57 Starting compiler/backend/arm8
Nov 24 13:30:38 Finished compiler/backend/arm8                                   40s   1GB
Nov 24 13:30:38 Starting compiler/backend/mips
Nov 24 13:31:21 Finished compiler/backend/mips                                   42s   1GB
Nov 24 13:31:21 Starting compiler/backend/riscv
Nov 24 13:32:04 Finished compiler/backend/riscv                                  42s   1GB
Nov 24 13:32:04 Starting compiler/backend/ag32
Nov 24 13:34:33 Finished compiler/backend/ag32                                 2m28s   1GB
Nov 24 13:34:34 Starting compiler/parsing/proofs
Nov 24 13:37:49 FAILED: compiler/parsing/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/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/quotient/src[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)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Starting work on README.md
Starting work on cmlNTPropsTheory
Starting work on pegSoundTheory
README.md                                                                                                                                                                                                                        (0s)     OK
cmlNTPropsTheory                                                                                                                                                                                                                (27s)     OK
pegSoundTheory                                                                                                                                                                                                                 (168s)     OK
Starting work on pegCompleteTheory
pegCompleteTheory                                                                                                                                                                                                               (19s)FAIL<1>
     ptree_head spt' = SEP  valid_lptree G cpt'  ptree_head cpt' = C 
     real_fringe cpt'  real_fringe spt'  real_fringe ppt' =
     MAP (TOK ## I) (pf  sf  cf) 
     leftLoc (ptree_loc cpt') = leftLoc (ptree_loc ppt) 
     rightLoc (ptree_loc ppt') = rightLoc (ptree_loc cpt) 
     mkNd P [ppt; spt; cpt] = left_insert ppt' P spt' cpt'
 
 failed.
 Failed to prove theorem lassoc_reassociated.
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}