Job 1372

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 16 08:24:42 Claimed job
Oct 16 08:24:50 Building HOL
Oct 16 08:40:14 Starting developers
Oct 16 08:40:18 Finished developers                                               4s  69MB
Oct 16 08:40:18 Starting developers/bin
Oct 16 08:40:25 Finished developers/bin                                           6s   1GB
Oct 16 08:40:25 Starting semantics/ffi
Oct 16 08:40:37 Finished semantics/ffi                                           11s 224MB
Oct 16 08:40:37 Starting semantics
Oct 16 08:42:13 Finished semantics                                             1m35s   1GB
Oct 16 08:42:13 Starting semantics/proofs
Oct 16 08:45:48 Finished semantics/proofs                                      3m35s 931MB
Oct 16 08:45:49 Starting semantics/alt_semantics
Oct 16 08:45:58 Finished semantics/alt_semantics                                  9s 267MB
Oct 16 08:45:58 Starting semantics/alt_semantics/proofs
Oct 16 08:48:15 Finished semantics/alt_semantics/proofs                        2m17s 756MB
Oct 16 08:48:15 Starting basis/pure
Oct 16 08:51:19 Finished basis/pure                                            3m03s 909MB
Oct 16 08:51:19 Starting translator
Oct 16 08:54:06 Finished translator                                            2m46s   1GB
Oct 16 08:54:06 Starting compiler/parsing
Oct 16 08:55:20 Finished compiler/parsing                                      1m13s   2GB
Oct 16 08:55:20 Starting characteristic
Oct 16 09:01:32 Finished characteristic                                        6m11s   2GB
Oct 16 09:01:32 Starting translator/monadic
Oct 16 09:03:15 Finished translator/monadic                                    1m42s   1GB
Oct 16 09:03:15 Starting basis
Oct 16 09:39:29 Finished basis                                                36m13s  13GB
Oct 16 09:39:29 Starting compiler/inference
Oct 16 09:40:42 Finished compiler/inference                                    1m12s   1GB
Oct 16 09:40:42 Starting compiler/backend/reg_alloc
Oct 16 09:41:48 Finished compiler/backend/reg_alloc                            1m06s   1GB
Oct 16 09:41:48 Starting compiler/backend/gc
Oct 16 09:45:31 Finished compiler/backend/gc                                   3m42s   2GB
Oct 16 09:45:31 Starting compiler/backend
Oct 16 09:50:16 Finished compiler/backend                                      4m44s   3GB
Oct 16 09:50:16 Starting compiler/encoders/asm
Oct 16 09:50:40 Finished compiler/encoders/asm                                   22s 654MB
Oct 16 09:50:40 Starting compiler/encoders/x64
Oct 16 09:51:44 Finished compiler/encoders/x64                                 1m03s 752MB
Oct 16 09:51:44 Starting compiler/encoders/arm7
Oct 16 09:53:46 Finished compiler/encoders/arm7                                2m01s   1GB
Oct 16 09:53:46 Starting compiler/encoders/arm8
Oct 16 09:54:23 Finished compiler/encoders/arm8                                  37s 942MB
Oct 16 09:54:24 Starting compiler/encoders/mips
Oct 16 09:55:48 Finished compiler/encoders/mips                                1m24s   1GB
Oct 16 09:55:48 Starting compiler/encoders/riscv
Oct 16 09:57:27 Finished compiler/encoders/riscv                               1m38s 967MB
Oct 16 09:57:27 Starting compiler/encoders/ag32
Oct 16 09:57:45 Finished compiler/encoders/ag32                                  18s 616MB
Oct 16 09:57:46 Starting compiler/backend/x64
Oct 16 09:58:04 Finished compiler/backend/x64                                    18s   1GB
Oct 16 09:58:04 Starting compiler/backend/arm7
Oct 16 09:58:24 Finished compiler/backend/arm7                                   20s   1GB
Oct 16 09:58:25 Starting compiler/backend/arm8
Oct 16 09:58:44 Finished compiler/backend/arm8                                   19s   1GB
Oct 16 09:58:44 Starting compiler/backend/mips
Oct 16 09:59:04 Finished compiler/backend/mips                                   19s   1GB
Oct 16 09:59:04 Starting compiler/backend/riscv
Oct 16 09:59:24 Finished compiler/backend/riscv                                  19s   1GB
Oct 16 09:59:24 Starting compiler/backend/ag32
Oct 16 10:00:36 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 16 10:00:36 Starting compiler/parsing/proofs
Oct 16 10:06:26 Finished compiler/parsing/proofs                               5m50s   1GB
Oct 16 10:06:26 Starting compiler/inference/proofs
Oct 16 10:09:04 Finished compiler/inference/proofs                             2m37s   1GB
Oct 16 10:09:04 Starting compiler/backend/semantics
Oct 16 10:39:59 Finished compiler/backend/semantics                           30m54s   2GB
Oct 16 10:39:59 Starting compiler/backend/reg_alloc/proofs
Oct 16 10:43:48 Finished compiler/backend/reg_alloc/proofs                     3m48s 836MB
Oct 16 10:43:48 Starting compiler/backend/proofs
Oct 16 11:06:49 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 README.md
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
README.md                                       real:    1s  user:    0s     OK
Starting work on data_simpProofTheory
reachable_sptProofTheory                        real:   12s  user:   11s     OK
Starting work on data_spaceProofTheory
data_simpProofTheory                            real:   14s  user:   13s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   28s  user:   27s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   20s  user:   19s     OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                            real:   55s  user:   54s     OK
Starting work on bvl_handleProofTheory
data_liveProofTheory                            real:   76s  user:   74s     OK
Starting work on bvi_to_dataProofTheory
clos_annotateProofTheory                        real:   27s  user:   26s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   20s  user:   19s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   34s  user:   32s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   17s  user:   16s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   11s  user:   10s     OK
Starting work on clos_letopProofTheory
clos_letopProofTheory                           real:   20s  user:   19s     OK
Starting work on clos_ticksProofTheory
bvi_tailrecProofTheory                          real:  194s  user:  191s     OK
Starting work on bvl_to_bviProofTheory
clos_ticksProofTheory                           real:   26s  user:   25s     OK
Starting work on clos_knownProofTheory
bvi_to_dataProofTheory                          real:  141s  user:  138s     OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                             real:   37s  user:   36s     OK
Starting work on clos_numberProofTheory
clos_callProofTheory                            real:  189s  user:  185s     OK
Starting work on bvl_jumpProofTheory
clos_numberProofTheory                          real:   27s  user:   26s     OK
Starting work on word_simpProofTheory
bvl_jumpProofTheory                             real:   11s  user:   10s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   55s  user:   54s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  136s  user:  133s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   29s  user:   28s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  206s  user:  201s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  217s  user:  213s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   52s  user:   50s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  223s  user:  218s     OK
Starting work on word_depthProofTheory
word_removeProofTheory                          real:   31s  user:   29s     OK
Starting work on flat_patternProofTheory
word_depthProofTheory                           real:   72s  user:   70s     OK
Starting work on flat_to_closProofTheory
flat_patternProofTheory                         real:   50s  user:   48s     OK
Starting work on lab_filterProofTheory
flat_to_closProofTheory                         real:   61s  user:   59s     OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                           real:   61s  user:   59s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   68s  user:   67s     OK
Starting work on source_to_flatProofTheory
source_to_flatProofTheory                       real:  109s  user:  106s     OK
Starting work on stack_allocProofTheory
stack_removeProofTheory                         real:  272s  user:  269s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  637s  user:  630s     OK
Starting work on word_to_wordProofTheory
word_to_wordProofTheory                         real:   68s  user:   66s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   32s  user:   31s     OK
Starting work on stack_rawcallProofTheory
data_to_word_memoryProofTheory                  real:  770s  user:  761s     OK
Starting work on data_to_word_gcProofTheory
stack_rawcallProofTheory                        real:   74s  user:   72s     OK
Starting work on word_to_stackProofTheory
lab_to_targetProofTheory                        real:  248s  user:  244s     OK
Starting work on word_elimProofTheory
stack_allocProofTheory                          real:  450s  user:  443s     OK
word_elimProofTheory                            real:  133s  user:  131s     OK
data_to_word_gcProofTheory                      real:  237s  user:  233sFAIL<1>
            stack_max :=
              OPTION_MAP2 MAX
                (OPTION_MAP2 MAX s.stack_max
                   (size_of_stack (Env s.locals_size x::s.stack)))
                (OPTION_MAP2 $+ (size_of_stack (Env s.locals_size x::s.stack))
                   ss)|>) t2 [] locs
 
 failed.
 Failed to prove theorem gc_lemma.
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
word_to_stackProofTheory                                                M-KILLED