Job 638

CakeML:7db669b022b0430c4ffdeee063a4625dd304592c
  Fix a few missed Holmakefiles [Dec 20 11:48:32]
#583 (heapfree)
Merging into:9b366aa092a1e2c8100d95bbe3fa77b5fe513dc9
  Merge pull request #582 from CakeML/cleanup [Dec 14 06:05:52]
HOL:c99bf069b288e4e86f509d0fac5871d776094f01
  Make the src/boss selftest run on top of the standard HOL heap [Dec 19 10:03:16]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 20 15:33:50 Claimed job
Dec 20 15:34:11 Building HOL
Dec 20 15:43:30 Starting developers
Dec 20 15:43:33 Finished developers                                               2s  20MB
Dec 20 15:43:34 Starting developers/bin
Dec 20 15:44:50 Finished developers/bin                                        1m15s 916MB
Dec 20 15:44:51 Starting semantics/ffi
Dec 20 15:45:30 Finished semantics/ffi                                           38s 379MB
Dec 20 15:45:31 Starting semantics
Dec 20 15:47:11 Finished semantics                                             1m39s   1GB
Dec 20 15:47:11 Starting semantics/proofs
Dec 20 15:50:35 Finished semantics/proofs                                      3m22s   1GB
Dec 20 15:50:35 Starting basis/pure
Dec 20 15:54:14 Finished basis/pure                                            3m37s 627MB
Dec 20 15:54:14 Starting translator
Dec 20 15:55:30 FAILED: translator
]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-638/basis/pure]0;Holmake: ~/oven/regression/cakeml-638/misc]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-638/misc]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-c99bf069b288e4e86f509d0fac5871d776094f01/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-638/misc]0;Holmake: ~/oven/regression/cakeml-638/developers]0;Holmake: ~/oven/regression/cakeml-638/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-638/misc]0;Holmake: ~/oven/regression/cakeml-638/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-638/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-638/misc]0;Holmake: ~/oven/regression/cakeml-638/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-638/basis/pure]0;Holmake: ~/oven/regression/cakeml-638/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-638/semantics]0;Holmake: ~/oven/regression/cakeml-638/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-638/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-638/semantics]0;Holmake: ~/oven/regression/cakeml-638/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-638/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-638/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                                                     OK
Starting work on std_preludeTheory
ml_module_demoTheory                                                         OK
ml_pmatch_demoTheory                                                FAILED! <1>
 Adding type : list
 Doing proof of: EqualityType (LIST_TYPE a)
 Adding type : # 
 Doing proof of: EqualityType (PAIR_TYPE b c)
 Adding type :unit
 Doing proof of: error in quse /home/cake/oven/regression/cakeml-638/translator/ml_pmatch_demoScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load ml_pmatch_demoScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 EqualityType UNIT_TYPE
 Failed translation: foo
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
ml_translator_testTheory                                               M-KILLED
std_preludeTheory                                                      M-KILLED