Job 772

CakeML: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 13:06:31 Claimed job
Apr 04 13:06:34 Reusing HOL
Apr 04 13:06:40 Starting developers
Apr 04 13:06:41 Finished developers                                               0s  35MB
Apr 04 13:06:41 Starting developers/bin
Apr 04 13:07:15 Finished developers/bin                                          33s 142MB
Apr 04 13:07:16 Starting semantics/ffi
Apr 04 13:07:24 Finished semantics/ffi                                            7s 222MB
Apr 04 13:07:24 Starting semantics
Apr 04 13:08:42 Finished semantics                                             1m17s   1GB
Apr 04 13:08:42 Starting semantics/proofs
Apr 04 13:11:33 Finished semantics/proofs                                      2m51s   1GB
Apr 04 13:11:34 Starting basis/pure
Apr 04 13:12:17 Finished basis/pure                                              43s 563MB
Apr 04 13:12:18 Starting translator
Apr 04 13:13:28 FAILED: translator
]0;Holmake: ~/regression/cakeml-772/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-772/basis/pure]0;Holmake: ~/regression/cakeml-772/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-772/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-772/misc]0;Holmake: ~/regression/cakeml-772/developers]0;Holmake: ~/regression/cakeml-772/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-772/misc]0;Holmake: ~/regression/cakeml-772/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-772/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-772/misc]0;Holmake: ~/regression/cakeml-772/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-772/basis/pure]0;Holmake: ~/regression/cakeml-772/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-772/semantics]0;Holmake: ~/regression/cakeml-772/semantics/ffi]0;Holmake: ~/regression/cakeml-772/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-772/semantics]0;Holmake: ~/regression/cakeml-772/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-772/semantics/proofs]0;Holmake: ~/regression/cakeml-772/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_module_demoTheory                                                         OK
Starting work on std_preludeTheory
ml_translator_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.>>
 Failed translation: ZIP2
 error in quse /home/myreen/regression/cakeml-772/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_pmatch_demoTheory                                                   M-KILLED
std_preludeTheory                                                      M-KILLED