Job 650

CakeML:966ca82f5f3d780f4ae4badc6f0065eb896ce3be
  Commit generated README.md [Dec 25 20:48:29]
HOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748
  Fix bug: TypeBase.simpls_of not being filled in on load [Dec 21 04:04:45]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Dec 25 21:41:30 Claimed job
Dec 25 21:41:36 Reusing HOL
Dec 25 21:41:47 Starting developers
Dec 25 21:41:49 Finished developers                                               0s  20MB
Dec 25 21:41:50 Starting developers/bin
Dec 25 21:42:25 Finished developers/bin                                          34s 201MB
Dec 25 21:42:26 Starting semantics/ffi
Dec 25 21:42:38 Finished semantics/ffi                                           11s 223MB
Dec 25 21:42:39 Starting semantics
Dec 25 21:44:04 Finished semantics                                             1m24s   1GB
Dec 25 21:44:05 Starting semantics/proofs
Dec 25 21:45:24 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ~/regression/cakeml-650/developers]0;Holmake: ~/regression/cakeml-650/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-650/misc]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-650/misc]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-89daca206b2ad7a8e43f3a59c20a178cc04d7748/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-650/misc]0;Holmake: ~/regression/cakeml-650/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-650/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-650/misc]0;Holmake: ~/regression/cakeml-650/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 astPropsTheory
Starting work on gramPropsTheory
Starting work on namespacePropsTheory
Starting work on README.md
README.md                                                                                                  OK
astPropsTheory                                                                                             OK
namespacePropsTheory                                                                                       OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
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 /home/myreen/regression/cakeml-650/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