Job 716

CakeML:0b669f77530f96dc7e085265545c193a6cd256f2
  Merge pull request #613 from CakeML/gh611 [Feb 04 10:11:36]
HOL:cef46b30e59158d5a063cde901ed20a4dbf06ed3
  Add composition thm for SUM_MAP; document sums better in DESCRIPTION [Feb 04 06:24:41]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 05 16:01:05 Claimed job
Feb 05 16:01:32 Building HOL
Feb 05 16:10:35 Starting developers
Feb 05 16:10:38 Finished developers                                               2s  20MB
Feb 05 16:10:38 Starting developers/bin
Feb 05 16:12:01 Finished developers/bin                                        1m21s 918MB
Feb 05 16:12:01 Starting semantics/ffi
Feb 05 16:12:40 Finished semantics/ffi                                           37s 365MB
Feb 05 16:12:40 Starting semantics
Feb 05 16:14:16 Finished semantics                                             1m35s   1GB
Feb 05 16:14:17 Starting semantics/proofs
Feb 05 16:17:24 Finished semantics/proofs                                      3m06s   1GB
Feb 05 16:17:25 Starting basis/pure
Feb 05 16:20:55 Finished basis/pure                                            3m29s 632MB
Feb 05 16:20:56 Starting translator
Feb 05 16:22:05 FAILED: translator
]0;Holmake: ~/oven/regression/cakeml-716/basis/pure]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-716/basis/pure]0;Holmake: ~/oven/regression/cakeml-716/misc]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-716/misc]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-cef46b30e59158d5a063cde901ed20a4dbf06ed3/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-716/misc]0;Holmake: ~/oven/regression/cakeml-716/developers]0;Holmake: ~/oven/regression/cakeml-716/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-716/misc]0;Holmake: ~/oven/regression/cakeml-716/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-716/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-716/misc]0;Holmake: ~/oven/regression/cakeml-716/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-716/basis/pure]0;Holmake: ~/oven/regression/cakeml-716/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-716/semantics]0;Holmake: ~/oven/regression/cakeml-716/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-716/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-716/semantics]0;Holmake: ~/oven/regression/cakeml-716/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-716/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-716/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/translator
Starting work on ml_progTheory
Starting work on README.md
README.md                                                                    OK
ml_progTheory                                                                OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                          OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                                                              OK
ml_optimiseTheory                                                            OK
Starting work on ml_module_demoTheory
Starting work on ml_pmatch_demoTheory
Starting work on ml_translator_demoTheory
Starting work on ml_translator_testTheory
ml_translator_demoTheory                                            FAILED! <1>
 error in quse /home/cake/oven/regression/cakeml-716/translator/ml_progTheory.sml : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load $(CAKEMLDIR)/translator/ml_progTheory : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load $(CAKEMLDIR)/translator/ml_translatorTheory : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load $(CAKEMLDIR)/translator/ml_optimiseTheory : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 error in load ml_translator_demoScript : HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
 <<HOL message: link_parents: the following parents of "ml_prog"
   should already be in the theory graph (but aren't): ("alist_tree",1549383176,975910)>>
 Exception- HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"} raised
 Uncaught exception: HOL_ERR {message = "load_theory_and_parents: HOL_ERR {message = \"\", origin_function = \"link_parents\", origin_structure = \"Theory\"}", origin_function = "load_thydata", origin_structure = "TheoryReader"}
ml_module_demoTheory                                                   M-KILLED
ml_pmatch_demoTheory                                                   M-KILLED
ml_translator_testTheory                                               M-KILLED