Job 593

CakeML:dfb6db573390c9831cc3ba0c2a5c18aa46848de9
  Reconcile thm names that differed in DB and ML-level names [Nov 29 06:02:06]
#569 (theorem)
Merging into:59886cd0205c1d5d943ef10a26890f79b515b68f
  Merge pull request #561 from CakeML/print-types [Nov 26 04:25:18]
HOL:f47304e1a773d1edc8606a0bda7299f8e926d11a
  Merge branch 'vars-and-variants' into master [Nov 28 21:10:26]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 29 06:23:43 Claimed job
Nov 29 06:24:02 Reusing HOL
Nov 29 06:24:10 Starting developers/bin
Nov 29 06:24:42 Finished developers/bin                                          31s 201MB
Nov 29 06:24:43 Starting semantics/ffi
Nov 29 06:24:53 Finished semantics/ffi                                            9s 266MB
Nov 29 06:24:54 Starting semantics
Nov 29 06:25:34 FAILED: semantics
]0;Holmake: .]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: .]0;Holmake: ../developers]0;Holmake: ../developers[1mWorking in $(CAKEMLDIR)/developers[0m
Starting work on readme_gen
readme_gen                                                                                                 OK
Starting work on README.md
README.md                                                                                                  OK
]0;Holmake: .]0;Holmake: ../misc]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f47304e1a773d1edc8606a0bda7299f8e926d11a/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../misc]0;Holmake: ../misc[1mWorking in $(CAKEMLDIR)/misc[0m
Starting work on README.md
Starting work on miscTheory
Starting work on alist_treeTheory
README.md                                                                                                  OK
alist_treeTheory                                                                                           OK
miscTheory                                                                                                 OK
]0;Holmake: .]0;Holmake: ffi]0;Holmake: ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/semantics[0m
Starting work on addancs
Starting work on heap
Starting work on README.md
README.md                                                                                                  OK
addancs                                                                                                    OK
Starting work on astScript
Starting work on namespaceScript
Starting work on tokensScript
namespaceScript                                                                                            OK
tokensScript                                                                                               OK
astScript                                                                                                  OK
heap                                                                                                       OK
Starting work on fpSemTheory
Starting work on namespaceTheory
Starting work on tokensTheory
fpSemTheory                                                                                                OK
namespaceTheory                                                                                            OK
Starting work on astTheory
tokensTheory                                                                                               OK
Starting work on gramTheory
Starting work on tokenUtilsTheory
Starting work on lexer_funTheory
astTheory                                                                                                  OK
Starting work on semanticPrimitivesTheory
lexer_funTheory                                                                                   FAILED! <1>
   Grammar-deltas:
     overload_on("skip_comment_tupled")
   invalidated by DelConstant(lexer_fun$skip_comment_tupled)>>
 Saved definition __ "skip_comment_def"
 Saved induction ___ "skip_comment_ind"
 error in quse /home/myreen/regression/cakeml-593/semantics/lexer_funScript.sml : Fail "Static Errors"
 error in load lexer_funScript : Fail "Static Errors"
 Saved theorem _____ "skip_comment_thm"
 /home/myreen/regression/cakeml-593/semantics/lexer_funScript.sml:129: error: ; expected but , was found
 Uncaught exception: Fail "Static Errors"
gramTheory                                                                                           M-KILLED
tokenUtilsTheory                                                                                     M-KILLED
semanticPrimitivesTheory                                                                             M-KILLED