Job 1247

CakeML:5348308f7ed9befea24011b4f2f4ad0baa4bb49e
  Fix two scripts for changes to HOL [Jun 04 13:48:09]
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 14:00:02 Claimed job
Jun 04 14:00:06 Reusing HOL
Jun 04 14:00:53 Starting developers
Jun 04 14:00:57 Finished developers                                               4s 116MB
Jun 04 14:00:57 Starting developers/bin
Jun 04 14:01:05 Finished developers/bin                                           7s   1GB
Jun 04 14:01:05 Starting semantics/ffi
Jun 04 14:01:16 Finished semantics/ffi                                           11s 243MB
Jun 04 14:01:16 Starting semantics
Jun 04 14:02:42 Finished semantics                                             1m25s   1GB
Jun 04 14:02:42 Starting semantics/proofs
Jun 04 14:05:47 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:    7s  user:    6s     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:   29s  user:   28s     OK
semanticPrimitivesPropsTheory                   real:   41s  user:   39s     OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
evaluatePropsTheory                             real:   24s  user:   23s     OK
typeSysPropsTheory                              real:   28s  user:   27s     OK
Starting work on primSemEnvTheory
Starting work on weakeningTheory
weakeningTheory                                 real:   11s  user:   10s     OK
primSemEnvTheory                                real:   12s  user:   11s     OK
Starting work on typeSoundTheory
typeSoundTheory                                 real:   89s  user:   87sFAIL<1>
         | Rerr (Rraise err_v) =>
           type_v 0 ctMap' tenvS' err_v Texn 
           type_sound_invariant st' env ctMap' tenvS'  tenv
         | Rerr (Rabort Rtype_error) => F
         | Rerr (Rabort Rtimeout_error) => T
         | Rerr (Rabort (Rffi_error v4)) => T
 
 failed.
 Failed to prove theorem decs_type_sound_no_check.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 2280) (THEN1 on line 2285) (THEN1 on line 2293) (THEN1 on line 2399) (THEN1 on line 2454)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}