Job 1244

CakeML:22d015799d0aada026d5615a6cb93f81da2f9b62
  Fix for recent HOL breakages [Jun 03 23:57:15]
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 00:05:14 Claimed job
Jun 04 00:05:18 Building HOL
Jun 04 00:19:20 Starting developers
Jun 04 00:19:24 Finished developers                                               4s  80MB
Jun 04 00:19:24 Starting developers/bin
Jun 04 00:19:33 Finished developers/bin                                           7s   1GB
Jun 04 00:19:33 Starting semantics/ffi
Jun 04 00:19:44 Finished semantics/ffi                                           11s 248MB
Jun 04 00:19:45 Starting semantics
Jun 04 00:21:19 Finished semantics                                             1m34s   1GB
Jun 04 00:21:19 Starting semantics/proofs
Jun 04 00:22:03 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 NTpropertiesTheory
Starting work on pegTheory
Starting work on README.md
Starting work on astPropsTheory
README.md                                       real:    0s  user:    0s     OK
Starting work on namespacePropsTheory
pegTheory                                       real:    6s  user:    5s     OK
Starting work on pegexecTheory
NTpropertiesTheory                              real:    7s  user:    6s     OK
Starting work on gramPropsTheory
astPropsTheory                                  real:    8s  user:    7s     OK
pegexecTheory                                   real:    2s  user:    2s     OK
namespacePropsTheory                            real:   12s  user:   11s     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                       real:    7s  user:    6s     OK
gramPropsTheory                                 real:   22s  user:   21s     OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                   real:   12s  user:   11sFAIL<1>
 Saved theorem _____ "ConstructorName_OK"
 error in quse /home/cake/oven/regression/cakeml-1244/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-1244/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