CakeML:873064b1566bc174e6b88a31121a235328ffc6c8
Merge pull request #737 from CakeML/concatAll
HOL:589e573d3a4ff602855aa5586d1dbf0019ae533c
emacs-mode: Allow _ to be "symbol" or "word" in Emacs syntax tables
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 2s 121MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 9s 261MB
Starting semantics
FAILED: semantics
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Starting work on grammarTheory
Starting work on lprefix_lubTheory
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory real: 0s user: 0s OK
Starting work on lem_list_extraTheory
lprefix_lubTheory real: 2s user: 2s OK
Starting work on lem_set_extraTheory
grammarTheory real: 2s 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
README.md real: 0s user: 0s OK
Starting work on addancs
set_sepTheory real: 3s user: 3s OK
Starting work on progTheory
addancs real: 0s user: 0s OK
Starting work on astScript
astScript real: 0s user: 0s OK
Starting work on fpSemTheory
byteTheory real: 2s user: 2s OK
Starting work on namespaceScript
namespaceScript real: 0s user: 0s OK
Starting work on namespaceTheory
lem_string_extraTheory real: 2s user: 2s OK
Starting work on tokensScript
tokensScript real: 0s user: 0s OK
Starting work on tokensTheory
progTheory real: 3s user: 3s OK
Starting work on addressTheory
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: 5s user: 5s OK
Starting work on miscTheory
astTheory real: 8s user: 8s OK
Starting work on semanticPrimitivesTheory
gramTheory real: 10s user: 9s OK
miscTheory real: 19s user: 17sFAIL<1>
P ls l1 l2. FIELDS P ls = l1::l2 STRLEN ls STRLEN l1 l1 = ls l2 = []
failed.
Failed to prove theorem FIELDS_full.
Exception raised at Tactic.STRIP_TAC:
(THEN1 on line 2820) (THEN1 on line 2825)
error in quse /home/myreen/regression/cakeml-1243/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/myreen/regression/cakeml-1243/misc/miscScript : HOL_ERR {message = " (THEN1 on line 2820) (THEN1 on line 2825)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
Uncaught exception: HOL_ERR {message = " (THEN1 on line 2820) (THEN1 on line 2825)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
semanticPrimitivesTheory M-KILLED