Overview

Job 842

CakeML:9b76da18451e61d9802a6c5b642f6af41912d070
  Fix some broken forward steps piled on tactics proofs
#635 (thm)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup
HOL:544f92fea1905436f7a85854eed6dcb089568063
  Emacs mode: key-bindings for 
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  21MB
 Starting developers/bin
 Finished developers/bin                                           3s 144MB
 Starting semantics/ffi
 Finished semantics/ffi                                            7s 221MB
 Starting semantics
 FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-842/developers]0;Holmake: ~/regression/cakeml-842/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-842/misc]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-842/misc]0;Holmake: ~/regression/cakeml-842/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-842/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-842/misc]0;Holmake: ~/regression/cakeml-842/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on byteTheory
byteTheory                                                                                                 OK
Starting work on miscTheory
miscTheory                                                                                        FAILED! <1>
 Saved definition __ "splitlines_def"
 Saved theorem _____ "splitlines_next"
 Saved theorem _____ "splitlines_nil"
 Saved theorem _____ "splitlines_eq_nil"
 Saved theorem _____ "splitlines_CONS_FST_SPLITP"
 /home/myreen/regression/cakeml-842/misc/miscScript.sml:3181: error: Value or constructor (DIV_0_IMP_LT) has not been declared in structure numposrepTheory
 Found near [numposrepTheory.DIV_0_IMP_LT, LESS_DIV_EQ_ZERO]
 error in quse /home/myreen/regression/cakeml-842/misc/miscScript.sml : Fail "Static Errors"
 error in load miscScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
]0;Holmake: .