Job 2871

CakeML:2a9deab6e91db380747768935512d60a84818734
  letrec progress/validity [May 31 01:26:21]
#1183 (scheme)
Merging into:b378040fc02c949ecd0a24ced798201a572514a4
  Merge pull request #1186 from CakeML/mcandidate-fix [Jun 16 00:47:48]
HOL:98d19aa7937d0d22a22b0a6dc34d08f94e0a7464
  Apply a fix suggested by Yong Kiam [Jun 24 05:53:03]
Machine:lammmington

Jun 24 17:39:23 Claimed job
Jun 24 17:39:30 Building HOL
Jun 24 17:50:16 Starting developers
Jun 24 17:50:20 Finished developers                                               3s 220MB
Jun 24 17:50:21 Starting developers/bin
Jun 24 17:50:27 Finished developers/bin                                           4s 592MB
Jun 24 17:50:28 Starting misc
Jun 24 17:51:06 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.650s) 
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  (3s)     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.320s) 
addressTheory                   examples/machine-code/hoare-triple  (6s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4]  (14.220s) 
Starting work on miscTheory
miscTheory                                                    misc (19s)FAIL<1>
 Saved theorem _______ "irreflexive_inv_image"
 Saved theorem _______ "trichotomous_inv_image"
 Saved theorem _______ "MEM_REPLICATE_IMP"
 Saved theorem _______ "plus_0_I"
 Saved theorem _______ "SUM_COUNT_LIST"
 Saved theorem _______ "OPTION_MAP_I"
 Saved theorem _______ "OPTION_MAP_INJ"
 Saved theorem _______ "the_OPTION_MAP"
 Saved theorem _______ "TAKE_FLAT_REPLICATE_LEQ"
 Saved theorem _______ "MOD_2EXP_0_EVEN"
 Saved theorem _______ "ADD_MOD_EQ_LEMMA"
 Saved definition ____ "list_subset_def"
 Saved definition ____ "list_set_eq_def"
 Saved theorem _______ "list_subset_LENGTH"
 Saved theorem _______ "BIJ_UPDATE"
 Saved theorem _______ "INJ_UPDATE"
 Saved theorem _______ "subspt_domain_SUBSET"
 Saved theorem _______ "SPLITP_TAKE_DROP"
 Saved theorem _______ "SND_SPLITP_DROP"
 Saved theorem _______ "FST_SPLITP_DROP"
 Saved theorem _______ "TAKE_DROP_SUBLIST"
 Saved definition ____ "Lnext_def"
 Saved induction _____ "Lnext_ind"
 Saved definition ____ "Lnext_pos_def"
 Saved theorem _______ "OPTION_CHOICE_EQUALS_OPTION"
 Saved theorem _______ "option_eq_some"
 Saved theorem _______ "ALL_DISTINCT_alist_to_fmap_REVERSE"
 Saved theorem _______ "FUPDATE_LIST_alist_to_fmap"
 Saved theorem _______ "DISTINCT_FUPDATE_LIST_UNION"
 Saved theorem _______ "fevery_to_drestrict"
 Saved theorem _______ "SUM_MAP_K"
 Saved theorem _______ "LAST_FLAT"
 Saved theorem _______ "TOKENS_unchanged"
 Proof of 
 
 EVERY (EVERY (y. x  y)) ls  EVERY ($  NULL) ls 
 TOKENS ($= x) (CONCAT (MAP (SNOC x) ls)) = ls
 
 failed.
 First unsolved sub-goal is
 
 F
 
 Failed to prove theorem TOKENS_FLAT_MAP_SNOC.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /scratch/cakeml/regression3/cakeml-2871/misc/miscScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression3/cakeml-2871/misc/miscScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression3/HOL-98d19aa7937d0d22a22b0a6dc34d08f94e0a7464/src/prekernel/Feedback.sml:124: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}