Job 995

CakeML:a4b9895e8b03fd5585edd4e7028cc2bd8ec02b73
  Retire bootstrap-translation steps for clos_labels [Aug 12 09:41:31]
#677 (clos-install)
Merging into:980410c6c89921c2e8950a5127bd9f32791f50bf
  Fix more def_compte issues [Aug 05 04:31:17]
HOL:c4ffdebc24abcae15e664f9603d3f5ce699cfaed
  Fix proof broken by change to drule in 812a08a5a8 [Aug 11 09:47:03]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 12 12:30:00 Claimed job
Aug 12 12:30:04 Reusing HOL
Aug 12 12:30:51 Starting developers
Aug 12 12:30:53 Finished developers                                               2s  20MB
Aug 12 12:30:53 Starting developers/bin
Aug 12 12:31:00 Finished developers/bin                                           6s 960MB
Aug 12 12:31:00 Starting semantics/ffi
Aug 12 12:31:10 Finished semantics/ffi                                            9s 210MB
Aug 12 12:31:10 Starting semantics
Aug 12 12:32:31 Finished semantics                                             1m20s   1GB
Aug 12 12:32:31 Starting semantics/proofs
Aug 12 12:33:21 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-995/developers]0;Holmake: ~/oven/regression/cakeml-995/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-995/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-995/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-995/misc]0;Holmake: ~/oven/regression/cakeml-995/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-995/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-995/misc]0;Holmake: ~/oven/regression/cakeml-995/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