Job 771

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:1e8de6219fcfa9f9d37e22b77693410497144d0f
  Fixes in Miller-Rabin example to cope with simpLib API change [Apr 02 23:31:30]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 04 12:48:04 Claimed job
Apr 04 12:48:27 Building HOL
Apr 04 12:56:16 Starting developers
Apr 04 12:56:17 Finished developers                                               0s  30MB
Apr 04 12:56:17 Starting developers/bin
Apr 04 12:56:47 Finished developers/bin                                          29s 204MB
Apr 04 12:56:47 Starting semantics/ffi
Apr 04 12:57:21 Finished semantics/ffi                                           33s 309MB
Apr 04 12:57:21 Starting semantics
Apr 04 12:58:51 Finished semantics                                             1m29s   1GB
Apr 04 12:58:52 Starting semantics/proofs
Apr 04 13:01:45 Finished semantics/proofs                                      2m53s   1GB
Apr 04 13:01:46 Starting basis/pure
Apr 04 13:05:18 Finished basis/pure                                            3m31s 721MB
Apr 04 13:05:18 Starting translator
Apr 04 13:06:29 FAILED: translator
]0;Holmake: ~/regression/cakeml-771/basis/pure]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-771/basis/pure]0;Holmake: ~/regression/cakeml-771/misc]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-771/misc]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-1e8de6219fcfa9f9d37e22b77693410497144d0f/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-771/misc]0;Holmake: ~/regression/cakeml-771/developers]0;Holmake: ~/regression/cakeml-771/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-771/misc]0;Holmake: ~/regression/cakeml-771/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-771/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-771/misc]0;Holmake: ~/regression/cakeml-771/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-771/basis/pure]0;Holmake: ~/regression/cakeml-771/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-771/semantics]0;Holmake: ~/regression/cakeml-771/semantics/ffi]0;Holmake: ~/regression/cakeml-771/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-771/semantics]0;Holmake: ~/regression/cakeml-771/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-771/semantics/proofs]0;Holmake: ~/regression/cakeml-771/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator[0m
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_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.>>
 Failed translation: ZIP2
 error in quse /home/myreen/regression/cakeml-771/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 = "??"}
 Uncaught exception: HOL_ERR {message = "Preprocessor failed: unable to reduce definition to single line.", origin_function = "failwith", origin_structure = "??"}
ml_module_demoTheory                                                   M-KILLED
ml_pmatch_demoTheory                                                   M-KILLED
std_preludeTheory                                                      M-KILLED