Job 1249

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments [May 25 05:14:54]
#738 (export_update)
Merging into: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 05 17:30:44 Claimed job
Jun 05 17:30:50 Reusing HOL
Jun 05 17:31:36 Starting developers
Jun 05 17:31:40 Finished developers                                               4s  99MB
Jun 05 17:31:41 Starting developers/bin
Jun 05 17:31:48 Finished developers/bin                                           7s   1GB
Jun 05 17:31:49 Starting semantics/ffi
Jun 05 17:32:00 Finished semantics/ffi                                           11s 239MB
Jun 05 17:32:00 Starting semantics
Jun 05 17:33:25 Finished semantics                                             1m24s   1GB
Jun 05 17:33:25 Starting semantics/proofs
Jun 05 17:36:27 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:    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:   38s  user:   37s     OK
Starting work on evaluatePropsTheory
Starting work on typeSysPropsTheory
cmlPtreeConversionPropsTheory                   real:   29s  user:   28s     OK
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"}