Overview

Job 1658

CakeML:4ab53d65d30d390110be9933723bc3f088c6e804
  Finish clos_opProof
#847 (clos-smart-op)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey
HOL:789ad86cf1243f351ce7b720d1829e274e34bbc9
  Use newer theorem style for list_size_append
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               4s  81MB
 Starting developers/bin
 Finished developers/bin                                           6s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s 243MB
 Starting semantics
 FAILED: semantics
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
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                   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.857s) 
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.456s) 
Starting work on lem_set_extraTheory
set_sepTheory                   examples/machine-code/hoare-triple  (3s)     OK
Starting work on progTheory
lem_listTheory                                   misc/lem_lib_stub  (2s)     OK
Starting work on lem_stringTheory
lem_set_extraTheory                              misc/lem_lib_stub  (0s)     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
addancs                                                  semantics  (0s)     OK
Starting work on astScript
astScript                                                semantics  (0s)     OK
Starting work on fpSemScript
fpSemScript                                              semantics  (0s)     OK
Starting work on fpSemTheory
lem_string_extraTheory                           misc/lem_lib_stub  (2s)     OK
Finished $(CAKEMLDIR)/misc/lem_lib_stub [#theories: 5]                 (8.202s) 
Starting work on namespaceScript
namespaceScript                                          semantics  (0s)     OK
Starting work on namespaceTheory
byteTheory                                                    misc  (2s)     OK
Starting work on tokensScript
tokensScript                                             semantics  (0s)     OK
Starting work on tokensTheory
namespaceTheory                                          semantics  (2s)     OK
fpSemTheory                                              semantics  (3s)     OK
Starting work on astTheory
tokensTheory                                             semantics  (4s)     OK
Starting work on gramTheory
addressTheory                   examples/machine-code/hoare-triple  (6s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 4]  (13.209s) 
Starting work on miscTheory
astTheory                                                semantics  (9s)     OK
Starting work on semanticPrimitivesTheory
gramTheory                                               semantics  (9s)     OK
miscTheory                                                    misc (27s)     OK
Finished $(CAKEMLDIR)/misc [#theories: 2]                             (29.434s) 
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory                                 semantics (31s)     OK
Starting work on evaluateTheory
Starting work on typeSystemTheory
lexer_funTheory                                          semantics (14s)     OK
evaluateTheory                                           semantics  (4s)     OK
tokenUtilsTheory                                         semantics (16s)     OK
Starting work on cmlPtreeConversionTheory
typeSystemTheory                                         semantics (14s)     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/cake/oven/regression/cakeml-1658/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/cake/oven/regression/cakeml-1658/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 (21s)MKILLED