Job 1265

CakeML:30d1750b37e638af75fbb1f0a438859aef1fee04
  Fix a broken script [Jun 08 17:54:39]
HOL:511e4a42e7cb57caffe27cfa441825baa744d7ec
  Update src for strip_binop change [Jun 13 04:34:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 15 06:00:55 Claimed job
Jun 15 06:01:02 Building HOL
Jun 15 06:15:47 Starting developers
Jun 15 06:15:51 Finished developers                                               4s  94MB
Jun 15 06:15:52 Starting developers/bin
Jun 15 06:15:59 Finished developers/bin                                           7s   1GB
Jun 15 06:16:00 Starting semantics/ffi
Jun 15 06:16:12 Finished semantics/ffi                                           12s 213MB
Jun 15 06:16:12 Starting semantics
Jun 15 06:16:37 FAILED: semantics
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Starting work on grammarTheory
Starting work on lprefix_lubTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory                                   real:    1s  user:    0s     OK
Starting work on lem_list_extraTheory
lprefix_lubTheory                               real:    3s  user:    3s     OK
Starting work on lem_set_extraTheory
grammarTheory                                   real:    3s  user:    3s     OK
Starting work on lem_stringTheory
set_sepTheory                                   real:    4s  user:    3s     OK
Starting work on progTheory
lem_set_extraTheory                             real:    0s  user:    0s     OK
Starting work on lem_string_extraTheory
lem_stringTheory                                real:    0s  user:    0s     OK
Starting work on byteTheory
lem_list_extraTheory                            real:    3s  user:    2s     OK
Starting work on README.md
README.md                                       real:    0s  user:    0s     OK
Starting work on addancs
addancs                                         real:    0s  user:    0s     OK
Starting work on astScript
astScript                                       real:    0s  user:    0s     OK
Starting work on fpSemScript
fpSemScript                                     real:    0s  user:    0s     OK
Starting work on fpSemTheory
progTheory                                      real:    3s  user:    2s     OK
Starting work on addressTheory
lem_string_extraTheory                          real:    3s  user:    3s     OK
Starting work on namespaceScript
namespaceScript                                 real:    0s  user:    0s     OK
Starting work on namespaceTheory
byteTheory                                      real:    3s  user:    3s     OK
Starting work on tokensScript
tokensScript                                    real:    0s  user:    0s     OK
Starting work on tokensTheory
fpSemTheory                                     real:    4s  user:    3s     OK
namespaceTheory                                 real:    3s  user:    2s     OK
Starting work on astTheory
tokensTheory                                    real:    5s  user:    4s     OK
Starting work on gramTheory
addressTheory                                   real:    6s  user:    6s     OK
Starting work on miscTheory
astTheory                                       real:   10s  user:   10s     OK
Starting work on semanticPrimitivesTheory
miscTheory                                      real:    8s  user:    7sFAIL<1>
 No match
 error in quse /home/cake/oven/regression/cakeml-1265/misc/miscScript.sml : HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 error in load /home/cake/oven/regression/cakeml-1265/misc/miscScript : HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Proof of 
 
 0 < k  n. SORTED $< (GENLIST ($* k) n)
 
 failed.
 Failed to prove theorem SORTED_GENLIST_TIMES.
 Uncaught exception: HOL_ERR {message = "No match", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
gramTheory                                                              M-KILLED
semanticPrimitivesTheory                                                M-KILLED