Job 706

CakeML:439765649dab969418d87f5592e9091a52fa175e
  Remove SML style datatype declarations from grammar [Jan 30 11:21:25]
#613 (gh611)
Merging into:be8c718bd26f8f7df6310ab4c48d33c300c1d23a
  Merge pull request #612 from CakeML/cleanup [Jan 28 07:33:16]
HOL:06ccf1b4dc843d47c83e3bcc524ba159273d7d1f
  Merge pull request #645 from binghe/hol-unicode-replacements.fix [Jan 30 10:22:13]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 30 12:08:30 Claimed job
Jan 30 12:08:34 Reusing HOL
Jan 30 12:08:48 Starting developers
Jan 30 12:08:49 Finished developers                                               0s  32MB
Jan 30 12:08:50 Starting developers/bin
Jan 30 12:09:21 Finished developers/bin                                          29s 205MB
Jan 30 12:09:21 Starting semantics/ffi
Jan 30 12:09:30 Finished semantics/ffi                                            7s 227MB
Jan 30 12:09:31 Starting semantics
Jan 30 12:10:48 Finished semantics                                             1m16s   1GB
Jan 30 12:10:49 Starting semantics/proofs
Jan 30 12:11:48 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ~/regression/cakeml-706/developers]0;Holmake: ~/regression/cakeml-706/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-706/misc]0;Holmake: ~/regression/HOL-06ccf1b4dc843d47c83e3bcc524ba159273d7d1f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-06ccf1b4dc843d47c83e3bcc524ba159273d7d1f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-706/misc]0;Holmake: ~/regression/HOL-06ccf1b4dc843d47c83e3bcc524ba159273d7d1f/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-06ccf1b4dc843d47c83e3bcc524ba159273d7d1f/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-706/misc]0;Holmake: ~/regression/cakeml-706/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-706/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-706/misc]0;Holmake: ~/regression/cakeml-706/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../ffi]0;Holmake: ../ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on namespacePropsTheory
Starting work on README.md
README.md                                                                                                  OK
astPropsTheory                                                                                             OK
namespacePropsTheory                                                                                       OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                                                                                  OK
gramPropsTheory                                                                                            OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                                                                              OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                                                                              OK
evaluatePropsTheory                                                                               FAILED! <1>
 error in load evaluatePropsScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Proof of 
 
 is_clock_io_mono f s 
 f s = (s',r)  r  Rerr (Rabort Rtimeout_error) 
 ck0. f (s with clock := ck0) = (s' with clock := ck1,r)
 
 failed.
 Failed to prove theorem is_clock_io_mono_set_clock.
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
typeSysPropsTheory                                                                                   M-KILLED