Overview

Job 705

CakeML:be8c718bd26f8f7df6310ab4c48d33c300c1d23a
  Merge pull request #612 from CakeML/cleanup
HOL:06ccf1b4dc843d47c83e3bcc524ba159273d7d1f
  Merge pull request #645 from binghe/hol-unicode-replacements.fix
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               0s  35MB
 Starting developers/bin
 Finished developers/bin                                          29s 205MB
 Starting semantics/ffi
 Finished semantics/ffi                                           33s 481MB
 Starting semantics
 Finished semantics                                             1m31s   1GB
 Starting semantics/proofs
 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ~/regression/cakeml-705/developers]0;Holmake: ~/regression/cakeml-705/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-705/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-705/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-705/misc]0;Holmake: ~/regression/cakeml-705/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-705/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-705/misc]0;Holmake: ~/regression/cakeml-705/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