CakeML:6055fa5cdc1832bbfd06a2a93e9d023f1d1d4050
Make a note of `as` patterns in how-to document
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
Merge pull request #842 from CakeML/ramsey
HOL:bdb437dfa109a22361c4d539c736d12e5828dbb8
Add two utility shell scripts to developers
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 163MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 240MB
Starting semantics
Finished semantics 1m24s 1GB
Starting semantics/proofs
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
Finished $(CAKEMLDIR)/misc (0.000s)
Starting work on README.md
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on namespacePropsTheory
README.md semantics/proofs (0s) OK
astPropsTheory semantics/proofs (6s) OK
namespacePropsTheory semantics/proofs (11s) OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory semantics/proofs (6s) OK
gramPropsTheory semantics/proofs (20s) OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory semantics/proofs (27s) 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 (12s) 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"}