Job 1057

CakeML:821c40a8d7939d7e951e716a31cbb6e69cc8db13
  Explain infix scheme [Oct 30 07:26:04]
#695 (ocaml-infixes)
Merging into:dc73bd8f21601e06bdc92eb303865a3992673970
  Merge pull request #694 from CakeML/remove-oom [Oct 13 07:36:28]
HOL:f11debc0b86c4c7bb97d340bf5ace2f75d4c69fd
  Holmake: key monitor function on combination of PID and tag-string [Oct 30 11:27:47]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Oct 30 22:38:02 Claimed job
Oct 30 22:38:09 Building HOL
Oct 30 22:48:27 Starting developers
Oct 30 22:48:30 Finished developers                                               3s 136MB
Oct 30 22:48:31 Starting developers/bin
Oct 30 22:48:36 Finished developers/bin                                           5s 964MB
Oct 30 22:48:36 Starting semantics/ffi
Oct 30 22:48:46 Finished semantics/ffi                                            9s 230MB
Oct 30 22:48:46 Starting semantics
Oct 30 22:50:08 Finished semantics                                             1m22s   1GB
Oct 30 22:50:08 Starting semantics/proofs
Oct 30 22:50:48 FAILED: semantics/proofs
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
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:    5s  user:    4s     OK
Starting work on pegexecTheory
NTpropertiesTheory                              real:    6s  user:    6s     OK
Starting work on gramPropsTheory
astPropsTheory                                  real:    7s  user:    6s     OK
pegexecTheory                                   real:    2s  user:    1s     OK
namespacePropsTheory                            real:   11s  user:   10s     OK
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
typeSoundInvariantsTheory                       real:    5s  user:    5s     OK
gramPropsTheory                                 real:   19s  user:   18s     OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                   real:   25s  user:   24s     OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                   real:   11s  user:   10sFAIL<1>
 MAP TK toks = ptree_fringe pt  ptree_head pt = NN N 
 opv. ptree_Op pt = SOME opv
 
 failed.
 First unsolved sub-goal is
 
 opv. singleSym validMultSym [Lf (TK (SymbolT s),l')] = SOME opv
 
 Failed to prove theorem Ops_OK0.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
evaluatePropsTheory                                                     M-KILLED
typeSysPropsTheory                                                      M-KILLED