Job 838

CakeML:da20e66e8f1e7ddce99de2a3503a96aa6708ed69
  Fix bootstrap proof [May 06 19:03:03]
#629 (vstte18)
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 06 19:05:05 Claimed job
May 06 19:05:11 Building HOL
May 06 19:13:11 Starting developers
May 06 19:13:11 Finished developers                                               0s  30MB
May 06 19:13:12 Starting developers/bin
May 06 19:13:15 Finished developers/bin                                           2s 144MB
May 06 19:13:15 Starting semantics/ffi
May 06 19:13:49 Finished semantics/ffi                                           33s 493MB
May 06 19:13:49 Starting semantics
May 06 19:14:22 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
Starting work on lprefix_lubTheory
lprefix_lubTheory                                                                                          OK
]0;Holmake: .]0;Holmake: ~/regression/cakeml-838/developers]0;Holmake: ~/regression/cakeml-838/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-838/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
Starting work on set_sepTheory
Starting work on tailrecTheory
tailrecTheory                                                                                              OK
set_sepTheory                                                                                              OK
Starting work on progTheory
progTheory                                                                                                 OK
Starting work on addressTheory
Starting work on temporalTheory
temporalTheory                                                                                             OK
addressTheory                                                                                              OK
]0;Holmake: ~/regression/cakeml-838/misc]0;Holmake: ~/regression/cakeml-838/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-838/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-838/misc]0;Holmake: ~/regression/cakeml-838/misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on byteTheory
Starting work on README.md
README.md                                                                                                  OK
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-838/misc/miscScript.sml:2645: 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-838/misc/miscScript.sml : Fail "Static Errors"
 error in load miscScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
]0;Holmake: .