Job 1245

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments [May 25 05:14:54]
#738 (export_update)
Merging into: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 09:10:15 Claimed job
Jun 04 09:10:17 Reusing HOL
Jun 04 09:11:10 Starting developers
Jun 04 09:11:14 Finished developers                                               4s  95MB
Jun 04 09:11:14 Starting developers/bin
Jun 04 09:11:22 Finished developers/bin                                           7s   1GB
Jun 04 09:11:22 Starting semantics/ffi
Jun 04 09:11:34 Finished semantics/ffi                                           11s 227MB
Jun 04 09:11:34 Starting semantics
Jun 04 09:13:01 Finished semantics                                             1m26s   1GB
Jun 04 09:13:01 Starting semantics/proofs
Jun 04 09:13:38 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:   23s  user:   22s     OK
Starting work on cmlPtreeConversionPropsTheory
cmlPtreeConversionPropsTheory                   real:   12s  user:   11sFAIL<1>
 Saved theorem _____ "ConstructorName_OK"
 error in quse /home/cake/oven/regression/cakeml-1245/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-1245/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