Job 611

CakeML:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name) [Dec 03 04:19:52]
HOL:e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6
  Fix bug in proof (18934f7cf gave 2 theorems same name) [Dec 04 10:59:11]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Dec 04 19:17:29 Claimed job
Dec 04 19:17:36 Reusing HOL
Dec 04 19:17:50 Starting developers
Dec 04 19:17:51 Finished developers                                               0s  19MB
Dec 04 19:17:52 Starting developers/bin
Dec 04 19:18:25 Finished developers/bin                                          32s 202MB
Dec 04 19:18:25 Starting semantics/ffi
Dec 04 19:18:34 Finished semantics/ffi                                            8s 222MB
Dec 04 19:18:35 Starting semantics
Dec 04 19:19:50 Finished semantics                                             1m14s   1GB
Dec 04 19:19:51 Starting semantics/proofs
Dec 04 19:22:41 Finished semantics/proofs                                      2m49s   1GB
Dec 04 19:22:42 Starting basis/pure
Dec 04 19:22:59 FAILED: basis/pure
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/basis/pure[0m
Starting work on mllistTheory
Starting work on mloptionTheory
Starting work on README.md
README.md                                           OK
mloptionTheory                                      OK
mllistTheory                                        OK
Starting work on mlstringTheory
Starting work on mlvectorTheory
mlstringTheory                             FAILED! <1>
 Saved theorem _____ "concat_thm"
 Saved theorem _____ "strlen_implode"
 Saved theorem _____ "strlen_substring"
 Saved definition __ "extract_def"
 error in quse /home/myreen/regression/cakeml-611/basis/pure/mlstringScript.sml : Fail "Static Errors"
 error in load mlstringScript : Fail "Static Errors"
 Saved theorem _____ "strlen_extract_le"
 /home/myreen/regression/cakeml-611/basis/pure/mlstringScript.sml:124: error: Value or constructor (SEG_TAKE_BUTFISTN) has not been declared
 Found near [SEG_TAKE_BUTFISTN, EL_TAKE]
 Uncaught exception: Fail "Static Errors"
mlvectorTheory                                M-KILLED