Job 839

CakeML:2e0cf4a777feb693f4bd0fc8479eef2b6c5ac107
  Fix minor spelling mistakes in readmePrefixes [May 06 11:19:44]
#633 (FMA_support)
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:14:23 Claimed job
May 06 19:14:26 Reusing HOL
May 06 19:14:31 Starting developers
May 06 19:14:32 Finished developers                                               0s  22MB
May 06 19:14:32 Starting developers/bin
May 06 19:14:35 Finished developers/bin                                           2s 144MB
May 06 19:14:36 Starting semantics/ffi
May 06 19:14:43 Finished semantics/ffi                                            7s 245MB
May 06 19:14:44 Starting semantics
May 06 19:15:04 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-839/developers]0;Holmake: ~/regression/cakeml-839/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-839/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-839/misc]0;Holmake: ~/regression/cakeml-839/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-839/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-839/misc]0;Holmake: ~/regression/cakeml-839/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-839/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-839/misc/miscScript.sml : Fail "Static Errors"
 error in load miscScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
]0;Holmake: .