Overview

Job 1661

CakeML:3ae2206f776be03e2aeacd6d2f059c2a98cfb630
  Fix some more proofs
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
  emacs-mode: adjust holmake command to get to use ANSI magic
Machine:oven3 4.19.67.1.amd64-smp

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               7s  98MB
 Starting developers/bin
 Finished developers/bin                                          12s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           19s 256MB
 Starting semantics
 Finished semantics                                             2m48s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      8m14s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 27s 410MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        5m13s   1GB
 Starting basis/pure
 Finished basis/pure                                            6m12s 887MB
 Starting translator
 Finished translator                                            5m53s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m38s   2GB
 Starting characteristic
 Finished characteristic                                       11m59s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m36s   1GB
 Starting basis
 Finished basis                                              1h37m59s  15GB
 Starting compiler/inference
 Finished compiler/inference                                    2m42s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            2m11s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   6m45s   2GB
 Starting compiler/backend
 Finished compiler/backend                                      8m17s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   49s 698MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 2m16s   1GB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                4m27s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                1m28s 944MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                3m14s 845MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               3m43s 971MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  40s 695MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    41s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   46s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   40s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   42s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  42s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 2m28s   1GB
 Starting compiler/parsing/proofs
 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"}