Job 1647

CakeML:fa6347ccf4c2e176933b407c71eac896b5d74295
  Add missing case [Nov 20 15:50:38]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:bbc4316ab6255e29628563000a9b6b171290f1be
  Fix congruence code (from acd5d8650) to also work with non-equalities [Nov 18 00:28:52]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 20 23:33:29 Claimed job
Nov 20 23:33:40 Building HOL
Nov 20 23:43:01 Starting developers
Nov 20 23:43:06 Finished developers                                               4s 142MB
Nov 20 23:43:06 Starting developers/bin
Nov 20 23:43:13 Finished developers/bin                                           6s   1GB
Nov 20 23:43:13 Starting semantics/ffi
Nov 20 23:43:24 Finished semantics/ffi                                           11s 232MB
Nov 20 23:43:24 Starting semantics
Nov 20 23:44:57 Finished semantics                                             1m32s   1GB
Nov 20 23:44:57 Starting semantics/proofs
Nov 20 23:47:49 FAILED: semantics/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$(CAKEMLDIR)/developers[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)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Starting work on NTpropertiesTheory
Starting work on pegTheory
Starting work on README.md
Starting work on astPropsTheory
README.md                                                                                 semantics/proofs  (0s)     OK
Starting work on namespacePropsTheory
NTpropertiesTheory                                                  examples/formal-languages/context-free  (4s)     OK
Starting work on gramPropsTheory
pegTheory                                                           examples/formal-languages/context-free  (6s)     OK
Starting work on pegexecTheory
astPropsTheory                                                                            semantics/proofs  (7s)     OK
pegexecTheory                                                       examples/formal-languages/context-free  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 3]                                      (13.471s) 
Finished $(CAKEMLDIR)/misc                                                                                     (0.000s) 
namespacePropsTheory                                                                      semantics/proofs (11s)     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                                                                 semantics/proofs  (6s)     OK
gramPropsTheory                                                                           semantics/proofs (21s)     OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                                                             semantics/proofs (28s)     OK
semanticPrimitivesPropsTheory                                                             semantics/proofs (47s)     OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
typeSysPropsTheory                                                                        semantics/proofs (26s)     OK
Starting work on primSemEnvTheory
Starting work on weakeningTheory
evaluatePropsTheory                                                                       semantics/proofs (35s)     OK
weakeningTheory                                                                           semantics/proofs (10s)     OK
primSemEnvTheory                                                                          semantics/proofs (11s)     OK
Starting work on typeSoundTheory
typeSoundTheory                                                                           semantics/proofs (68s)FAIL<1>
     tbindings 
   pmatch_list cenv st ps vs bindings = No_match 
   bindings'.
     pmatch_list cenv st ps vs bindings = Match bindings' 
     LIST_REL ((x,v) (x',t). x = x'  type_v tvs ctMap tenvS v t) bindings'
       (new_tbindings ++ tbindings)
 
 failed.
 Failed to prove theorem pat_type_sound.
 Uncaught exception: HOL_ERR {message = "goal completely solved by first tactic (THEN1 on line 1192) (THEN1 on line 1186) (THEN1 on line 1195) (THEN1 on line 1199) (THEN1 on line 1200) (THEN1 on line 1201) (THEN1 on line 1202) (THEN1 on line 1203) (THEN1 on line 1204) (THEN1 on line 1205) (THEN1 on line 1206) (THEN1 on line 1207) (THEN1 on line 1208) (THEN1 on line 1209) (THEN1 on line 1210) (THEN1 on line 1211) (THEN1 on line 1212) (THEN1 on line 1213) (THEN1 on line 1214) (THEN1 on line 1215) (THEN1 on line 1216) (THEN1 on line 1217) (THEN1 on line 1218) (THEN1 on line 1219) (THEN1 on line 1220) (THEN1 on line 1235) (THEN1 on line 1236)", origin_function = "THEN1", origin_structure = "Tactical"}