Job 844

CakeML:75faef2802d06fc46af487153366727db2988ada
  Fix ListProgScript [May 07 06:54:31]
#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 16:15:06 Claimed job
May 07 16:15:11 Reusing HOL
May 07 16:15:15 Starting developers
May 07 16:15:16 Finished developers                                               0s  22MB
May 07 16:15:16 Starting developers/bin
May 07 16:15:20 Finished developers/bin                                           2s 207MB
May 07 16:15:20 Starting semantics/ffi
May 07 16:15:27 Finished semantics/ffi                                            7s 226MB
May 07 16:15:28 Starting semantics
May 07 16:15:47 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-844/developers]0;Holmake: ~/regression/cakeml-844/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-844/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-844/misc]0;Holmake: ~/regression/cakeml-844/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-844/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-844/misc]0;Holmake: ~/regression/cakeml-844/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-844/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-844/misc/miscScript.sml : Fail "Static Errors"
 error in load miscScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
]0;Holmake: .