Job 1869

CakeML:4c966fba47c4550a982b3512dc6a08cc1ee4f7da
  Translate new mlmap functions [Apr 12 08:48:57]
#881 (mlmap-additions)
Merging into:915403669818aaaea2c42cd400fad0542de3fa99
  Merge pull request #878 from CakeML/array-appi-fix [Apr 20 08:36:39]
HOL:cb44cc2412d08a2baf1dd127ba6dc5f565e2834b
  "orthogonal edge routing" style of core theory hierarchy graph [Apr 14 03:45:39]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 20 14:59:55 Claimed job
Apr 20 14:59:57 Reusing HOL
Apr 20 15:00:09 Starting developers
Apr 20 15:00:14 Finished developers                                               4s 162MB
Apr 20 15:00:14 Starting developers/bin
Apr 20 15:01:11 Finished developers/bin                                          56s   1GB
Apr 20 15:01:11 Starting semantics/ffi
Apr 20 15:01:21 Finished semantics/ffi                                            9s 235MB
Apr 20 15:01:21 Starting semantics
Apr 20 15:03:18 Finished semantics                                             1m57s   1GB
Apr 20 15:03:18 Starting semantics/proofs
Apr 20 15:07:25 Finished semantics/proofs                                      4m06s   4GB
Apr 20 15:07:25 Starting semantics/alt_semantics
Apr 20 15:07:49 Finished semantics/alt_semantics                                 23s 555MB
Apr 20 15:07:49 Starting semantics/alt_semantics/proofs
Apr 20 15:10:47 Finished semantics/alt_semantics/proofs                        2m58s   1GB
Apr 20 15:10:47 Starting basis/pure
Apr 20 15:10:58 FAILED: basis/pure
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/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanned 21 directories
Starting work on README.md
Starting work on mllistTheory
Starting work on mloptionTheory
Starting work on mlmapTheory
README.md                                                           (0s)     OK
mlmapTheory                                                         (8s)FAIL<1>
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 57, character 2 and line 58, character 50:
 at Defn.parse_quote:
 at Term.prim_mk_const:
 "unionWithKey" not found in theory "balanced_map"
 error in quse /home/cug/hk324/cml-regression/cakeml-1869/basis/pure/mlmapScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 57, character 2 and line 58, character 50:\nat Defn.parse_quote:\nat Term.prim_mk_const:\n\"unionWithKey\" not found in theory \"balanced_map\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1869/basis/pure/mlmapScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 57, character 2 and line 58, character 50:\nat Defn.parse_quote:\nat Term.prim_mk_const:\n\"unionWithKey\" not found in theory \"balanced_map\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 57, character 2 and line 58, character 50:\nat Defn.parse_quote:\nat Term.prim_mk_const:\n\"unionWithKey\" not found in theory \"balanced_map\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
mllistTheory                                                        (8s)MKILLED
mloptionTheory                                                      (9s)MKILLED