Job 1738

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: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:08:09 Claimed job
Jan 27 06:08:12 Building HOL
Jan 27 06:18:16 Starting developers
Jan 27 06:18:20 Finished developers                                               4s 166MB
Jan 27 06:18:21 Starting developers/bin
Jan 27 06:18:26 Finished developers/bin                                           5s 670MB
Jan 27 06:18:26 Starting semantics/ffi
Jan 27 06:18:37 Finished semantics/ffi                                           10s 216MB
Jan 27 06:18:37 Starting semantics
Jan 27 06:20:35 Finished semantics                                             1m57s 885MB
Jan 27 06:20:35 Starting semantics/proofs
Jan 27 06:24:32 Finished semantics/proofs                                      3m56s   1GB
Jan 27 06:24:32 Starting semantics/alt_semantics
Jan 27 06:24:47 Finished semantics/alt_semantics                                 14s 394MB
Jan 27 06:24:47 Starting semantics/alt_semantics/proofs
Jan 27 06:27:27 Finished semantics/alt_semantics/proofs                        2m39s 899MB
Jan 27 06:27:27 Starting basis/pure
Jan 27 06:30:29 Finished basis/pure                                            3m01s 867MB
Jan 27 06:30:29 Starting translator
Jan 27 06:32:02 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 (37s)     OK
Starting work on ml_optimiseTheory
Starting work on ml_pmatchTheory
ml_optimiseTheory                                       translator (16s)     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-1738/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-1738/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"}
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-1738/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-1738/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