Job 1446

CakeML:4762e6f7932683fa7c3dd0a1199b9f03ba5b76aa
  Fix a broken proof [Jan 22 14:58:50]
HOL:bc19c02fccfaad188f632f362b283743827faa72
  Fix another lassie Holmakefile to use right "signal file" [Jan 21 05:07:07]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 22 21:12:31 Claimed job
Jan 22 21:12:37 Building HOL
Jan 22 21:28:21 Starting developers
Jan 22 21:28:26 Finished developers                                               4s  97MB
Jan 22 21:28:26 Starting developers/bin
Jan 22 21:28:33 Finished developers/bin                                           6s   1GB
Jan 22 21:28:33 Starting semantics/ffi
Jan 22 21:28:45 Finished semantics/ffi                                           11s 244MB
Jan 22 21:28:45 Starting semantics
Jan 22 21:30:21 Finished semantics                                             1m35s   1GB
Jan 22 21:30:21 Starting semantics/proofs
Jan 22 21:31:43 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
NTpropertiesTheory                              real:    6s  user:    5s     OK
pegTheory                                       real:    6s  user:    5s     OK
Starting work on pegexecTheory
Starting work on gramPropsTheory
astPropsTheory                                  real:    8s  user:    7s     OK
pegexecTheory                                   real:    2s  user:    2s     OK
namespacePropsTheory                            real:   13s  user:   12s     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                       real:    7s  user:    6s     OK
gramPropsTheory                                 real:   23s  user:   21s     OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                   real:   39s  user:   38s     OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                   real:   34s  user:   32s     OK
evaluatePropsTheory                             real:   25s  user:   24s     OK
typeSysPropsTheory                              real:   28s  user:   26sFAIL<1>
 Saved theorem _____ "type_def_to_ctMap_mem"
 Saved theorem _____ "ctMap_ok_type_defs"
 error in quse /home/cake/oven/regression/cakeml-1446/semantics/proofs/typeSysPropsScript.sml : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 error in load /home/cake/oven/regression/cakeml-1446/semantics/proofs/typeSysPropsScript : HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}
 Proof of 
 
 l v. ALL_DISTINCT (MAP ((x,y). x) l)  ALL_DISTINCT (MAP ((x,y). (x,v)) l)
 
 failed.
 Uncaught exception: HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"}