Job 2240

CakeML:d583298e0c76a8ece3f43ecf8f216d697225e9e0
  Move byteTheory to HOL [Nov 15 21:14:47]
#975 (byte)
Merging into:8ac36a22c960a9f4aaae14aa89dabaf177cd63fa
  Merge pull request #974 from CakeML/dominance [Nov 15 15:00:12]
HOL:8f74c6afc449d7002c926d75228bd4ecb539d82f
  Allow type vars in cv_typesLib functions [Nov 19 10:16:00]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Nov 22 14:39:05 Claimed job
Nov 22 14:39:08 Building HOL
Nov 22 14:52:51 Starting developers
Nov 22 14:52:56 Finished developers                                               5s 168MB
Nov 22 14:52:56 Starting developers/bin
Nov 22 14:53:03 Finished developers/bin                                           6s   1GB
Nov 22 14:53:03 Starting compiler/proofs
Nov 22 16:46:55 Finished compiler/proofs                                    1h53m52s  15GB
Nov 22 16:46:55 Starting compiler/bootstrap/translation
Nov 23 00:50:36 Finished compiler/bootstrap/translation                     8h03m40s  42GB
Nov 23 00:50:36 Starting semantics/ffi
Nov 23 00:50:41 Finished semantics/ffi                                            4s 386MB
Nov 23 00:50:41 Starting semantics
Nov 23 00:50:42 Finished semantics                                                1s  20MB
Nov 23 00:50:42 Starting semantics/proofs
Nov 23 00:51:16 Finished semantics/proofs                                        33s 717MB
Nov 23 00:51:16 Starting semantics/alt_semantics
Nov 23 00:51:48 Finished semantics/alt_semantics                                 32s 788MB
Nov 23 00:51:48 Starting semantics/alt_semantics/proofs
Nov 23 01:02:18 FAILED: semantics/alt_semantics/proofs
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/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$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 19 directories
Starting work on README.md
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
README.md                                                                                                                                                                       (0s)     OK
bigSmallInvariantsTheory                                                                                                                                                        (6s)     OK
determTheory                                                                                                                                                                   (34s)     OK
Starting work on bigClockTheory
Starting work on smallStepPropsTheory
bigStepPropsTheory                                                                                                                                                             (71s)     OK
bigClockTheory                                                                                                                                                                (114s)     OK
Starting work on interpTheory
interpTheory                                                                                                                                                                   (25s)     OK
Starting work on funBigStepEquivTheory
funBigStepEquivTheory                                                                                                                                                          (35s)     OK
smallStepPropsTheory                                                                                                                                                          (371s)     OK
Starting work on bigSmallEquivTheory
Starting work on itree_semanticsPropsTheory
itree_semanticsPropsTheory                                                                                                                                                     (58s)     OK
bigSmallEquivTheory                                                                                                                                                           (189s)     OK
Starting work on itree_semanticsEquivTheory
itree_semanticsEquivTheory                                                                                                                                                     (19s)FAIL<1>
 error in load /home/cug/hk324/cml-regression/cakeml-2240/semantics/alt_semantics/proofs/itree_semanticsEquivScript : HOL_ERR {message = "No match (THEN1 on line 109)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}
 Proof of 
 
 (s. op  FFI s)  ctxt_rel cs1 cs2 
 step_result_rel (application op env st fp vs cs1)
   (application op env (st,ffi) fp vs cs2)
 
 failed.
 Failed to prove theorem application_rel.
 Uncaught exception: HOL_ERR {message = "No match (THEN1 on line 109)", origin_function = "MATCH_MP_TAC", origin_structure = "Tactic"}