Job 412

CakeML:392961c89db2505438d210e8fb3bc23d57d28b91
  regenerate files with Lem 2018-07-13 [Aug 06 10:31:27]
#509 (lem-updates)
Merging into:1802ff5409009d31ba5fe8636638bb5fc9c724df
  Fix proof in inferProg [Aug 08 13:46:34]
HOL:f243fe78da5dcc426046ce1b6a0f756e6aa524b9
  Hide vim scratch buffer from the list of buffers [Aug 08 03:52:48]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Aug 08 14:08:19 Claimed job
Aug 08 14:08:29 Building HOL
Aug 08 14:20:57 Starting developers/bin
Aug 08 14:21:07 Finished developers/bin                                           8s 224MB
Aug 08 14:21:09 Starting semantics/ffi
Aug 08 14:22:10 Finished semantics/ffi                                           59s 296MB
Aug 08 14:22:12 Starting semantics
Aug 08 14:24:33 Finished semantics                                             2m18s 852MB
Aug 08 14:24:35 Starting semantics/proofs
Aug 08 14:26:25 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-f243fe78da5dcc426046ce1b6a0f756e6aa524b9/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developers[1mWorking in ../../developers[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
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../ffi]0;Holmake: ../ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
Starting work on heap
heap                                                                                                                                                      OK
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
astPropsTheory                                                                                                                                            OK
typeSoundInvariantsTheory                                                                                                                                 OK
gramPropsTheory                                                                                                                                           OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                                                                                                                             OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                                                                                                                             OK
evaluatePropsTheory                                                                                                                                       OK
typeSysPropsTheory                                                                                                                                        OK
Starting work on primSemEnvTheory
Starting work on weakeningTheory
primSemEnvTheory                                                                                                                                 FAILED! <1>
 <<HOL message: Created theory "primSemEnv">>
 error in quse /scratch/cakeml/regression/cakeml-412/semantics/proofs/primSemEnvScript.sml : HOL_ERR {message = "lhs and rhs have different types", origin_function = "mk_eq", origin_structure = "boolSyntax"}
 error in load primSemEnvScript : HOL_ERR {message = "lhs and rhs have different types", origin_function = "mk_eq", origin_structure = "boolSyntax"}
 Uncaught exception: HOL_ERR {message = "lhs and rhs have different types", origin_function = "mk_eq", origin_structure = "boolSyntax"}
weakeningTheory                                                                                                                                     M-KILLED