Job 842

CakeML:9b76da18451e61d9802a6c5b642f6af41912d070
  Fix some broken forward steps piled on tactics proofs [May 07 04:36:50]
#635 (thm)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:544f92fea1905436f7a85854eed6dcb089568063
  Emacs mode: key-bindings for  [May 05 04:49:45]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 07 05:39:10 Claimed job
May 07 05:39:14 Reusing HOL
May 07 05:39:18 Starting developers
May 07 05:39:19 Finished developers                                               0s  21MB
May 07 05:39:19 Starting developers/bin
May 07 05:39:22 Finished developers/bin                                           3s 144MB
May 07 05:39:23 Starting semantics/ffi
May 07 05:39:31 Finished semantics/ffi                                            7s 221MB
May 07 05:39:31 Starting semantics
May 07 05:39:50 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: .