Job 1388

CakeML:8896e36a51c9aa46e6a4b849a3351ddc1398e829
  Fix parsing problems in word_to_stackProof due to ancestry changes [Nov 08 23:34:32]
HOL:0c45436d2e80652f7fd2c0c6c22230f194a0d238
  Fix Unicode violation in previous [Nov 06 07:17:15]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Nov 09 02:00:41 Claimed job
Nov 09 02:00:43 Reusing HOL
Nov 09 02:01:30 Starting developers
Nov 09 02:01:34 Finished developers                                               4s 109MB
Nov 09 02:01:35 Starting developers/bin
Nov 09 02:01:41 Finished developers/bin                                           6s   1GB
Nov 09 02:01:42 Starting semantics/ffi
Nov 09 02:01:53 Finished semantics/ffi                                           10s 266MB
Nov 09 02:01:53 Starting semantics
Nov 09 02:03:20 Finished semantics                                             1m26s 944MB
Nov 09 02:03:20 Starting semantics/proofs
Nov 09 02:06:54 Finished semantics/proofs                                      3m33s   1GB
Nov 09 02:06:54 Starting semantics/alt_semantics
Nov 09 02:07:03 Finished semantics/alt_semantics                                  8s 289MB
Nov 09 02:07:03 Starting semantics/alt_semantics/proofs
Nov 09 02:09:19 Finished semantics/alt_semantics/proofs                        2m15s 796MB
Nov 09 02:09:19 Starting basis/pure
Nov 09 02:10:10 Finished basis/pure                                              51s 775MB
Nov 09 02:10:10 Starting translator
Nov 09 02:12:56 Finished translator                                            2m45s   1GB
Nov 09 02:12:56 Starting compiler/parsing
Nov 09 02:14:10 Finished compiler/parsing                                      1m14s   3GB
Nov 09 02:14:11 Starting characteristic
Nov 09 02:20:23 Finished characteristic                                        6m11s   2GB
Nov 09 02:20:23 Starting translator/monadic
Nov 09 02:22:05 Finished translator/monadic                                    1m41s   1GB
Nov 09 02:22:05 Starting basis
Nov 09 02:58:40 Finished basis                                                36m34s  13GB
Nov 09 02:58:40 Starting compiler/inference
Nov 09 02:59:44 Finished compiler/inference                                    1m04s   1GB
Nov 09 02:59:45 Starting compiler/backend/reg_alloc
Nov 09 03:00:51 Finished compiler/backend/reg_alloc                            1m06s   1GB
Nov 09 03:00:51 Starting compiler/backend/gc
Nov 09 03:04:22 Finished compiler/backend/gc                                   3m30s   2GB
Nov 09 03:04:22 Starting compiler/backend
Nov 09 03:09:12 Finished compiler/backend                                      4m49s   4GB
Nov 09 03:09:12 Starting compiler/encoders/asm
Nov 09 03:09:35 Finished compiler/encoders/asm                                   22s 669MB
Nov 09 03:09:35 Starting compiler/encoders/x64
Nov 09 03:10:01 Finished compiler/encoders/x64                                   26s   1GB
Nov 09 03:10:01 Starting compiler/encoders/arm7
Nov 09 03:10:55 Finished compiler/encoders/arm7                                  53s   1GB
Nov 09 03:10:55 Starting compiler/encoders/arm8
Nov 09 03:11:09 Finished compiler/encoders/arm8                                  13s 659MB
Nov 09 03:11:09 Starting compiler/encoders/mips
Nov 09 03:11:27 Finished compiler/encoders/mips                                  17s   1GB
Nov 09 03:11:27 Starting compiler/encoders/riscv
Nov 09 03:11:43 Finished compiler/encoders/riscv                                 15s   1GB
Nov 09 03:11:43 Starting compiler/encoders/ag32
Nov 09 03:12:01 Finished compiler/encoders/ag32                                  18s 602MB
Nov 09 03:12:02 Starting compiler/backend/x64
Nov 09 03:12:21 Finished compiler/backend/x64                                    18s   1GB
Nov 09 03:12:21 Starting compiler/backend/arm7
Nov 09 03:12:41 Finished compiler/backend/arm7                                   20s   1GB
Nov 09 03:12:42 Starting compiler/backend/arm8
Nov 09 03:13:01 Finished compiler/backend/arm8                                   19s   1GB
Nov 09 03:13:02 Starting compiler/backend/mips
Nov 09 03:13:21 Finished compiler/backend/mips                                   19s   1GB
Nov 09 03:13:21 Starting compiler/backend/riscv
Nov 09 03:13:41 Finished compiler/backend/riscv                                  19s   1GB
Nov 09 03:13:42 Starting compiler/backend/ag32
Nov 09 03:14:53 Finished compiler/backend/ag32                                 1m11s   1GB
Nov 09 03:14:54 Starting compiler/parsing/proofs
Nov 09 03:20:45 Finished compiler/parsing/proofs                               5m51s   1GB
Nov 09 03:20:45 Starting compiler/inference/proofs
Nov 09 03:23:23 Finished compiler/inference/proofs                             2m37s   1GB
Nov 09 03:23:23 Starting compiler/backend/semantics
Nov 09 03:54:54 Finished compiler/backend/semantics                           31m30s   2GB
Nov 09 03:54:55 Starting compiler/backend/reg_alloc/proofs
Nov 09 03:58:44 Finished compiler/backend/reg_alloc/proofs                     3m49s 859MB
Nov 09 03:58:44 Starting compiler/backend/proofs
Nov 09 04:48:23 FAILED: compiler/backend/proofs
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Starting work on reachable_sptProofTheory
Starting work on README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md                                       real:    1s  user:    1s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   15s  user:   14s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   28s  user:   27s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   21s  user:   19s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   54s  user:   53s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   75s  user:   73s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   28s  user:   26s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   21s  user:   20s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   34s  user:   33s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   18s  user:   17s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   12s  user:   11s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   19s  user:   18s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  196s  user:  193s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   27s  user:   25s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  141s  user:  138s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   38s  user:   36s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  186s  user:  182s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   28s  user:   26s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   10s  user:   10s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   56s  user:   55s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  135s  user:  132s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   30s  user:   29s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  200s  user:  197s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  213s  user:  208s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   51s  user:   50s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  220s  user:  216s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   32s  user:   30s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:   72s  user:   71s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   49s  user:   48s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   60s  user:   58s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   61s  user:   59s     OK
Starting work on flat_elimProofTheory
stack_removeProofTheory                         real:  274s  user:  270s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  664s  user:  655s     OK
Starting work on word_to_wordProofTheory
data_to_word_memoryProofTheory                  real:  757s  user:  749s     OK
Starting work on stack_allocProofTheory
word_to_wordProofTheory                         real:   71s  user:   69s     OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                        real:  249s  user:  245s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   34s  user:   33s     OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory                        real:   75s  user:   74s     OK
Starting work on word_to_stackProofTheory
data_to_word_gcProofTheory                      real:  262s  user:  258s     OK
Starting work on data_to_word_bignumProofTheory
stack_allocProofTheory                          real:  460s  user:  453s     OK
data_to_word_bignumProofTheory                  real:  262s  user:  257s     OK
Starting work on data_to_word_assignProofTheory
data_to_word_assignProofTheory                  real: 1269s  user: 1258s     OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                         real:   48s  user:   46sFAIL<1>
            NONE => res1 = NONE
          | SOME (Rval v) => w. res1 = SOME (Result (Loc l1 l2) w)
          | SOME (Rerr (Rraise v')) => v w. res1 = SOME (Exception v w)
          | SOME (Rerr (Rabort Rtype_error)) => res1 = SOME TimeOut
          | SOME (Rerr (Rabort Rtimeout_error)) => res1 = SOME TimeOut
          | SOME (Rerr (Rabort (Rffi_error f))) => res1 = SOME (FinalFFI f))
 
 failed.
 Failed to prove theorem compile_correct.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 619", origin_function = "by", origin_structure = "BasicProvers"}
flat_elimProofTheory                                                    M-KILLED
word_to_stackProofTheory                                                M-KILLED