Job 1778

CakeML:9da62db97bd8d36599f7e1ed93eb8396290d8b71
  Fix Define calls in translator [Feb 17 13:35:07]
#863 (repl)
Merging into:67b312862a2b9919d20a41b16a6599ef4a7635fe
  Merge pull request #855 from CakeML/minor-reheapification [Feb 14 13:06:51]
HOL:b42a44c7c2eceaa7d85097e51c32ac752db13c32
  Change to Define loses ability to write leading !vs. block [Feb 16 10:07:18]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 17 15:11:41 Claimed job
Feb 17 15:11:42 Reusing HOL
Feb 17 15:11:55 Starting developers
Feb 17 15:11:59 Finished developers                                               4s 174MB
Feb 17 15:11:59 Starting developers/bin
Feb 17 15:12:04 Finished developers/bin                                           4s 674MB
Feb 17 15:12:04 Starting semantics/ffi
Feb 17 15:12:13 Finished semantics/ffi                                            9s 239MB
Feb 17 15:12:13 Starting semantics
Feb 17 15:14:15 Finished semantics                                             2m01s   1GB
Feb 17 15:14:15 Starting semantics/proofs
Feb 17 15:17:59 Finished semantics/proofs                                      3m43s   1GB
Feb 17 15:17:59 Starting semantics/alt_semantics
Feb 17 15:18:16 Finished semantics/alt_semantics                                 16s 482MB
Feb 17 15:18:16 Starting semantics/alt_semantics/proofs
Feb 17 15:20:45 Finished semantics/alt_semantics/proofs                        2m28s 770MB
Feb 17 15:20:45 Starting basis/pure
Feb 17 15:21:51 Finished basis/pure                                            1m05s 821MB
Feb 17 15:21:51 Starting translator
Feb 17 15:23:34 FAILED: translator
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 23 directories
Finished $(CAKEMLDIR)/misc                                                                                                                                                           (0.000s) 
Starting work on README.md
Starting work on ml_progTheory
README.md                                                                                                                                                             translator  (0s)     OK
ml_progTheory                                                                                                                                                         translator (20s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                                                   translator (43s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                                                                                                                                                       translator (16s)     OK
ml_optimiseTheory                                                                                                                                                     translator (18s)     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                                                                                                                                              translator (13s)     OK
Starting work on std_preludeTheory
ml_module_demoTheory                                                                                                                                                  translator (14s)     OK
ml_translator_testTheory                                                                                                                                              translator (14s)FAIL<1>
 Adding type : # 
 Attempting proof of: EqualityType (PAIR_TYPE b c)
 .. done EqualityType proof.
 Adding type : # .
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Failed translation: !
 error in quse /home/cug/hk324/cml-regression/cakeml-1778/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 /home/cug/hk324/cml-regression/cakeml-1778/translator/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                                                                                                                                                  translator (15s)MKILLED
std_preludeTheory                                                                                                                                                     translator  (1s)MKILLED