Overview

Job 412

CakeML:392961c89db2505438d210e8fb3bc23d57d28b91
  regenerate files with Lem 2018-07-13
#509 (lem-updates)
Merging into:1802ff5409009d31ba5fe8636638bb5fc9c724df
  Fix proof in inferProg
HOL:f243fe78da5dcc426046ce1b6a0f756e6aa524b9
  Hide vim scratch buffer from the list of buffers
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                           8s 224MB
 Starting semantics/ffi
 Finished semantics/ffi                                           59s 296MB
 Starting semantics
 Finished semantics                                             2m18s 852MB
 Starting semantics/proofs
 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