CakeML:856d32baf4e547c01bc264b9550889360e90a51c
Remove all Lem files from semantics dir and subdirs
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
Merge pull request #842 from CakeML/ramsey
HOL:789ad86cf1243f351ce7b720d1829e274e34bbc9
Use newer theorem style for list_size_append
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 4s 142MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 7s 220MB
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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Starting work on byteTheory
Starting work on README.md
Starting work on fpSemTheory
Starting work on namespaceTheory
README.md semantics (0s) OK
Starting work on tokensTheory
namespaceTheory semantics (1s) OK
byteTheory misc (2s) OK
Starting work on miscTheory
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 (25s) OK
Finished $(CAKEMLDIR)/misc [#theories: 2] (27.913s)
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
semanticPrimitivesTheory semantics (29s) OK
Starting work on evaluateTheory
Starting work on typeSystemTheory
lexer_funTheory semantics (14s) OK
tokenUtilsTheory semantics (15s) OK
Starting work on cmlPtreeConversionTheory
evaluateTheory semantics (4s) OK
typeSystemTheory semantics (13s) OK
Starting work on primTypesTheory
Starting work on terminationTheory
primTypesTheory semantics (3s) OK
terminationTheory semantics (11s)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-1655/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-1655/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 (23s)MKILLED