Job 777

CakeML:a478fddb6f76220d45e0ec482d4cb75e4913fdf8
  Fix for removal of script-file new_attribute fn [Apr 08 07:26:54]
#625 (thm-attribute-fix)
Merging into:4e837ffdd2b7c207dc897fe6802efd3407fce74d
  Merge pull request #624 from CakeML/cf-div [Mar 31 19:10:45]
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
  Remove (generated file) Thm-sig.sml when cleaning src/thm [Apr 07 04:31:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 08 11:35:04 Claimed job
Apr 08 11:35:07 Reusing HOL
Apr 08 11:35:54 Starting developers
Apr 08 11:35:57 Finished developers                                               2s  20MB
Apr 08 11:35:57 Starting developers/bin
Apr 08 11:37:13 Finished developers/bin                                        1m16s 918MB
Apr 08 11:37:14 Starting semantics/ffi
Apr 08 11:37:24 Finished semantics/ffi                                           10s 203MB
Apr 08 11:37:24 Starting semantics
Apr 08 11:38:46 Finished semantics                                             1m21s   1GB
Apr 08 11:38:46 Starting semantics/proofs
Apr 08 11:41:40 Finished semantics/proofs                                      2m53s   1GB
Apr 08 11:41:41 Starting basis/pure
Apr 08 11:42:27 Finished basis/pure                                              46s 663MB
Apr 08 11:42:27 Starting translator
Apr 08 11:43:40 FAILED: translator
]0;Holmake: ~/oven/regression/cakeml-777/basis/pure]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-777/basis/pure]0;Holmake: ~/oven/regression/cakeml-777/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-777/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-777/misc]0;Holmake: ~/oven/regression/cakeml-777/developers]0;Holmake: ~/oven/regression/cakeml-777/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-777/misc]0;Holmake: ~/oven/regression/cakeml-777/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-777/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-777/misc]0;Holmake: ~/oven/regression/cakeml-777/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-777/basis/pure]0;Holmake: ~/oven/regression/cakeml-777/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-777/semantics]0;Holmake: ~/oven/regression/cakeml-777/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-777/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-777/semantics]0;Holmake: ~/oven/regression/cakeml-777/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-777/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-777/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_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-777/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_module_demoTheory                                                   M-KILLED
ml_pmatch_demoTheory                                                   M-KILLED
std_preludeTheory                                                      M-KILLED