Job 323

CakeML:5b0e7d5130d24f8fe2ac9a5bf8f4536091c4f7b8
  Add resource usage warning to readme and build doc [May 23 15:19:25]
HOL:1c2f967871ae1f61f75a30d037a4100413700554
  Fix pretty-printing bug for large-if-exprs in rator position [May 28 08:02:00]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

May 28 21:30:55 Claimed job
May 28 21:31:15 Building HOL
May 28 21:39:29 Starting developers/bin
May 28 21:40:11 Finished developers/bin                                          41s 925MB
May 28 21:40:11 Starting semantics/ffi
May 28 21:40:51 Finished semantics/ffi                                           38s 410MB
May 28 21:40:51 Starting semantics
May 28 21:42:16 Finished semantics                                             1m24s   1GB
May 28 21:42:17 Starting semantics/proofs
May 28 21:43:16 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../misc]0;Holmake: ~/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-1c2f967871ae1f61f75a30d037a4100413700554/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developersWorking in ../../developers
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../misc]0;Holmake: ../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../ffi]0;Holmake: ../ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/semantics/proofs
Starting work on heap
heap                                                                                                                                                                                 OK
Starting work on astPropsTheory
Starting work on gramPropsTheory
Starting work on semanticPrimitivesPropsTheory
Starting work on typeSoundInvariantsTheory
astPropsTheory                                                                                                                                                                       OK
typeSoundInvariantsTheory                                                                                                                                                            OK
gramPropsTheory                                                                                                                                                                      OK
Starting work on cmlPtreeConversionPropsTheory
semanticPrimitivesPropsTheory                                                                                                                                                        OK
Starting work on evaluatePropsTheory
Starting work on primSemEnvTheory
Starting work on typeSysPropsTheory
primSemEnvTheory                                                                                                                                                                     OK
cmlPtreeConversionPropsTheory                                                                                                                                                        OK
typeSysPropsTheory                                                                                                                                                          FAILED! <1>
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 2308) (THEN1 on line 2304)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Proof of 
 
 mn tenvT specs decls' tenv'.
     type_specs mn tenvT specs decls' tenv' 
     tenv_abbrev_ok tenvT 
     tenv_ok tenv'
 
 failed.
 Failed to prove theorem type_specs_tenv_ok.
evaluatePropsTheory                                                                                                                                                            M-KILLED