CakeML:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
Merge pull request #842 from CakeML/ramsey
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
emacs-mode: adjust holmake command to get to use ANSI magic
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 4s 126MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 11s 265MB
Starting semantics
FAILED: semantics
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
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 examples/machine-code/hoare-triple (0s) OK
Starting work on lem_listTheory
grammarTheory examples/formal-languages/context-free (2s) OK
Finished $(HOLDIR)/examples/formal-languages/context-free [#theories: 1] (2.623s)
Starting work on lem_list_extraTheory
lprefix_lubTheory examples/fun-op-sem/lprefix_lub (3s) OK
Finished $(HOLDIR)/examples/fun-op-sem/lprefix_lub [#theories: 1] (3.205s)
Starting work on lem_set_extraTheory
set_sepTheory examples/machine-code/hoare-triple (3s) OK
Starting work on progTheory
lem_set_extraTheory misc/lem_lib_stub (0s) OK
Starting work on lem_stringTheory
lem_listTheory misc/lem_lib_stub (2s) OK
Starting work on lem_string_extraTheory
lem_stringTheory misc/lem_lib_stub (0s) OK
Starting work on byteTheory
lem_list_extraTheory misc/lem_lib_stub (2s) OK
Starting work on README.md
README.md semantics (0s) OK
Starting work on addancs
progTheory examples/machine-code/hoare-triple (2s) OK
Starting work on addressTheory
lem_string_extraTheory misc/lem_lib_stub (2s) OK
Finished $(CAKEMLDIR)/misc/lem_lib_stub [#theories: 5] (8.237s)
Starting work on fpSemScript
addancs semantics (0s) OK
Starting work on astScript
byteTheory misc (2s) OK
Starting work on namespaceScript
astScript semantics (2s) OK
Starting work on tokensScript
namespaceScript semantics (2s) OK
Starting work on namespaceTheory
fpSemScript semantics (3s) OK
Starting work on fpSemTheory
tokensScript semantics (2s) OK
Starting work on tokensTheory
addressTheory examples/machine-code/hoare-triple (5s) OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4] (12.524s)
Starting work on miscTheory
namespaceTheory semantics (2s) OK
fpSemTheory semantics (2s) OK
Starting work on astTheory
tokensTheory semantics (4s) OK
Starting work on gramTheory
astTheory semantics (8s) OK
Starting work on semanticPrimitivesTheory
gramTheory semantics (9s) OK
miscTheory misc (26s) OK
Finished $(CAKEMLDIR)/misc [#theories: 2] (29.019s)
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory semantics (30s) OK
Starting work on evaluateTheory
Starting work on typeSystemTheory
lexer_funTheory semantics (14s) OK
evaluateTheory semantics (4s) OK
tokenUtilsTheory semantics (17s) OK
Starting work on cmlPtreeConversionTheory
typeSystemTheory semantics (13s) OK
Starting work on primTypesTheory
Starting work on terminationTheory
primTypesTheory semantics (3s) OK
terminationTheory semantics (10s)FAIL<1>
Saved theorem _____ "evaluate_decs_ind"
Saved theorem _____ "dec1_size_eq"
Saved theorem _____ "enc_ast_t_def"
Saved theorem _____ "enc_ast_t_ind"
Exception raised at Tactical.THEN1:
goal completely solved by first tactic (THEN1 on line 396)
error in quse /home/cug/hk324/cml-regression/cakeml-1662/semantics/terminationScript.sml : HOL_ERR {message = "at Tactical.THEN1:\ngoal completely solved by first tactic (THEN1 on line 396)", origin_function = "tprove", origin_structure = "Defn"}
error in load /home/cug/hk324/cml-regression/cakeml-1662/semantics/terminationScript : HOL_ERR {message = "at Tactical.THEN1:\ngoal completely solved by first tactic (THEN1 on line 396)", origin_function = "tprove", origin_structure = "Defn"}
Uncaught exception: HOL_ERR {message = "at Tactical.THEN1:\ngoal completely solved by first tactic (THEN1 on line 396)", origin_function = "tprove", origin_structure = "Defn"}
cmlPtreeConversionTheory semantics (20s)MKILLED