Job 410

CakeML:392961c89db2505438d210e8fb3bc23d57d28b91
  regenerate files with Lem 2018-07-13 [Aug 06 10:31:27]
#509 (lem-updates)
Merging into:1b5f8be3242a8a1d13d1289f21c06650fb5eb463
  Update translator for new length check [Aug 06 19:03:49]
HOL:f243fe78da5dcc426046ce1b6a0f756e6aa524b9
  Hide vim scratch buffer from the list of buffers [Aug 08 03:52:48]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Aug 08 05:04:33 Claimed job
Aug 08 05:04:42 Building HOL
Aug 08 05:17:07 Starting developers/bin
Aug 08 05:17:17 Finished developers/bin                                           8s 224MB
Aug 08 05:17:19 Starting semantics/ffi
Aug 08 05:18:21 Finished semantics/ffi                                           59s 441MB
Aug 08 05:18:23 Starting semantics
Aug 08 05:20:50 Finished semantics                                             2m24s 946MB
Aug 08 05:20:52 Starting semantics/proofs
Aug 08 05:22:40 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-410/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