Job 2741

CakeML:f58b9e5503eabc896d460c81c92571a9f7029080
  Remove temp_overload_on [Dec 09 08:22:52]
#1110 (efficient-cases-peg)
Merging into:515c45c629ea3bc53e91514be13688eb4041e0c0
  Merge pull request #1107 from CakeML/noneq-refs [Dec 09 05:39:51]
HOL:429df142120f03f0e1e3dcae1ec14dd20d66d9dd
  Tweak Holmake docs; include new features from 629d43fd28ac8 [Dec 06 04:03:59]
Machine:pavlova

Dec 09 14:22:55 Claimed job
Dec 09 14:23:02 Building HOL
Dec 09 14:34:01 Starting developers
Dec 09 14:34:05 Finished developers                                               2s 117MB
Dec 09 14:34:06 Starting developers/bin
Dec 09 14:34:12 Finished developers/bin                                           5s 746MB
Dec 09 14:34:13 Starting compiler/proofs
Dec 09 16:16:02 Finished compiler/proofs                                    1h41m48s  37GB
Dec 09 16:16:03 Starting compiler/bootstrap/translation
Dec 09 22:10:42 Finished compiler/bootstrap/translation                     5h54m38s  83GB
Dec 09 22:10:43 Starting semantics/ffi
Dec 09 22:10:53 Finished semantics/ffi                                            8s 611MB
Dec 09 22:10:54 Starting semantics
Dec 09 22:10:55 Finished semantics                                                0s  53MB
Dec 09 22:10:56 Starting semantics/proofs
Dec 09 22:11:28 FAILED: semantics/proofs
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanned 18 directories
Starting work on README.md
Starting work on cmlPtreeConversionPropsTheory
README.md                                                           (0s)     OK
cmlPtreeConversionPropsTheory                                      (28s)FAIL<1>
 Saved theorem _______ "type_to_AST_injection"
 Saved theorem _______ "ptree_Type_surjection"
 Saved theorem _______ "ptree_head_TOK"
 Saved theorem _______ "UQTyOp_OK"
 Saved theorem _______ "TyOp_OK"
 Saved theorem _______ "TyvarN_OK"
 Saved theorem _______ "TyVarList_OK"
 Saved theorem _______ "TypeName_OK"
 Saved theorem _______ "tuplify_OK"
 Saved theorem _______ "Type_OK0"
 Saved theorem _______ "Type_OK"
 Saved theorem _______ "V_OK"
 Saved theorem _______ "FQV_OK"
 Saved theorem _______ "UQConstructorName_OK"
 Saved theorem _______ "ConstructorName_OK"
 Saved theorem _______ "Ops_OK0"
 Proved triviality ___ "MAP_TK11"
 Saved theorem _______ "OpID_OK"
 Saved theorem _______ "Pattern_OK0"
 Saved theorem _______ "Pattern_OK"
 Saved theorem _______ "Eseq_encode_OK"
 Saved theorem _______ "PbaseList1_OK"
 Saved theorem _______ "Eliteral_OK"
 The E_OK proof takes a while
 Proof of 
 
 valid_ptree cmlG pt  MAP TK toks = ptree_fringe pt 
 (N 
  {nE; nE'; nEhandle; nElogicOR; nElogicAND; nEtuple; nEmult; nEadd; nElistop;
   nErel; nEcomp; nEbefore; nEtyped; nEapp; nEbase}  ptree_head pt = NN N 
  t. ptree_Expr N pt = SOME t) 
 (ptree_head pt = NN nEseq  el. ptree_Eseq pt = SOME el  el  []) 
 (ptree_head pt = NN nPEs  pes. ptree_PEs pt = SOME pes) 
 (ptree_head pt = NN nElist2  el. ptree_Exprlist nElist2 pt = SOME el) 
 (ptree_head pt = NN nElist1  el. ptree_Exprlist nElist1 pt = SOME el) 
 (ptree_head pt = NN nLetDecs  lds. ptree_LetDecs pt = SOME lds) 
 (ptree_head pt = NN nPE  pe. ptree_PE pt = SOME pe) 
 (ptree_head pt = NN nPE'  pe. ptree_PE' pt = SOME pe) 
 (ptree_head pt = NN nLetDec  ld. ptree_LetDec pt = SOME ld) 
 (ptree_head pt = NN nAndFDecls  fds. ptree_AndFDecls pt = SOME fds) 
 (ptree_head pt = NN nFDecl  fd. ptree_FDecl pt = SOME fd)
 
 failed.
 Failed to prove theorem E_OK0.
 
 Exception raised at Tactic.MATCH_MP_TAC:
 No match
 error in quse /scratch/cakeml/regression/cakeml-2741/semantics/proofs/cmlPtreeConversionPropsScript.sml : HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2741/semantics/proofs/cmlPtreeConversionPropsScript : HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-429df142120f03f0e1e3dcae1ec14dd20d66d9dd/src/prekernel/Feedback.sml:124: HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic", source_location = Loc_Unknown}