Job 1777

CakeML: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 13:00:34 Claimed job
Feb 17 13:00:36 Reusing HOL
Feb 17 13:00:48 Starting developers
Feb 17 13:00:53 Finished developers                                               4s 138MB
Feb 17 13:00:53 Starting developers/bin
Feb 17 13:00:57 Finished developers/bin                                           4s 675MB
Feb 17 13:00:57 Starting semantics/ffi
Feb 17 13:01:07 Finished semantics/ffi                                            9s 239MB
Feb 17 13:01:07 Starting semantics
Feb 17 13:03:10 Finished semantics                                             2m03s   1GB
Feb 17 13:03:11 Starting semantics/proofs
Feb 17 13:06:51 Finished semantics/proofs                                      3m40s   1GB
Feb 17 13:06:51 Starting semantics/alt_semantics
Feb 17 13:07:08 Finished semantics/alt_semantics                                 16s 491MB
Feb 17 13:07:08 Starting semantics/alt_semantics/proofs
Feb 17 13:09:36 Finished semantics/alt_semantics/proofs                        2m28s 849MB
Feb 17 13:09:36 Starting basis/pure
Feb 17 13:10:39 Finished basis/pure                                            1m02s 907MB
Feb 17 13:10:39 Starting translator
Feb 17 13:11:35 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)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 23 directories
Finished $(CAKEMLDIR)/misc                                                                                                                                                           (0.000s) 
Starting work on README.md
Starting work on ml_progTheory
README.md                                                                                                                                                             translator  (0s)     OK
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-1777/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-1777/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"}