Job 1371

CakeML:631fbdde10d14041072739c82fd457729fe3083f
  Add a bignum to sum example [Sep 15 11:44:00]
#802 (data-cost)
Merging into:018eec673b8b703adeecb85ccab09ec91be05cb3
  Merge pull request #791 from CakeML/lpr_opt [Sep 29 19:56:37]
HOL:b320cfef77ec162c09020353b84e75afad108480
  Simplify handling of diminish_srw_ss by forcing it to initialise [Oct 15 10:45:33]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Oct 16 07:20:53 Claimed job
Oct 16 07:21:02 Building HOL
Oct 16 07:34:49 Starting developers
Oct 16 07:34:49 Finished developers                                               0s  35MB
Oct 16 07:34:49 Starting developers/bin
Oct 16 07:34:55 Finished developers/bin                                           5s   1GB
Oct 16 07:34:56 Starting semantics/ffi
Oct 16 07:35:06 Finished semantics/ffi                                           10s 308MB
Oct 16 07:35:06 Starting semantics
Oct 16 07:36:50 Finished semantics                                             1m43s   1GB
Oct 16 07:36:50 Starting semantics/proofs
Oct 16 07:40:17 Finished semantics/proofs                                      3m26s   1GB
Oct 16 07:40:17 Starting semantics/alt_semantics
Oct 16 07:40:26 Finished semantics/alt_semantics                                  8s 428MB
Oct 16 07:40:26 Starting semantics/alt_semantics/proofs
Oct 16 07:42:38 Finished semantics/alt_semantics/proofs                        2m11s   1GB
Oct 16 07:42:38 Starting basis/pure
Oct 16 07:45:33 Finished basis/pure                                            2m54s   1GB
Oct 16 07:45:33 Starting translator
Oct 16 07:48:29 Finished translator                                            2m56s   2GB
Oct 16 07:48:30 Starting compiler/parsing
Oct 16 07:49:48 Finished compiler/parsing                                      1m18s   5GB
Oct 16 07:49:48 Starting characteristic
Oct 16 07:56:38 Finished characteristic                                        6m49s   2GB
Oct 16 07:56:38 Starting translator/monadic
Oct 16 07:58:32 Finished translator/monadic                                    1m53s   2GB
Oct 16 07:58:32 Starting basis
Oct 16 08:33:01 Finished basis                                                34m29s  28GB
Oct 16 08:33:02 Starting compiler/inference
Oct 16 08:34:13 Finished compiler/inference                                    1m10s   2GB
Oct 16 08:34:13 Starting compiler/backend/reg_alloc
Oct 16 08:35:24 Finished compiler/backend/reg_alloc                            1m11s   2GB
Oct 16 08:35:25 Starting compiler/backend/gc
Oct 16 08:38:59 Finished compiler/backend/gc                                   3m33s   3GB
Oct 16 08:38:59 Starting compiler/backend
Oct 16 08:44:03 Finished compiler/backend                                      5m03s   4GB
Oct 16 08:44:03 Starting compiler/encoders/asm
Oct 16 08:44:27 Finished compiler/encoders/asm                                   23s   1GB
Oct 16 08:44:27 Starting compiler/encoders/x64
Oct 16 08:45:32 Finished compiler/encoders/x64                                 1m04s   1GB
Oct 16 08:45:33 Starting compiler/encoders/arm7
Oct 16 08:47:31 Finished compiler/encoders/arm7                                1m57s   1GB
Oct 16 08:47:31 Starting compiler/encoders/arm8
Oct 16 08:48:12 Finished compiler/encoders/arm8                                  40s   1GB
Oct 16 08:48:12 Starting compiler/encoders/mips
Oct 16 08:49:30 Finished compiler/encoders/mips                                1m17s   1GB
Oct 16 08:49:30 Starting compiler/encoders/riscv
Oct 16 08:51:17 Finished compiler/encoders/riscv                               1m47s   1GB
Oct 16 08:51:18 Starting compiler/encoders/ag32
Oct 16 08:51:40 Finished compiler/encoders/ag32                                  22s 964MB
Oct 16 08:51:40 Starting compiler/backend/x64
Oct 16 08:52:00 Finished compiler/backend/x64                                    20s   1GB
Oct 16 08:52:01 Starting compiler/backend/arm7
Oct 16 08:52:22 Finished compiler/backend/arm7                                   21s   1GB
Oct 16 08:52:22 Starting compiler/backend/arm8
Oct 16 08:52:42 Finished compiler/backend/arm8                                   19s   1GB
Oct 16 08:52:42 Starting compiler/backend/mips
Oct 16 08:53:03 Finished compiler/backend/mips                                   20s   1GB
Oct 16 08:53:03 Starting compiler/backend/riscv
Oct 16 08:53:24 Finished compiler/backend/riscv                                  20s   1GB
Oct 16 08:53:24 Starting compiler/backend/ag32
Oct 16 08:54:36 Finished compiler/backend/ag32                                 1m11s   2GB
Oct 16 08:54:36 Starting compiler/parsing/proofs
Oct 16 08:56:48 Finished compiler/parsing/proofs                               2m11s   1GB
Oct 16 08:56:48 Starting compiler/inference/proofs
Oct 16 08:59:04 Finished compiler/inference/proofs                             2m16s   1GB
Oct 16 08:59:05 Starting compiler/backend/semantics
Oct 16 09:25:50 Finished compiler/backend/semantics                           26m45s   4GB
Oct 16 09:25:50 Starting compiler/backend/reg_alloc/proofs
Oct 16 09:29:12 Finished compiler/backend/reg_alloc/proofs                     3m21s   1GB
Oct 16 09:29:12 Starting compiler/backend/proofs
Oct 16 10:06:30 FAILED: compiler/backend/proofs
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Starting work on reachable_sptProofTheory
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   14s  user:   13s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   17s  user:   15s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   72s  user:   46s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   51s  user:   32s     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                            real:  163s  user:  111s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   65s  user:   44s     OK
Starting work on clos_callProofTheory
bvl_constProofTheory                            real:  298s  user:  193s     OK
Starting work on bvl_handleProofTheory
bvl_handleProofTheory                           real:   56s  user:   35s     OK
Starting work on bvl_inlineProofTheory
bvi_tailrecProofTheory                          real:  456s  user:  306s     OK
Starting work on clos_fvsProofTheory
bvl_inlineProofTheory                           real:   89s  user:   55s     OK
Starting work on bvl_to_bviProofTheory
bvi_to_dataProofTheory                          real:  328s  user:  213s     OK
Starting work on clos_knownPropsTheory
clos_fvsProofTheory                             real:   44s  user:   30s     OK
Starting work on clos_letopProofTheory
clos_knownPropsTheory                           real:   29s  user:   21s     OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                           real:   43s  user:   34s     OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory                           real:   59s  user:   47s     OK
Starting work on clos_knownProofTheory
clos_mtiProofTheory                             real:   80s  user:   62s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  431s  user:  305s     OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                             real:   27s  user:   20s     OK
Starting work on word_simpProofTheory
clos_numberProofTheory                          real:   52s  user:   45s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:  133s  user:  101s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  283s  user:  227s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   69s  user:   56s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  427s  user:  341s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  434s  user:  388s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:  120s  user:   91s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  393s  user:  354s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   55s  user:   52s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:  108s  user:  105s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   81s  user:   78s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   88s  user:   86s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   95s  user:   92s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   96s  user:   94s     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                       real:  140s  user:  135s     OK
Starting work on stack_allocProofTheory
word_allocProofTheory                           real:  859s  user:  823s     OK
Starting work on word_to_wordProofTheory
stack_removeProofTheory                         real:  311s  user:  307s     OK
Starting work on lab_to_targetProofTheory
word_to_wordProofTheory                         real:   82s  user:   80s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   43s  user:   41s     OK
Starting work on stack_rawcallProofTheory
stack_rawcallProofTheory                        real:   83s  user:   81s     OK
Starting work on word_to_stackProofTheory
data_to_word_memoryProofTheory                  real: 1103s  user: 1060s     OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                        real:  283s  user:  280s     OK
Starting work on word_elimProofTheory
word_elimProofTheory                            real:  140s  user:  138s     OK
stack_allocProofTheory                          real:  526s  user:  518s     OK
data_to_word_gcProofTheory                      real:  265s  user:  260sFAIL<1>
                   ss)|>) t2 [] locs
 
 failed.
 Failed to prove theorem gc_lemma.
 
 Exception raised at Tactical.FIRST_ASSUM:
 
 error in quse /home/myreen/regression/cakeml-1371/compiler/backend/proofs/data_to_word_gcProofScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1371/compiler/backend/proofs/data_to_word_gcProofScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
word_to_stackProofTheory                                                M-KILLED