Job 1780

CakeML:8d561d6e716a58c469481107541f2ab9ef8007fa
  Update some definitions that wanted leading universals [Feb 17 23:44:30]
HOL:52eeaf3318cb6512881f389d6c992b1949b376e9
  vimhol: revoke key shortcut for loading of HOL_CONFIG file (486e33c7b [Feb 17 20:53:06]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 18 14:04:12 Claimed job
Feb 18 14:04:17 Building HOL
Feb 18 14:13:51 Starting developers
Feb 18 14:13:56 Finished developers                                               4s 108MB
Feb 18 14:13:56 Starting developers/bin
Feb 18 14:14:00 Finished developers/bin                                           4s 675MB
Feb 18 14:14:00 Starting semantics/ffi
Feb 18 14:14:10 Finished semantics/ffi                                            9s 249MB
Feb 18 14:14:10 Starting semantics
Feb 18 14:16:26 Finished semantics                                             2m16s   1GB
Feb 18 14:16:26 Starting semantics/proofs
Feb 18 14:20:05 Finished semantics/proofs                                      3m38s   1GB
Feb 18 14:20:05 Starting semantics/alt_semantics
Feb 18 14:20:22 Finished semantics/alt_semantics                                 16s 509MB
Feb 18 14:20:22 Starting semantics/alt_semantics/proofs
Feb 18 14:22:53 Finished semantics/alt_semantics/proofs                        2m31s 843MB
Feb 18 14:22:53 Starting basis/pure
Feb 18 14:25:53 Finished basis/pure                                            2m56s 924MB
Feb 18 14:25:53 Starting translator
Feb 18 14:27:49 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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[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 (21s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                                                   translator (41s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_optimiseTheory                                                                                                                                                     translator (17s)     OK
ml_pmatchTheory                                                                                                                                                       translator (17s)     OK
Starting work on decProgTheory
Starting work on ml_module_demoTheory
Starting work on ml_pmatch_demoTheory
Starting work on ml_translator_demoTheory
ml_translator_demoTheory                                                                                                                                              translator (13s)     OK
Starting work on ml_translator_testTheory
ml_module_demoTheory                                                                                                                                                  translator (15s)     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-1780/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-1780/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 = "??"}
decProgTheory                                                                                                                                                         translator (30s)MKILLED
ml_pmatch_demoTheory                                                                                                                                                  translator (29s)MKILLED