Job 2015

CakeML:b264b826ccfabe749ca082b1d286a7cd9135c23c
  Fix missing case in inferScript for RealFromIntProd [Oct 12 15:22:10]
#911 (libm_gen)
Merging into:59e14a942bb54a58350e86539c1953c541eff3f4
  Merge pull request #909 from mktnk3/word_to_word_Pancake [Oct 01 15:44:31]
HOL:52406bd0bb1d700af123bb9b3fe55c38be50c11c
  Use Zorn's Lemma to show all strong orders can extend to linear ones [Oct 10 05:46:28]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Oct 13 22:49:06 Claimed job
Oct 13 22:49:10 Reusing HOL
Oct 13 22:49:50 Starting developers
Oct 13 22:49:55 Finished developers                                               5s 147MB
Oct 13 22:49:55 Starting developers/bin
Oct 13 22:50:02 Finished developers/bin                                           6s   1GB
Oct 13 22:50:02 Starting compiler/proofs
Oct 14 00:34:55 Finished compiler/proofs                                    1h44m51s  24GB
Oct 14 00:34:55 Starting compiler/bootstrap/translation
Oct 14 05:24:16 Finished compiler/bootstrap/translation                     4h49m20s  46GB
Oct 14 05:24:16 Starting semantics/ffi
Oct 14 05:24:20 Finished semantics/ffi                                            3s 220MB
Oct 14 05:24:20 Starting semantics
Oct 14 05:24:21 Finished semantics                                                1s  19MB
Oct 14 05:24:21 Starting semantics/proofs
Oct 14 05:24:53 Finished semantics/proofs                                        31s 767MB
Oct 14 05:24:54 Starting semantics/alt_semantics
Oct 14 05:25:22 Finished semantics/alt_semantics                                 27s 537MB
Oct 14 05:25:22 Starting semantics/alt_semantics/proofs
Oct 14 05:27:34 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/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$(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 20 directories
Starting work on README.md
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
README.md                                                                                                                                                                       (0s)     OK
bigSmallInvariantsTheory                                                                                                                                                        (4s)     OK
determTheory                                                                                                                                                                   (31s)     OK
Starting work on bigClockTheory
Starting work on smallStepPropsTheory
bigStepPropsTheory                                                                                                                                                             (65s)     OK
bigClockTheory                                                                                                                                                                 (96s)FAIL<1>
 error in quse /home/cug/hk324/cml-regression/cakeml-2015/semantics/alt_semantics/proofs/bigClockScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 563 (THEN1 on line 492)", origin_function = "by", origin_structure = "BasicProvers"}
 error in load /home/cug/hk324/cml-regression/cakeml-2015/semantics/alt_semantics/proofs/bigClockScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 563 (THEN1 on line 492)", origin_function = "by", origin_structure = "BasicProvers"}
 Proof of 
 
 count_e env s. s' r.
   evaluate T env (s with clock := FST count_e) (SND count_e) (s',r)
 
 failed.
 Failed to prove theorem big_clocked_total_lem.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 563 (THEN1 on line 492)", origin_function = "by", origin_structure = "BasicProvers"}
smallStepPropsTheory                                                                                                                                                           (96s)MKILLED