Overview

Job 994

CakeML:980410c6c89921c2e8950a5127bd9f32791f50bf
  Fix more def_compte issues
HOL:c4ffdebc24abcae15e664f9603d3f5ce699cfaed
  Fix proof broken by change to drule in 812a08a5a8
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               2s  20MB
 Starting developers/bin
 Finished developers/bin                                           6s 960MB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 240MB
 Starting semantics
 Finished semantics                                             1m20s   1GB
 Starting semantics/proofs
 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-994/developers]0;Holmake: ~/oven/regression/cakeml-994/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-994/misc]0;Holmake: ~/oven/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-994/misc]0;Holmake: ~/oven/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-994/misc]0;Holmake: ~/oven/regression/cakeml-994/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-994/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-994/misc]0;Holmake: ~/oven/regression/cakeml-994/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../ffi]0;Holmake: ../ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/semantics/proofs
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on namespacePropsTheory
Starting work on README.md
README.md                                                                    OK
astPropsTheory                                                               OK
namespacePropsTheory                                                         OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                                                    OK
gramPropsTheory                                                              OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                                                OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                                       FAILED! <1>
 error in load cmlPtreeConversionPropsScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 702) (THEN1 on line 703) (THEN1 on line 705) (THEN1 on line 708) (THEN1 on line 695) (THEN1 on line 709)", origin_function = "THEN1", origin_structure = "Tactical"}
 Proof of 
 
 valid_ptree cmlG pt  MAP TK toks = ptree_fringe pt 
 (ptree_head pt = NN nDecl  d. ptree_Decl pt = SOME d) 
 (ptree_head pt = NN nDecls  d. ptree_Decls pt = SOME d)
 
 failed.
 Failed to prove theorem Decl_OK.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 702) (THEN1 on line 703) (THEN1 on line 705) (THEN1 on line 708) (THEN1 on line 695) (THEN1 on line 709)", origin_function = "THEN1", origin_structure = "Tactical"}
evaluatePropsTheory                                                    M-KILLED
typeSysPropsTheory                                                     M-KILLED