Job 1246

CakeML:4cf05f7d09cb669d61fdb949d60f10b7ac8ca44b
  Fix pegSound for recent HOL changes [Jun 04 00:02:53]
HOL:ac7497223d5845f2709250fa8fdcb566cbc2e1ae
  emacs-mode: make regexp searching case-sensitive; SOME not a q'fier [Jun 03 04:25:22]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 04 12:55:04 Claimed job
Jun 04 12:55:06 Reusing HOL
Jun 04 12:55:53 Starting developers
Jun 04 12:55:57 Finished developers                                               4s 103MB
Jun 04 12:55:57 Starting developers/bin
Jun 04 12:56:05 Finished developers/bin                                           7s   1GB
Jun 04 12:56:05 Starting semantics/ffi
Jun 04 12:56:17 Finished semantics/ffi                                           11s 227MB
Jun 04 12:56:17 Starting semantics
Jun 04 12:57:42 Finished semantics                                             1m25s   1GB
Jun 04 12:57:42 Starting semantics/proofs
Jun 04 12:58:20 FAILED: semantics/proofs
Scanning $(CAKEMLDIR)/developers
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Starting work on README.md
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on namespacePropsTheory
README.md                                       real:    0s  user:    0s     OK
astPropsTheory                                  real:    8s  user:    7s     OK
namespacePropsTheory                            real:   12s  user:   11s     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                       real:    7s  user:    6s     OK
gramPropsTheory                                 real:   24s  user:   23s     OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                   real:   12s  user:   11sFAIL<1>
 Saved theorem _____ "ConstructorName_OK"
 error in quse /home/cake/oven/regression/cakeml-1246/semantics/proofs/cmlPtreeConversionPropsScript.sml : HOL_ERR {message = "no solution found (THEN1 on line 396)", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /home/cake/oven/regression/cakeml-1246/semantics/proofs/cmlPtreeConversionPropsScript : HOL_ERR {message = "no solution found (THEN1 on line 396)", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Saved theorem _____ "Ops_OK0"
 Proof of 
 
 l1 l2. MAP TK l1 = MAP TK l2  l1 = l2
 
 failed.
 Uncaught exception: HOL_ERR {message = "no solution found (THEN1 on line 396)", origin_function = "FOL_FIND", origin_structure = "folTools"}
semanticPrimitivesPropsTheory                                           M-KILLED