Job 1776

CakeML:6bcfea2bfe7ac7b632f2c21ac11f30fd66211e81
  Rename monad constructors in candle_kernel_funs [Feb 17 12:32:12]
#863 (repl)
Merging into:67b312862a2b9919d20a41b16a6599ef4a7635fe
  Merge pull request #855 from CakeML/minor-reheapification [Feb 14 13:06:51]
HOL:b42a44c7c2eceaa7d85097e51c32ac752db13c32
  Change to Define loses ability to write leading !vs. block [Feb 16 10:07:18]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 17 12:37:49 Claimed job
Feb 17 12:37:55 Building HOL
Feb 17 12:47:28 Starting developers
Feb 17 12:47:32 Finished developers                                               4s 154MB
Feb 17 12:47:32 Starting developers/bin
Feb 17 12:47:37 Finished developers/bin                                           4s 674MB
Feb 17 12:47:37 Starting semantics/ffi
Feb 17 12:47:46 Finished semantics/ffi                                            9s 238MB
Feb 17 12:47:47 Starting semantics
Feb 17 12:50:00 Finished semantics                                             2m13s   1GB
Feb 17 12:50:00 Starting semantics/proofs
Feb 17 12:53:40 Finished semantics/proofs                                      3m39s   1GB
Feb 17 12:53:40 Starting semantics/alt_semantics
Feb 17 12:53:56 Finished semantics/alt_semantics                                 16s 477MB
Feb 17 12:53:56 Starting semantics/alt_semantics/proofs
Feb 17 12:56:23 Finished semantics/alt_semantics/proofs                        2m26s 858MB
Feb 17 12:56:23 Starting basis/pure
Feb 17 12:59:35 Finished basis/pure                                            3m11s 884MB
Feb 17 12:59:36 Starting translator
Feb 17 13:00:33 FAILED: translator
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
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 23 directories
Finished $(CAKEMLDIR)/misc                                                                                                                                                           (0.000s) 
Starting work on ml_progTheory
ml_progTheory                                                                                                                                                         translator (20s)     OK
Starting work on ml_translatorTheory
ml_translatorTheory                                                                                                                                                   translator (32s)FAIL<1>
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn:
 between line 1605, character 2 and line 1612, character 41:
 at Defn.parse_quote:
 at boolSyntax.dest_eq(_ty):
 not an "="
 error in quse /home/cug/hk324/cml-regression/cakeml-1776/translator/ml_translatorScript.sml : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1605, character 2 and line 1612, character 41:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 error in load /home/cug/hk324/cml-regression/cakeml-1776/translator/ml_translatorScript : HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1605, character 2 and line 1612, character 41:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}
 Uncaught exception: HOL_ERR {message = "at Defn.Hol_defn:\nbetween line 1605, character 2 and line 1612, character 41:\nat Defn.parse_quote:\nat boolSyntax.dest_eq(_ty):\nnot an \"=\"", origin_function = "xDefine", origin_structure = "TotalDefn"}