Job 1739

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:d537de783f9b4ddec728931f42b2fd7882e487f3
  Point L3 equivalence proofs to new snapshot in HOL repo [Jan 26 23:30:25]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 27 06:32:03 Claimed job
Jan 27 06:32:08 Reusing HOL
Jan 27 06:32:46 Starting developers
Jan 27 06:32:51 Finished developers                                               4s  87MB
Jan 27 06:32:52 Starting developers/bin
Jan 27 06:32:57 Finished developers/bin                                           5s 670MB
Jan 27 06:32:57 Starting semantics/ffi
Jan 27 06:33:07 Finished semantics/ffi                                            9s 219MB
Jan 27 06:33:07 Starting semantics
Jan 27 06:34:36 Finished semantics                                             1m28s   1GB
Jan 27 06:34:37 Starting semantics/proofs
Jan 27 06:38:33 Finished semantics/proofs                                      3m55s 949MB
Jan 27 06:38:33 Starting semantics/alt_semantics
Jan 27 06:38:46 Finished semantics/alt_semantics                                 13s 380MB
Jan 27 06:38:47 Starting semantics/alt_semantics/proofs
Jan 27 06:41:27 Finished semantics/alt_semantics/proofs                        2m40s 744MB
Jan 27 06:41:28 Starting basis/pure
Jan 27 06:42:25 Finished basis/pure                                              57s 721MB
Jan 27 06:42:26 Starting translator
Jan 27 06:43:58 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_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)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-1739/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-1739/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 (13s)MKILLED
ml_pmatch_demoTheory                                    translator (14s)MKILLED