Job 1656

CakeML:8f085db9a8f465e352879abff4452dc03e8665e7
  Fix breakage in terminationTheory [Nov 23 15:12:24]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:789ad86cf1243f351ce7b720d1829e274e34bbc9
  Use newer theorem style for list_size_append [Nov 22 23:02:25]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 23 15:28:38 Claimed job
Nov 23 15:28:42 Reusing HOL
Nov 23 15:29:19 Starting developers
Nov 23 15:29:23 Finished developers                                               4s 133MB
Nov 23 15:29:23 Starting developers/bin
Nov 23 15:29:30 Finished developers/bin                                           6s   1GB
Nov 23 15:29:30 Starting semantics/ffi
Nov 23 15:29:38 Finished semantics/ffi                                            8s 236MB
Nov 23 15:29:38 Starting semantics
Nov 23 15:31:01 Finished semantics                                             1m23s   1GB
Nov 23 15:31:01 Starting semantics/proofs
Nov 23 15:34:37 Finished semantics/proofs                                      3m35s   1GB
Nov 23 15:34:37 Starting semantics/alt_semantics
Nov 23 15:34:49 Finished semantics/alt_semantics                                 11s 375MB
Nov 23 15:34:49 Starting semantics/alt_semantics/proofs
Nov 23 15:37:15 Finished semantics/alt_semantics/proofs                        2m26s 877MB
Nov 23 15:37:15 Starting basis/pure
Nov 23 15:40:12 Finished basis/pure                                            2m56s 858MB
Nov 23 15:40:12 Starting translator
Nov 23 15:42:59 Finished translator                                            2m46s   1GB
Nov 23 15:42:59 Starting compiler/parsing
Nov 23 15:44:13 Finished compiler/parsing                                      1m13s   2GB
Nov 23 15:44:13 Starting characteristic
Nov 23 15:46:50 FAILED: characteristic
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/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Starting work on temporalTheory
Starting work on README.md
Starting work on cfFFITypeTheory
README.md                                                                                   characteristic  (0s)     OK
temporalTheory                                                          examples/machine-code/hoare-triple  (2s)     OK
Finished $(HOLDIR)/examples/machine-code/hoare-triple [#theories: 1]                                           (2.061s) 
cfFFITypeTheory                                                                             characteristic  (9s)     OK
Starting work on cfHeapsBaseTheory
cfHeapsBaseTheory                                                                           characteristic (21s)     OK
Starting work on cfHeapsTheory
cfHeapsTheory                                                                               characteristic (15s)     OK
Starting work on cfStoreTheory
cfStoreTheory                                                                               characteristic (18s)     OK
Starting work on cfNormaliseTheory
cfNormaliseTheory                                                                           characteristic (17s)     OK
Starting work on cfAppTheory
cfAppTheory                                                                                 characteristic (18s)     OK
Starting work on cfTheory
cfTheory                                                                                    characteristic (47s)FAIL<1>
 Exception raised at Tactical.THEN1:
 goal completely solved by first tactic (THEN1 on line 1877) (THEN1 on line 1881)
 
 Exception raised at TotalDefn.tDefine:
 at Defn.tprove:
 at Tactical.THEN1:
 goal completely solved by first tactic (THEN1 on line 1877) (THEN1 on line 1881)
 error in quse /home/cug/hk324/cml-regression/cakeml-1656/characteristic/cfScript.sml : HOL_ERR {message = "at Defn.tprove:\nat Tactical.THEN1:\ngoal completely solved by first tactic (THEN1 on line 1877) (THEN1 on line 1881)", origin_function = "tDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1656/characteristic/cfScript : HOL_ERR {message = "at Defn.tprove:\nat Tactical.THEN1:\ngoal completely solved by first tactic (THEN1 on line 1877) (THEN1 on line 1881)", origin_function = "tDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.tprove:\nat Tactical.THEN1:\ngoal completely solved by first tactic (THEN1 on line 1877) (THEN1 on line 1881)", origin_function = "tDefine", origin_structure = "TotalDefn"}