Job 1735

CakeML:c74447249e34aa9bad9962a68ed36b4e86f87b56
  Add a toplevel printing hook and the test [Jan 24 12:55:17]
#856 (printing)
Merging into:fe46ca072678de42c6fdfc32f40eafeb917dab02
  Fix proof broken by HOL changes making more rewrites automatic [Jan 20 00:31:55]
HOL:25791203572c0eaec5a25d436e61053c3571dccd
  Merge with branch 'develop' [Jan 26 22:01:54]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 26 23:52:18 Claimed job
Jan 26 23:52:24 Building HOL
Jan 27 00:02:30 Starting developers
Jan 27 00:02:35 Finished developers                                               4s 102MB
Jan 27 00:02:35 Starting developers/bin
Jan 27 00:02:40 Finished developers/bin                                           5s 670MB
Jan 27 00:02:41 Starting semantics/ffi
Jan 27 00:02:51 Finished semantics/ffi                                           10s 216MB
Jan 27 00:02:51 Starting semantics
Jan 27 00:04:31 Finished semantics                                             1m40s   1GB
Jan 27 00:04:32 Starting semantics/proofs
Jan 27 00:08:26 Finished semantics/proofs                                      3m53s   1GB
Jan 27 00:08:26 Starting semantics/alt_semantics
Jan 27 00:08:39 Finished semantics/alt_semantics                                 13s 355MB
Jan 27 00:08:39 Starting semantics/alt_semantics/proofs
Jan 27 00:11:20 Finished semantics/alt_semantics/proofs                        2m40s 924MB
Jan 27 00:11:20 Starting basis/pure
Jan 27 00:14:36 Finished basis/pure                                            3m15s 765MB
Jan 27 00:14:36 Starting translator
Jan 27 00:16:11 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)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
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 (16s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                     translator (38s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_pmatchTheory                                         translator (16s)     OK
ml_optimiseTheory                                       translator (18s)     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-1735/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-1735/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