Job 322

CakeML:5b0e7d5130d24f8fe2ac9a5bf8f4536091c4f7b8
  Add resource usage warning to readme and build doc [May 23 15:19:25]
HOL:3b740aa3349ed6589cf50e17f47d519833de1964
  tactictoe: abstracting + exporting theorem values for list of theorems [May 23 13:23:15]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

May 23 17:47:40 Claimed job
May 23 17:47:53 Building HOL
May 23 17:59:27 Starting developers/bin
May 23 17:59:38 Finished developers/bin                                           9s 224MB
May 23 17:59:40 Starting semantics/ffi
May 23 18:00:41 Finished semantics/ffi                                           58s 530MB
May 23 18:00:43 Starting semantics
May 23 18:03:03 Finished semantics                                             2m17s   1GB
May 23 18:03:05 Starting semantics/proofs
May 23 18:04:46 FAILED: semantics/proofs
]0;Holmake: .]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-3b740aa3349ed6589cf50e17f47d519833de1964/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-3b740aa3349ed6589cf50e17f47d519833de1964/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../misc]0;Holmake: /scratch/cakeml/regression/HOL-3b740aa3349ed6589cf50e17f47d519833de1964/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-3b740aa3349ed6589cf50e17f47d519833de1964/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