Job 857

CakeML:4db10e33ea7c63a89d97389e723abf84bad5275a
  Update given various spt theorems have moved to HOL [May 09 14:46:50]
#643 (cleanup)
Merging into:53fd12a2f3ee14927097506986b55a5d2bcf1b97
  Merge pull request #641 from CakeML/issue465 [May 10 05:54:52]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 10 15:58:29 Claimed job
May 10 15:58:32 Reusing HOL
May 10 15:58:36 Starting developers
May 10 15:58:37 Finished developers                                               0s  30MB
May 10 15:58:37 Starting developers/bin
May 10 15:58:41 Finished developers/bin                                           2s 144MB
May 10 15:58:41 Starting semantics/ffi
May 10 15:58:49 Finished semantics/ffi                                            7s 212MB
May 10 15:58:49 Starting semantics
May 10 16:00:05 Finished semantics                                             1m15s   1GB
May 10 16:00:05 Starting semantics/proofs
May 10 16:03:03 Finished semantics/proofs                                      2m57s   1GB
May 10 16:03:04 Starting basis/pure
May 10 16:03:47 Finished basis/pure                                              43s 758MB
May 10 16:03:48 Starting translator
May 10 16:05:25 Finished translator                                            1m36s   1GB
May 10 16:05:25 Starting compiler/parsing
May 10 16:06:22 Finished compiler/parsing                                        56s   2GB
May 10 16:06:23 Starting characteristic
May 10 16:11:33 Finished characteristic                                        5m09s   1GB
May 10 16:11:33 Starting translator/monadic
May 10 16:12:56 Finished translator/monadic                                    1m22s   1GB
May 10 16:12:56 Starting basis
May 10 16:29:51 Finished basis                                                16m54s   2GB
May 10 16:29:51 Starting compiler/inference
May 10 16:31:21 Finished compiler/inference                                    1m29s   1GB
May 10 16:31:22 Starting compiler/backend/reg_alloc
May 10 16:32:19 Finished compiler/backend/reg_alloc                              57s   1GB
May 10 16:32:20 Starting compiler/backend/gc
May 10 16:40:12 Finished compiler/backend/gc                                   7m51s   2GB
May 10 16:40:12 Starting compiler/backend
May 10 16:40:13 Finished compiler/backend                                         0s  42MB
May 10 16:40:14 Starting compiler/encoders/asm
May 10 16:40:14 Finished compiler/encoders/asm                                    0s  32MB
May 10 16:40:14 Starting compiler/encoders/x64
May 10 16:40:37 Finished compiler/encoders/x64                                   22s 701MB
May 10 16:40:38 Starting compiler/encoders/arm6
May 10 16:41:21 Finished compiler/encoders/arm6                                  43s 907MB
May 10 16:41:21 Starting compiler/encoders/arm8
May 10 16:41:33 Finished compiler/encoders/arm8                                  11s 520MB
May 10 16:41:33 Starting compiler/encoders/mips
May 10 16:41:49 Finished compiler/encoders/mips                                  15s   1GB
May 10 16:41:49 Starting compiler/encoders/riscv
May 10 16:42:02 Finished compiler/encoders/riscv                                 12s 790MB
May 10 16:42:02 Starting compiler/encoders/ag32
May 10 16:42:17 Finished compiler/encoders/ag32                                  14s 802MB
May 10 16:42:17 Starting compiler/backend/x64
May 10 16:42:33 Finished compiler/backend/x64                                    15s   1GB
May 10 16:42:34 Starting compiler/backend/arm6
May 10 16:42:50 Finished compiler/backend/arm6                                   16s   1GB
May 10 16:42:50 Starting compiler/backend/arm8
May 10 16:43:06 Finished compiler/backend/arm8                                   15s   1GB
May 10 16:43:06 Starting compiler/backend/mips
May 10 16:43:23 Finished compiler/backend/mips                                   16s   1GB
May 10 16:43:24 Starting compiler/backend/riscv
May 10 16:43:40 Finished compiler/backend/riscv                                  16s   1GB
May 10 16:43:41 Starting compiler/backend/ag32
May 10 16:44:47 Finished compiler/backend/ag32                                 1m05s 950MB
May 10 16:44:47 Starting compiler/parsing/proofs
May 10 16:50:13 Finished compiler/parsing/proofs                               5m25s   1GB
May 10 16:50:13 Starting compiler/inference/proofs
May 10 16:52:50 Finished compiler/inference/proofs                             2m36s   1GB
May 10 16:52:50 Starting compiler/backend/semantics
May 10 16:59:45 Finished compiler/backend/semantics                            6m54s   2GB
May 10 16:59:45 Starting compiler/backend/reg_alloc/proofs
May 10 17:03:01 Finished compiler/backend/reg_alloc/proofs                     3m15s 811MB
May 10 17:03:01 Starting compiler/backend/proofs
May 10 17:07:57 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/regression/cakeml-857/basis/pure]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/balanced_bst]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-857/basis/pure]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-857/basis/pure]0;Holmake: ~/regression/cakeml-857/misc]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-857/misc]0;Holmake: ~/regression/cakeml-857/developers]0;Holmake: ~/regression/cakeml-857/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-857/misc]0;Holmake: ~/regression/cakeml-857/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-857/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-857/misc]0;Holmake: ~/regression/cakeml-857/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-857/basis/pure]0;Holmake: ~/regression/cakeml-857/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-857/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-857/semantics]0;Holmake: ~/regression/cakeml-857/semantics/ffi]0;Holmake: ~/regression/cakeml-857/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-857/semantics]0;Holmake: ~/regression/cakeml-857/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-857/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-857/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/regression/cakeml-857/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-857/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../reg_alloc]0;Holmake: ../reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ..]0;Holmake: ../../encoders/asm]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ~/regression/cakeml-857/semantics/proofs]0;Holmake: ~/regression/cakeml-857/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: .]0;Holmake: ../gc]0;Holmake: ../gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: .]0;Holmake: ../reg_alloc/proofs]0;Holmake: ~/regression/cakeml-857/translator/monadic]0;Holmake: ~/regression/cakeml-857/characteristic]0;Holmake: ~/regression/cakeml-857/compiler/parsing]0;Holmake: ~/regression/cakeml-857/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-857/characteristic]0;Holmake: ~/regression/cakeml-857/translator]0;Holmake: ~/regression/cakeml-857/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-857/characteristic]0;Holmake: ~/regression/cakeml-857/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-857/translator/monadic]0;Holmake: ~/regression/cakeml-857/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../reg_alloc/proofs]0;Holmake: ../reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
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
clos_knownPropsTheory                                                                                                             OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                                                                                                            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
bvl_to_bviProofTheory                                                                                                    FAILED! <1>
         evaluate (ys,MAP (adjust_bv b2) env,inc_clock c t1) =
         (map_result (MAP (adjust_bv b2)) (adjust_bv b2) res,t2) 
         state_rel b2 s2 t2 
         MAP (adjust_bv b1) env = MAP (adjust_bv b2) env 
         a. a  FDOM s1.refs  b1 a = b2 a
 
 failed.
 error in quse /home/myreen/regression/cakeml-857/compiler/backend/proofs/bvl_to_bviProofScript.sml : HOL_ERR {message = "Not of pair type (THEN1 on line 2252) (THEN1 on line 2249) (THEN1 on line 2135) (THEN1 on line 2266) (THEN1 on line 2274) (THEN1 on line 2287) (THEN1 on line 2317) (THEN1 on line 2421) (THEN1 on line 2516) (THEN1 on line 2618) (THEN1 on line 2646) (THEN1 on line 2675) (THEN1 on line 2734) (THEN1 on line 2809) (THEN1 on line 2928) (THEN1 on line 3023) (THEN1 on line 3066) (THEN1 on line 3118) (THEN1 on line 2087) (THEN1 on line 3128) (THEN1 on line 3151)", origin_function = "PairCases_on", origin_structure = "pairTools"}
 error in load bvl_to_bviProofScript : HOL_ERR {message = "Not of pair type (THEN1 on line 2252) (THEN1 on line 2249) (THEN1 on line 2135) (THEN1 on line 2266) (THEN1 on line 2274) (THEN1 on line 2287) (THEN1 on line 2317) (THEN1 on line 2421) (THEN1 on line 2516) (THEN1 on line 2618) (THEN1 on line 2646) (THEN1 on line 2675) (THEN1 on line 2734) (THEN1 on line 2809) (THEN1 on line 2928) (THEN1 on line 3023) (THEN1 on line 3066) (THEN1 on line 3118) (THEN1 on line 2087) (THEN1 on line 3128) (THEN1 on line 3151)", origin_function = "PairCases_on", origin_structure = "pairTools"}
 Uncaught exception: HOL_ERR {message = "Not of pair type (THEN1 on line 2252) (THEN1 on line 2249) (THEN1 on line 2135) (THEN1 on line 2266) (THEN1 on line 2274) (THEN1 on line 2287) (THEN1 on line 2317) (THEN1 on line 2421) (THEN1 on line 2516) (THEN1 on line 2618) (THEN1 on line 2646) (THEN1 on line 2675) (THEN1 on line 2734) (THEN1 on line 2809) (THEN1 on line 2928) (THEN1 on line 3023) (THEN1 on line 3066) (THEN1 on line 3118) (THEN1 on line 2087) (THEN1 on line 3128) (THEN1 on line 3151)", origin_function = "PairCases_on", origin_structure = "pairTools"}
word_bignumProofTheory                                                                                                      M-KILLED
word_gcFunctionsTheory                                                                                                      M-KILLED
clos_to_bvlProofTheory                                                                                                      M-KILLED