Job 1742

CakeML:b6ce1417ef4a3913736824d1853fa54db032c681
  Merge branch 'master' into minor-reheapification [Jan 21 05:38:01]
#855 (minor-reheapification)
Merging into:fe46ca072678de42c6fdfc32f40eafeb917dab02
  Fix proof broken by HOL changes making more rewrites automatic [Jan 20 00:31:55]
HOL:a6997b93e871c1306b82caf1f7333e32e21c4db0
  Reinstate the old xDefine and tDefine functions (at least in bossLib) [Jan 28 05:26:17]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 28 13:08:16 Claimed job
Jan 28 13:08:23 Building HOL
Jan 28 13:18:24 Starting developers
Jan 28 13:18:29 Finished developers                                               4s  64MB
Jan 28 13:18:29 Starting developers/bin
Jan 28 13:18:34 Finished developers/bin                                           5s 670MB
Jan 28 13:18:35 Starting semantics/ffi
Jan 28 13:18:45 Finished semantics/ffi                                           10s 227MB
Jan 28 13:18:45 Starting semantics
Jan 28 13:20:44 Finished semantics                                             1m58s 936MB
Jan 28 13:20:44 Starting semantics/proofs
Jan 28 13:24:37 Finished semantics/proofs                                      3m52s   1GB
Jan 28 13:24:37 Starting semantics/alt_semantics
Jan 28 13:24:52 Finished semantics/alt_semantics                                 14s 408MB
Jan 28 13:24:52 Starting semantics/alt_semantics/proofs
Jan 28 13:27:32 Finished semantics/alt_semantics/proofs                        2m39s   1GB
Jan 28 13:27:32 Starting basis/pure
Jan 28 13:30:39 Finished basis/pure                                            3m06s 761MB
Jan 28 13:30:39 Starting translator
Jan 28 13:32:13 FAILED: translator
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Finished $(CAKEMLDIR)/misc                                             (0.000s) 
Starting work on README.md
Starting work on ml_progTheory
README.md                                               translator  (0s)     OK
ml_progTheory                                           translator (17s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                     translator (38s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_optimiseTheory                                       translator (16s)     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)FAIL<1>
 Adding type : list.
 Adding type : # 
 Attempting proof of: EqualityType (PAIR_TYPE b c)
 .. done EqualityType proof.
 Adding type : # .
 Translating part
 error in quse /home/cake/oven/regression/cakeml-1742/translator/ml_translator_demoScript.sml : HOL_ERR {message = "Malformed theorem-binding specifier: @temp[[ part_code ]]", origin_function = "resolve_storename", origin_structure = "boolLib"}
 error in load /home/cake/oven/regression/cakeml-1742/translator/ml_translator_demoScript : HOL_ERR {message = "Malformed theorem-binding specifier: @temp[[ part_code ]]", origin_function = "resolve_storename", origin_structure = "boolLib"}
 Failed translation: !
 Uncaught exception: HOL_ERR {message = "Malformed theorem-binding specifier: @temp[[ part_code ]]", origin_function = "resolve_storename", origin_structure = "boolLib"}
decProgTheory                                           translator (14s)MKILLED
ml_module_demoTheory                                    translator (14s)MKILLED
ml_pmatch_demoTheory                                    translator (14s)MKILLED