Job 3130

CakeML:237bf6ea5194bfb28b40c2fe25d26ae17ec19ecb
  Fix some proofs [Jan 12 10:52:11]
#1300 (vname)
Merging into:014fc3e0326aaa062d074ef278f11ec4cc4aec65
  Fix a proof [Jan 12 00:42:18]
HOL:ec2580f47550bf224fbbcb8063c4ece8e08de73c
  Sketch implementation of facility to handle script chunks [Jan 12 05:55:57]
Machine:pavlova

Jan 13 06:29:53 Claimed job
Jan 13 06:29:58 Building HOL
Jan 13 06:41:27 Starting developers
Jan 13 06:41:32 Finished developers                                               4s 227MB
Jan 13 06:41:33 Starting developers/bin
Jan 13 06:41:38 Finished developers/bin                                           3s  91MB
Jan 13 06:41:39 Starting misc
Jan 13 06:42:14 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)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanned 15 directories
Starting work on locationTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
Starting work on lprefix_lubTheory
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/pl-semantics/lprefix_lub  (3s)     OK
Finished $(HOLDIR)/examples/pl-semantics/lprefix_lub [#theories: 1]    (3.210s) 
set_sepTheory                   examples/machine-code/hoare-triple  (3s)     OK
Starting work on progTheory
grammarTheory               examples/formal-languages/context-free  (2s)     OK
Starting work on pegTheory
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.700s) 
addressTheory                   examples/machine-code/hoare-triple  (6s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4]  (13.710s) 
Starting work on miscTheory
miscTheory                                                    misc (16s)FAIL<1>
 Saved theorem _______ "FUN_FMAP_FAPPLY_FEMPTY_FAPPLY"
 Saved theorem _______ "LESS_1"
 Saved theorem _______ "map_fst"
 Saved theorem _______ "map_some_eq"
 Saved theorem _______ "map_some_eq_append"
 Saved theorem _______ "LASTN_LEMMA"
 Saved theorem _______ "LASTN_TL"
 Saved theorem _______ "LASTN_LENGTH_LESS_EQ"
 Saved theorem _______ "LASTN_ALT"
 Saved theorem _______ "LENGTH_LASTN_LESS"
 Saved theorem _______ "MAP_EQ_MAP_IMP"
 Saved theorem _______ "INJ_MAP_EQ_2"
 Saved theorem _______ "LENGTH_EQ_FILTER_FILTER"
 Saved theorem _______ "LIST_REL_MAP_FILTER_NEQ"
 Saved definition ____ "word_list_def"
 Saved definition ____ "word_list_exists_def"
 Saved definition ____ "lookup_vars_def"
 Saved theorem _______ "EVERY_lookup_vars"
 Saved theorem _______ "EVERY_LAST"
 Saved theorem _______ "num_to_hex_string_length_1"
 Saved theorem _______ "num_to_hex_string_length_2"
 Saved theorem _______ "num_from_hex_string_length_2"
 Saved theorem _______ "num_from_hex_string_leading_0"
 Saved theorem _______ "num_from_hex_string_length_2_less_16"
 Saved theorem _______ "num_from_hex_string_num_to_hex_string"
 Saved theorem _______ "MAPi_ID"
 Saved definition ____ "enumerate_def"
 Saved theorem _______ "LENGTH_enumerate"
 Saved theorem _______ "EL_enumerate"
 Saved theorem _______ "MAP_enumerate_MAPi"
 Saved theorem _______ "MAPi_enumerate_MAP"
 Saved theorem _______ "MEM_enumerate"
 Saved theorem _______ "MEM_enumerate_IMP"
 Saved theorem _______ "MAP_FST_enumerate"
 Saved theorem _______ "ALL_DISTINCT_MAP_FST_enumerate"
 Saved theorem _______ "ALOOKUP_enumerate"
 Saved theorem _______ "SUM_MAP_LENGTH_REPLICATE"
 Saved theorem _______ "SUM_MAP_COUNT_LIST"
 Saved theorem _______ "SUM_REPLICATE"
 Saved theorem _______ "SUM_MAP_BOUND"
 Saved theorem _______ "SUM_MOD"
 Proof of 
 
 n MOD k = 0  m MOD k = 0  0 < k  (n  m) MOD k = 0
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at boolSyntax.dest_imp: Failed to prove theorem "MOD_SUB_LEMMA":
 not an "==>"
 Full log: /scratch/cakeml/regression/cakeml-3130/misc/.hol/logs/miscTheory