Job 1744

CakeML:874bb72cf49d4a806eb88215b31da518ea5352f8
  Delay building of L3 equivalence proofs until needed [Jan 25 23:29:04]
#858 (asl-equiv)
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:44:12 Claimed job
Jan 28 13:44:13 Reusing HOL
Jan 28 13:44:52 Starting developers
Jan 28 13:44:57 Finished developers                                               4s 119MB
Jan 28 13:44:57 Starting developers/bin
Jan 28 13:45:03 Finished developers/bin                                           5s 670MB
Jan 28 13:45:03 Starting semantics/ffi
Jan 28 13:45:14 Finished semantics/ffi                                           10s 192MB
Jan 28 13:45:14 Starting semantics
Jan 28 13:46:44 Finished semantics                                             1m30s   1GB
Jan 28 13:46:44 Starting semantics/proofs
Jan 28 13:50:37 Finished semantics/proofs                                      3m52s   1GB
Jan 28 13:50:37 Starting semantics/alt_semantics
Jan 28 13:50:50 Finished semantics/alt_semantics                                 13s 321MB
Jan 28 13:50:50 Starting semantics/alt_semantics/proofs
Jan 28 13:53:33 Finished semantics/alt_semantics/proofs                        2m41s 796MB
Jan 28 13:53:33 Starting basis/pure
Jan 28 13:54:27 Finished basis/pure                                              53s 789MB
Jan 28 13:54:27 Starting translator
Jan 28 13:56:01 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_pmatchTheory                                         translator (17s)     OK
ml_optimiseTheory                                       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-1744/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-1744/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