Job 1746

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:a1eeb53dfc767d417d825457463d269718d87ee4
  Holmake: update mlton build info for change in 244fc47a4 [Jan 31 00:25:43]
Machine:oven3+4.19.67.1.amd64-smp+

Jan 31 04:57:28 Claimed job
Jan 31 04:57:40 Building+HOL
Jan 31 05:16:54 Starting+developers
Jan 31 05:17:02 Finished+developers++++++++++++++++++++++++++++++++++++++++8.28+162164
Jan 31 05:17:02 Starting+developers/bin
Jan 31 05:17:14 Finished+developers/bin++++++++++++++++++++++++++++++++++++11.01+685000
Jan 31 05:17:14 Starting+semantics/ffi
Jan 31 05:17:36 Finished+semantics/ffi+++++++++++++++++++++++++++++++++++++21.98+265960
Jan 31 05:17:36 Starting+semantics
Jan 31 05:21:30 Finished+semantics+++++++++++++++++++++++++++++++++++++++++233.51+1167904
Jan 31 05:21:30 Starting+semantics/proofs
Jan 31 05:29:29 Finished+semantics/proofs++++++++++++++++++++++++++++++++++478.25+1013696
Jan 31 05:29:29 Starting+semantics/alt_semantics
Jan 31 05:30:02 Finished+semantics/alt_semantics+++++++++++++++++++++++++++32.66+426548
Jan 31 05:30:02 Starting+semantics/alt_semantics/proofs
Jan 31 05:35:25 Finished+semantics/alt_semantics/proofs++++++++++++++++++++323.25+1183952
Jan 31 05:35:25 Starting+basis/pure
Jan 31 05:41:25 Finished+basis/pure++++++++++++++++++++++++++++++++++++++++358.76+904980
Jan 31 05:41:25 Starting+translator
Jan 31 05:44:28 FAILED:+translator
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/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
Finished $(CAKEMLDIR)/misc                                                                                                                                                                                                          (0.000s) 
Starting work on README.md
Starting work on ml_progTheory
README.md                                                                                                                                                                                                            translator  (0s)     OK
ml_progTheory                                                                                                                                                                                                        translator (35s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                                                                                                  translator (73s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_optimiseTheory                                                                                                                                                                                                    translator (33s)     OK
ml_pmatchTheory                                                                                                                                                                                                      translator (34s)     OK
Starting work on decProgTheory
Starting work on ml_module_demoTheory
Starting work on ml_pmatch_demoTheory
Starting work on ml_translator_demoTheory
ml_module_demoTheory                                                                                                                                                                                                 translator (25s)FAIL<1>
 Saved theorem _______ "EVEN_TYPE_def"
 Attempting proof of: EqualityType EVEN_TYPE
 .. done EqualityType proof.
 Adding type :even to module Even.
 error in quse /root/regression/cakeml-1746/translator/ml_module_demoScript.sml : HOL_ERR {message = "Malformed theorem-binding specifier: @temp[[ zero_code ]]", origin_function = "resolve_storename", origin_structure = "boolLib"}
 error in load /root/regression/cakeml-1746/translator/ml_module_demoScript : HOL_ERR {message = "Malformed theorem-binding specifier: @temp[[ zero_code ]]", origin_function = "resolve_storename", origin_structure = "boolLib"}
 Saved theorem _______ "nsLookup_ml_module_demo_env_0_pfun_eqs"
 Translating zero
 Failed translation: zero
 Uncaught exception: HOL_ERR {message = "Malformed theorem-binding specifier: @temp[[ zero_code ]]", origin_function = "resolve_storename", origin_structure = "boolLib"}
decProgTheory                                                                                                                                                                                                        translator (27s)MKILLED
ml_pmatch_demoTheory                                                                                                                                                                                                 translator (26s)MKILLED
ml_translator_demoTheory                                                                                                                                                                                             translator (26s)MKILLED