Job 1779

CakeML:8d561d6e716a58c469481107541f2ab9ef8007fa
  Update some definitions that wanted leading universals [Feb 17 23:44:30]
HOL:b42a44c7c2eceaa7d85097e51c32ac752db13c32
  Change to Define loses ability to write leading !vs. block [Feb 16 10:07:18]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 17 23:48:22 Claimed job
Feb 17 23:48:27 Building HOL
Feb 17 23:57:38 Starting developers
Feb 17 23:57:41 Finished developers                                               2s 116MB
Feb 17 23:57:41 Starting developers/bin
Feb 17 23:57:47 Finished developers/bin                                           5s 675MB
Feb 17 23:57:47 Starting semantics/ffi
Feb 17 23:57:56 Finished semantics/ffi                                            8s 296MB
Feb 17 23:57:56 Starting semantics
Feb 18 00:00:10 Finished semantics                                             2m13s   1GB
Feb 18 00:00:10 Starting semantics/proofs
Feb 18 00:04:00 Finished semantics/proofs                                      3m49s   2GB
Feb 18 00:04:00 Starting semantics/alt_semantics
Feb 18 00:04:18 Finished semantics/alt_semantics                                 18s 632MB
Feb 18 00:04:18 Starting semantics/alt_semantics/proofs
Feb 18 00:07:14 Finished semantics/alt_semantics/proofs                        2m55s   1GB
Feb 18 00:07:14 Starting basis/pure
Feb 18 00:11:53 Finished basis/pure                                            4m38s   1GB
Feb 18 00:11:53 Starting translator
Feb 18 00:15:18 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 (34s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory            translator (70s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                translator (30s)     OK
ml_optimiseTheory              translator (31s)     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 (23s)     OK
Starting work on ml_translator_testTheory
ml_module_demoTheory           translator (27s)     OK
ml_translator_testTheory       translator (29s)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/myreen/regression/cakeml-1779/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/myreen/regression/cakeml-1779/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 (56s)MKILLED
ml_pmatch_demoTheory           translator (56s)MKILLED