Job 1743

CakeML:9e90ae98b5b5634a5987feccd20207bcef46c03c
  Handle failure more gracefully in printTweaks [Jan 27 11:43:21]
#856 (printing)
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:32:14 Claimed job
Jan 28 13:32:16 Reusing HOL
Jan 28 13:32:55 Starting developers
Jan 28 13:33:00 Finished developers                                               4s  86MB
Jan 28 13:33:00 Starting developers/bin
Jan 28 13:33:05 Finished developers/bin                                           5s 670MB
Jan 28 13:33:06 Starting semantics/ffi
Jan 28 13:33:16 Finished semantics/ffi                                           10s 208MB
Jan 28 13:33:16 Starting semantics
Jan 28 13:34:46 Finished semantics                                             1m29s   1GB
Jan 28 13:34:46 Starting semantics/proofs
Jan 28 13:38:39 Finished semantics/proofs                                      3m52s 863MB
Jan 28 13:38:39 Starting semantics/alt_semantics
Jan 28 13:38:53 Finished semantics/alt_semantics                                 13s 353MB
Jan 28 13:38:53 Starting semantics/alt_semantics/proofs
Jan 28 13:41:36 Finished semantics/alt_semantics/proofs                        2m43s 955MB
Jan 28 13:41:36 Starting basis/pure
Jan 28 13:42:34 Finished basis/pure                                              57s 694MB
Jan 28 13:42:35 Starting translator
Jan 28 13:44:10 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 (39s)     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_module_demoTheory                                    translator (14s)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 /home/cake/oven/regression/cakeml-1743/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 /home/cake/oven/regression/cakeml-1743/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 (14s)MKILLED
ml_pmatch_demoTheory                                    translator (14s)MKILLED
ml_translator_demoTheory                                translator (14s)MKILLED