Job 2851

CakeML:2a9deab6e91db380747768935512d60a84818734
  letrec progress/validity [May 31 01:26:21]
#1183 (scheme)
Merging into:e1650fc504837c0fbd3931cc5066914ffdc9d877
  Merge pull request #1184 from CakeML/bnn_checker [May 30 18:07:55]
HOL:8103ca8222144bafcc066e6482fa3e6eb59d97c9
  repairing termination proofs [Jun 02 08:30:13]
Machine:pavlova

Jun 03 08:07:51 Claimed job
Jun 03 08:08:01 Building HOL
Jun 03 08:18:51 Starting developers
Jun 03 08:18:55 Finished developers                                               3s 214MB
Jun 03 08:18:56 Starting developers/bin
Jun 03 08:19:02 Finished developers/bin                                           4s 591MB
Jun 03 08:19:03 Starting misc
Jun 03 08:19:35 FAILED: misc
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 $(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)/developers
Scanned 15 directories
Starting work on locationTheory
Starting work on lprefix_lubTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory                   examples/machine-code/hoare-triple  (0s)     OK
Starting work on README.md
README.md                                                     misc  (0s)     OK
locationTheory              examples/formal-languages/context-free  (1s)     OK
Starting work on grammarTheory
lprefix_lubTheory                  examples/fun-op-sem/lprefix_lub  (3s)     OK
Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1]      (3.740s) 
grammarTheory               examples/formal-languages/context-free  (2s)     OK
Starting work on pegTheory
set_sepTheory                   examples/machine-code/hoare-triple  (4s)     OK
Starting work on progTheory
progTheory                      examples/machine-code/hoare-triple  (2s)     OK
Starting work on addressTheory
pegTheory                   examples/formal-languages/context-free  (5s)     OK
Starting work on pegexecTheory
pegexecTheory               examples/formal-languages/context-free  (2s)     OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 4] (12.070s) 
addressTheory                   examples/machine-code/hoare-triple  (6s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4]  (14.460s) 
Starting work on miscTheory
miscTheory                                                    misc (12s)FAIL<1>
 Saved theorem _______ "ALOOKUP_ZIP_FAIL"
 Saved theorem _______ "MEM_ALOOKUP"
 Saved definition ____ "anub_def"
 Saved induction _____ "anub_ind"
 Saved theorem _______ "EVERY_anub_imp"
 Saved theorem _______ "ALOOKUP_anub"
 Saved theorem _______ "anub_eq_nil"
 Saved theorem _______ "EVERY_anub_suff"
 Saved theorem _______ "anub_notin_acc"
 Saved theorem _______ "anub_tl_anub"
 Saved theorem _______ "anub_all_distinct_keys"
 Saved theorem _______ "MEM_anub_ALOOKUP"
 Saved theorem _______ "toAList_domain"
 Saved theorem _______ "domain_nat_set_from_list"
 Saved theorem _______ "wf_nat_set_from_list"
 Saved theorem _______ "BIT_11"
 Saved theorem _______ "BIT_11_2"
 Saved theorem _______ "LOG2_TIMES2"
 Saved theorem _______ "LOG2_TIMES2_1"
 Saved theorem _______ "C_BIT_11"
 Saved theorem _______ "BIT_num_from_bin_list_leading"
 Saved definition ____ "least_from_def"
 Saved theorem _______ "LEAST_thm"
 Saved theorem _______ "least_from_thm"
 Saved theorem _______ "FUNPOW_mono"
 Saved theorem _______ "FUNPOW_SUC_PLUS"
 Saved theorem _______ "OPTREL_trans"
 Saved definition ____ "UPDATE_LIST_def"
 Saved theorem _______ "UPDATE_LIST_THM"
 Saved theorem _______ "APPLY_UPDATE_LIST_ALOOKUP"
 Saved definition ____ "find_index_def"
 Saved theorem _______ "INDEX_FIND_CONS_EQ_SOME"
 Saved theorem _______ "find_index_INDEX_FIND"
 Saved theorem _______ "find_index_INDEX_OF"
 Proof of 
 
 ls x n. MEM x ls  find_index x ls n = NONE
 
 failed.
 First unsolved sub-goal is
 
 x  h  MEM x ls  h  x  find_index x ls (n + 1) = NONE
 
 Failed to prove theorem find_index_NOT_MEM.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /scratch/cakeml/regression/cakeml-2851/misc/miscScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2851/misc/miscScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-8103ca8222144bafcc066e6482fa3e6eb59d97c9/src/prekernel/Feedback.sml:124: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}