Job 1248

CakeML:6979fa3359c4f2644288926d9eeaf5fe2c616d71
  Partly fix the translator [Jun 04 20:11:12]
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 20:15:06 Claimed job
Jun 04 20:15:08 Reusing HOL
Jun 04 20:15:55 Starting developers
Jun 04 20:15:59 Finished developers                                               4s  86MB
Jun 04 20:15:59 Starting developers/bin
Jun 04 20:16:07 Finished developers/bin                                           7s   1GB
Jun 04 20:16:07 Starting semantics/ffi
Jun 04 20:16:19 Finished semantics/ffi                                           11s 253MB
Jun 04 20:16:19 Starting semantics
Jun 04 20:17:44 Finished semantics                                             1m25s   1GB
Jun 04 20:17:44 Starting semantics/proofs
Jun 04 20:20:45 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:    8s  user:    7s     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
semanticPrimitivesPropsTheory                   real:   39s  user:   38s     OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                   real:   29s  user:   28s     OK
evaluatePropsTheory                             real:   24s  user:   23s     OK
typeSysPropsTheory                              real:   27s  user:   26s     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:   87s  user:   85sFAIL<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"}