Job 1242

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments [May 25 05:14:54]
#738 (export_update)
Merging into:873064b1566bc174e6b88a31121a235328ffc6c8
  Merge pull request #737 from CakeML/concatAll [Jun 01 09:27:57]
HOL:589e573d3a4ff602855aa5586d1dbf0019ae533c
  emacs-mode: Allow _ to be "symbol" or "word" in Emacs syntax tables [May 29 02:11:41]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 03 10:15:01 Claimed job
Jun 03 10:15:09 Building HOL
Jun 03 10:29:15 Starting developers
Jun 03 10:29:20 Finished developers                                               4s 103MB
Jun 03 10:29:20 Starting developers/bin
Jun 03 10:29:28 Finished developers/bin                                           7s   1GB
Jun 03 10:29:28 Starting semantics/ffi
Jun 03 10:29:39 Finished semantics/ffi                                           11s 239MB
Jun 03 10:29:40 Starting semantics
Jun 03 10:30:13 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
set_sepTheory                                   real:    4s  user:    3s     OK
Starting work on progTheory
lem_list_extraTheory                            real:    3s  user:    2s     OK
Starting work on byteTheory
lem_stringTheory                                real:    0s  user:    0s     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:    2s     OK
Starting work on namespaceScript
namespaceScript                                 real:    0s  user:    0s     OK
Starting work on namespaceTheory
byteTheory                                      real:    3s  user:    2s     OK
Starting work on tokensScript
tokensScript                                    real:    0s  user:    0s     OK
Starting work on tokensTheory
fpSemTheory                                     real:    3s  user:    2s     OK
namespaceTheory                                 real:    2s  user:    2s     OK
Starting work on astTheory
tokensTheory                                    real:    4s  user:    4s     OK
Starting work on gramTheory
addressTheory                                   real:    6s  user:    5s     OK
Starting work on miscTheory
astTheory                                       real:   10s  user:    9s     OK
Starting work on semanticPrimitivesTheory
gramTheory                                      real:   10s  user:    9s     OK
miscTheory                                      real:   18s  user:   17sFAIL<1>
  (THEN1 on line 2820) (THEN1 on line 2825)
 error in quse /home/cake/oven/regression/cakeml-1242/misc/miscScript.sml : HOL_ERR {message = " (THEN1 on line 2820) (THEN1 on line 2825)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
 error in load /home/cake/oven/regression/cakeml-1242/misc/miscScript : HOL_ERR {message = " (THEN1 on line 2820) (THEN1 on line 2825)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
 Proof of 
 
 P ls l1 l2. FIELDS P ls = l1::l2  STRLEN ls  STRLEN l1  l1 = ls  l2 = []
 
 failed.
 Failed to prove theorem FIELDS_full.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 2820) (THEN1 on line 2825)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
semanticPrimitivesTheory                                                M-KILLED