Job 1213

CakeML:10e67580f911d5088b98a64a04b236f2e0b2e507
  Merge pull request #734 from CakeML/func-names [Mar 25 11:36:11]
HOL:6b4719d7d8f08e26a916ae574f5dda24c6fc4245
  Fix proofs broken by 508f79ea974 [Mar 25 05:16:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 29 19:30:43 Claimed job
Mar 29 19:30:48 Building HOL
Mar 29 19:43:55 Starting developers
Mar 29 19:44:00 Finished developers                                               4s  91MB
Mar 29 19:44:00 Starting developers/bin
Mar 29 19:44:08 Finished developers/bin                                           7s   1GB
Mar 29 19:44:08 Starting semantics/ffi
Mar 29 19:44:18 Finished semantics/ffi                                           10s 225MB
Mar 29 19:44:19 Starting semantics
Mar 29 19:44:27 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
grammarTheory                                   real:    3s  user:    2s     OK
Starting work on lem_set_extraTheory
lprefix_lubTheory                               real:    3s  user:    2s     OK
Starting work on lem_stringTheory
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:    2s  user:    2s     OK
Starting work on README.md
set_sepTheory                                   real:    4s  user:    3s     OK
Starting work on progTheory
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
lem_string_extraTheory                          real:    2s  user:    2s     OK
Starting work on namespaceScript
namespaceScript                                 real:    0s  user:    0s     OK
Starting work on namespaceTheory
byteTheory                                      real:    3s  user:    2sFAIL<1>
     LENGTH l1 MOD w2n bytes_in_word = 0 
     words_of_bytes be (l1  l2) = words_of_bytes be l1  words_of_bytes be l2
 
 failed.
 First unsolved sub-goal is
 
 d. bytes_in_word = 0w  n' = d
 
 Failed to prove theorem words_of_bytes_append.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
progTheory                                                              M-KILLED
fpSemTheory                                                             M-KILLED
namespaceTheory                                                         M-KILLED