Overview

Job 794

CakeML:b2c1007e2e54c223bcc1b1cb29e00c496a52e275
  Find and fix more definition-saves that cause loss of "compute"
HOL:a083c115f48c74233904c5c3e8fa848239e6ab9c
  Deal with rebindings of ptree_{size,fringe}_def in grammarScript
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               2s  21MB
 Starting developers/bin
 Finished developers/bin                                        1m09s 918MB
 Starting semantics/ffi
 Finished semantics/ffi                                           10s 222MB
 Starting semantics
 Finished semantics                                             1m21s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m54s   1GB
 Starting basis/pure
 Finished basis/pure                                              48s 602MB
 Starting translator
 Finished translator                                            1m39s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        57s   2GB
 Starting characteristic
 Finished characteristic                                        5m12s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m27s   1GB
 Starting basis
 Finished basis                                                16m21s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m31s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              53s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m59s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  20MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  15MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   24s 723MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                  45s 733MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  12s 798MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  17s 761MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 14s 782MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  16s 852MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    18s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   18s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   19s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  19s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m07s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m34s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m40s 959MB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            6m51s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     2m38s 814MB
 Starting compiler/backend/proofs
 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-794/basis/pure]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/cakeml-794/basis/pure]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-794/basis/pure]0;Holmake: ~/oven/regression/cakeml-794/misc]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-794/misc]0;Holmake: ~/oven/regression/cakeml-794/developers]0;Holmake: ~/oven/regression/cakeml-794/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-794/misc]0;Holmake: ~/oven/regression/cakeml-794/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-794/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-794/misc]0;Holmake: ~/oven/regression/cakeml-794/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-794/basis/pure]0;Holmake: ~/oven/regression/cakeml-794/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-794/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-794/semantics]0;Holmake: ~/oven/regression/cakeml-794/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-794/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-794/semantics]0;Holmake: ~/oven/regression/cakeml-794/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-794/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-794/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ~/oven/regression/cakeml-794/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-794/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-a083c115f48c74233904c5c3e8fa848239e6ab9c/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ~/oven/regression/cakeml-794/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-794/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/oven/regression/cakeml-794/translator/monadic]0;Holmake: ~/oven/regression/cakeml-794/characteristic]0;Holmake: ~/oven/regression/cakeml-794/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-794/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-794/characteristic]0;Holmake: ~/oven/regression/cakeml-794/translator]0;Holmake: ~/oven/regression/cakeml-794/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-794/characteristic]0;Holmake: ~/oven/regression/cakeml-794/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-794/translator/monadic]0;Holmake: ~/oven/regression/cakeml-794/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/proofs
Starting work on bvi_tailrecProofTheory
Starting work on data_liveProofTheory
Starting work on data_simpProofTheory
Starting work on data_spaceProofTheory
data_simpProofTheory                                                         OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                                                        OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                                                          OK
Starting work on bvi_letProofTheory
data_liveProofTheory                                                         OK
Starting work on bvi_to_dataProofTheory
bvi_letProofTheory                                                           OK
Starting work on clos_annotateProofTheory
bvl_constProofTheory                                                         OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory                                                     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                                                        OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                                                        OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                                                          OK
Starting work on clos_knownPropsTheory
bvi_to_dataProofTheory                                                       OK
Starting work on clos_letopProofTheory
clos_knownPropsTheory                                                        OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                                                        OK
Starting work on clos_labelsProofTheory
clos_ticksProofTheory                                                        OK
Starting work on clos_knownProofTheory
bvi_tailrecProofTheory                                                       OK
Starting work on bvl_to_bviProofTheory
clos_labelsProofTheory                                                       OK
Starting work on clos_mtiProofTheory
clos_mtiProofTheory                                                          OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                                                       OK
Starting work on word_simpProofTheory
clos_knownProofTheory                                                        OK
Starting work on word_bignumProofTheory
word_simpProofTheory                                                         OK
Starting work on word_gcFunctionsTheory
clos_callProofTheory                                                         OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                                                       OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                                                        OK
Starting work on word_allocProofTheory
word_bignumProofTheory                                                       OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                                                       OK
Starting work on word_removeProofTheory
word_removeProofTheory                                                       OK
Starting work on flat_elimProofTheory
word_instProofTheory                                                         OK
Starting work on flat_exh_matchProofTheory
flat_exh_matchProofTheory                                                    OK
Starting work on flat_reorder_matchProofTheory
flat_elimProofTheory                                                         OK
Starting work on flat_to_patProofTheory
flat_reorder_matchProofTheory                                                OK
Starting work on flat_uncheck_ctorsProofTheory
flat_uncheck_ctorsProofTheory                                                OK
Starting work on lab_filterProofTheory
flat_to_patProofTheory                                                       OK
Starting work on stack_removeProofTheory
lab_filterProofTheory                                                        OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                                                       OK
Starting work on source_to_flatProofTheory
data_to_word_memoryProofTheory                                               OK
Starting work on stack_allocProofTheory
source_to_flatProofTheory                                                    OK
Starting work on stack_namesProofTheory
word_allocProofTheory                                                        OK
Starting work on word_to_wordProofTheory
stack_namesProofTheory                                                       OK
Starting work on word_to_stackProofTheory
word_to_wordProofTheory                                                      OK
Starting work on data_to_word_gcProofTheory
stack_removeProofTheory                                                      OK
Starting work on lab_to_targetProofTheory
data_to_word_gcProofTheory                                                   OK
Starting work on data_to_word_bignumProofTheory
lab_to_targetProofTheory                                                     OK
Starting work on word_elimProofTheory
stack_allocProofTheory                                                       OK
Starting work on README.md
README.md                                                                    OK
word_elimProofTheory                                                         OK
data_to_word_bignumProofTheory                                               OK
Starting work on data_to_word_assignProofTheory
word_to_stackProofTheory                                                     OK
Starting work on stack_to_labProofTheory
stack_to_labProofTheory                                                      OK
data_to_word_assignProofTheory                                               OK
Starting work on data_to_wordProofTheory
data_to_wordProofTheory                                             FAILED! <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 = "first subgoal not solved by second tactic (THEN1 on line 486) (THEN1 on line 483) (THEN1 on line 491) (THEN1 on line 470) (THEN1 on line 515) (THEN1 on line 522)", origin_function = "THEN1", origin_structure = "Tactical"}