Job 773

CakeML:363f4063657209f371cfe85a62fd00695856a200
  Linear scan: change the name of the theorem `set_MAP_FST_toAList` in  [Apr 03 07:31:27]
#623 (linear-scan)
Merging into:4e837ffdd2b7c207dc897fe6802efd3407fce74d
  Merge pull request #624 from CakeML/cf-div [Mar 31 19:10:45]
HOL:8990db3c7743feb190d98f4bce666d3163022557
  Fix a proof to be more efficient [Apr 04 11:32:09]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 05 11:36:34 Claimed job
Apr 05 11:37:13 Building HOL
Apr 05 11:46:31 Starting developers
Apr 05 11:46:34 Finished developers                                               2s  20MB
Apr 05 11:46:34 Starting developers/bin
Apr 05 11:47:40 Finished developers/bin                                        1m05s 918MB
Apr 05 11:47:40 Starting semantics/ffi
Apr 05 11:48:18 Finished semantics/ffi                                           38s 372MB
Apr 05 11:48:19 Starting semantics
Apr 05 11:49:55 Finished semantics                                             1m36s   1GB
Apr 05 11:49:55 Starting semantics/proofs
Apr 05 11:52:53 Finished semantics/proofs                                      2m57s   1GB
Apr 05 11:52:54 Starting basis/pure
Apr 05 11:56:31 Finished basis/pure                                            3m37s 698MB
Apr 05 11:56:32 Starting translator
Apr 05 11:57:45 FAILED: translator
]0;Holmake: ~/oven/regression/cakeml-773/basis/pure]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-773/basis/pure]0;Holmake: ~/oven/regression/cakeml-773/misc]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-773/misc]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-8990db3c7743feb190d98f4bce666d3163022557/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-773/misc]0;Holmake: ~/oven/regression/cakeml-773/developers]0;Holmake: ~/oven/regression/cakeml-773/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-773/misc]0;Holmake: ~/oven/regression/cakeml-773/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-773/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-773/misc]0;Holmake: ~/oven/regression/cakeml-773/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-773/basis/pure]0;Holmake: ~/oven/regression/cakeml-773/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-773/semantics]0;Holmake: ~/oven/regression/cakeml-773/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-773/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-773/semantics]0;Holmake: ~/oven/regression/cakeml-773/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-773/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-773/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_translator_testTheory                                            FAILED! <1>
 Adding type : list.
 Adding type : # 
 Doing proof of: EqualityType (PAIR_TYPE b c)
 Adding type : # .
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 error in quse /home/cake/oven/regression/cakeml-773/translator/ml_translator_testScript.sml : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 error in load ml_translator_testScript : HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
 Failed translation: ZIP2
 Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
ml_pmatch_demoTheory                                                   M-KILLED
std_preludeTheory                                                      M-KILLED