Job 1047

CakeML:efb917e659c4e574a87fb90d9ed8f3283561a5b9
  Merge pull request #691 from CakeML/regexp_delta [Oct 03 21:52:59]
HOL:c80b32898bc7a3f692c1be84161e569112efdfa9
  Fix ARM_security_properties example for change in 44aabdd82 [Oct 02 12:15:29]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Oct 03 21:59:38 Claimed job
Oct 03 21:59:41 Reusing HOL
Oct 03 22:00:34 Starting developers
Oct 03 22:00:38 Finished developers                                               3s 123MB
Oct 03 22:00:38 Starting developers/bin
Oct 03 22:00:44 Finished developers/bin                                           5s 964MB
Oct 03 22:00:44 Starting semantics/ffi
Oct 03 22:00:53 Finished semantics/ffi                                            9s 286MB
Oct 03 22:00:53 Starting semantics
Oct 03 22:02:09 Finished semantics                                             1m16s   1GB
Oct 03 22:02:09 Starting semantics/proofs
Oct 03 22:05:02 Finished semantics/proofs                                      2m53s 995MB
Oct 03 22:05:03 Starting semantics/alt_semantics
Oct 03 22:05:10 Finished semantics/alt_semantics                                  7s 281MB
Oct 03 22:05:10 Starting semantics/alt_semantics/proofs
Oct 03 22:06:54 Finished semantics/alt_semantics/proofs                        1m43s 926MB
Oct 03 22:06:54 Starting basis/pure
Oct 03 22:07:39 Finished basis/pure                                              45s 780MB
Oct 03 22:07:40 Starting translator
Oct 03 22:09:19 Finished translator                                            1m39s   1GB
Oct 03 22:09:19 Starting compiler/parsing
Oct 03 22:10:14 Finished compiler/parsing                                        54s   1GB
Oct 03 22:10:14 Starting characteristic
Oct 03 22:15:22 Finished characteristic                                        5m08s   1GB
Oct 03 22:15:22 Starting translator/monadic
Oct 03 22:16:52 Finished translator/monadic                                    1m29s   1GB
Oct 03 22:16:52 Starting basis
Oct 03 22:35:34 Finished basis                                                18m42s   3GB
Oct 03 22:35:35 Starting compiler/inference
Oct 03 22:37:07 Finished compiler/inference                                    1m32s   1GB
Oct 03 22:37:07 Starting compiler/backend/reg_alloc
Oct 03 22:38:04 Finished compiler/backend/reg_alloc                              56s   1GB
Oct 03 22:38:04 Starting compiler/backend/gc
Oct 03 22:45:46 Finished compiler/backend/gc                                   7m41s   2GB
Oct 03 22:45:46 Starting compiler/backend
Oct 03 22:45:48 Finished compiler/backend                                         2s  33MB
Oct 03 22:45:49 Starting compiler/encoders/asm
Oct 03 22:45:50 Finished compiler/encoders/asm                                    1s  18MB
Oct 03 22:45:50 Starting compiler/encoders/x64
Oct 03 22:46:13 Finished compiler/encoders/x64                                   23s 765MB
Oct 03 22:46:13 Starting compiler/encoders/arm7
Oct 03 22:46:57 Finished compiler/encoders/arm7                                  44s 847MB
Oct 03 22:46:57 Starting compiler/encoders/arm8
Oct 03 22:47:10 Finished compiler/encoders/arm8                                  12s 574MB
Oct 03 22:47:10 Starting compiler/encoders/mips
Oct 03 22:47:27 Finished compiler/encoders/mips                                  16s 975MB
Oct 03 22:47:27 Starting compiler/encoders/riscv
Oct 03 22:47:41 Finished compiler/encoders/riscv                                 13s 885MB
Oct 03 22:47:41 Starting compiler/encoders/ag32
Oct 03 22:47:57 Finished compiler/encoders/ag32                                  16s 816MB
Oct 03 22:47:57 Starting compiler/backend/x64
Oct 03 22:48:14 Finished compiler/backend/x64                                    17s 880MB
Oct 03 22:48:14 Starting compiler/backend/arm7
Oct 03 22:48:33 Finished compiler/backend/arm7                                   18s   1GB
Oct 03 22:48:33 Starting compiler/backend/arm8
Oct 03 22:48:50 Finished compiler/backend/arm8                                   16s   1GB
Oct 03 22:48:50 Starting compiler/backend/mips
Oct 03 22:49:08 Finished compiler/backend/mips                                   18s   1GB
Oct 03 22:49:08 Starting compiler/backend/riscv
Oct 03 22:49:27 Finished compiler/backend/riscv                                  18s   1GB
Oct 03 22:49:27 Starting compiler/backend/ag32
Oct 03 22:50:30 Finished compiler/backend/ag32                                 1m03s   1GB
Oct 03 22:50:30 Starting compiler/parsing/proofs
Oct 03 22:55:47 Finished compiler/parsing/proofs                               5m16s   1GB
Oct 03 22:55:47 Starting compiler/inference/proofs
Oct 03 22:58:26 Finished compiler/inference/proofs                             2m38s 884MB
Oct 03 22:58:26 Starting compiler/backend/semantics
Oct 03 23:03:55 Finished compiler/backend/semantics                            5m28s   1GB
Oct 03 23:03:55 Starting compiler/backend/reg_alloc/proofs
Oct 03 23:07:02 Finished compiler/backend/reg_alloc/proofs                     3m07s 923MB
Oct 03 23:07:02 Starting compiler/backend/proofs
Oct 03 23:24:22 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/machine-code/multiword]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ~/cakeml/regression/cakeml-1047/basis/pure]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/balanced_bst]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/basis/pure]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/basis/pure]0;Holmake: ~/cakeml/regression/cakeml-1047/misc]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/misc]0;Holmake: ~/cakeml/regression/cakeml-1047/developers]0;Holmake: ~/cakeml/regression/cakeml-1047/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/misc]0;Holmake: ~/cakeml/regression/cakeml-1047/misc/lem_lib_stub]0;Holmake: ~/cakeml/regression/cakeml-1047/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/misc]0;Holmake: ~/cakeml/regression/cakeml-1047/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/basis/pure]0;Holmake: ~/cakeml/regression/cakeml-1047/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/cakeml/regression/cakeml-1047/translator/monadic/monad_base]0;Holmake: ~/cakeml/regression/cakeml-1047/semantics]0;Holmake: ~/cakeml/regression/cakeml-1047/semantics/ffi]0;Holmake: ~/cakeml/regression/cakeml-1047/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/semantics]0;Holmake: ~/cakeml/regression/cakeml-1047/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/translator/monadic/monad_base]0;Holmake: ~/cakeml/regression/cakeml-1047/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/cakeml/regression/cakeml-1047/unverified/reg_alloc]0;Holmake: ~/cakeml/regression/cakeml-1047/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: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/l3-machine-code/common]0;Holmake: ~/cakeml/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/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: ~/cakeml/regression/cakeml-1047/semantics/proofs]0;Holmake: ~/cakeml/regression/cakeml-1047/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: ~/cakeml/regression/cakeml-1047/translator/monadic]0;Holmake: ~/cakeml/regression/cakeml-1047/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1047/compiler/parsing]0;Holmake: ~/cakeml/regression/cakeml-1047/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1047/translator]0;Holmake: ~/cakeml/regression/cakeml-1047/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1047/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/cakeml/regression/cakeml-1047/translator/monadic]0;Holmake: ~/cakeml/regression/cakeml-1047/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                            real:   12s  user:   11s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   18s  user:   17s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   17s  user:   16s     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                            real:   41s  user:   40s     OK
Starting work on bvi_to_dataProofTheory
bvl_constProofTheory                            real:   43s  user:   42s     OK
Starting work on bvl_handleProofTheory
clos_annotateProofTheory                        real:   24s  user:   23s     OK
Starting work on clos_callProofTheory
bvl_handleProofTheory                           real:   17s  user:   16s     OK
Starting work on bvl_inlineProofTheory
bvl_inlineProofTheory                           real:   29s  user:   27s     OK
Starting work on clos_fvsProofTheory
clos_fvsProofTheory                             real:   15s  user:   14s     OK
Starting work on clos_knownPropsTheory
clos_knownPropsTheory                           real:   10s  user:    9s     OK
Starting work on clos_letopProofTheory
bvi_to_dataProofTheory                          real:   86s  user:   85s     OK
Starting work on clos_ticksProofTheory
clos_letopProofTheory                           real:   16s  user:   15s     OK
Starting work on clos_mtiProofTheory
clos_ticksProofTheory                           real:   22s  user:   21s     OK
Starting work on clos_knownProofTheory
bvi_tailrecProofTheory                          real:  154s  user:  152s     OK
Starting work on bvl_to_bviProofTheory
clos_mtiProofTheory                             real:   32s  user:   30s     OK
Starting work on clos_numberProofTheory
clos_numberProofTheory                          real:   23s  user:   22s     OK
Starting work on bvl_jumpProofTheory
bvl_jumpProofTheory                             real:    9s  user:    8s     OK
Starting work on word_simpProofTheory
clos_callProofTheory                            real:  161s  user:  157s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   46s  user:   44s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  113s  user:  111s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   25s  user:   23s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  168s  user:  165s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  185s  user:  181s     OK
Starting work on word_instProofTheory
clos_to_bvlProofTheory                          real:  183s  user:  179s     OK
Starting work on word_removeProofTheory
word_instProofTheory                            real:   42s  user:   40s     OK
Starting work on flat_to_patProofTheory
word_removeProofTheory                          real:   22s  user:   21s     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                           real:   52s  user:   51s     OK
Starting work on stack_removeProofTheory
flat_to_patProofTheory                          real:   93s  user:   91s     OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                          real:   32s  user:   31s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   37s  user:   36s     OK
Starting work on flat_exh_matchProofTheory
flat_exh_matchProofTheory                       real:   32s  user:   31s     OK
Starting work on flat_reorder_matchProofTheory
flat_reorder_matchProofTheory                   real:   29s  user:   28s     OK
Starting work on flat_uncheck_ctorsProofTheory
flat_uncheck_ctorsProofTheory                   real:   23s  user:   22s     OK
Starting work on source_to_flatProofTheory
stack_removeProofTheory                         real:  225s  user:  222s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  430s  user:  425s     OK
Starting work on word_to_wordProofTheory
source_to_flatProofTheory                       real:   70s  user:   69s     OK
Starting work on stack_allocProofTheory
word_to_wordProofTheory                         real:   52s  user:   51s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   27s  user:   25s     OK
Starting work on word_to_stackProofTheory
data_to_word_memoryProofTheory                  real:  568s  user:  563s     OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                        real:  206s  user:  203s     OK
Starting work on word_elimProofTheory
data_to_word_gcProofTheory                      real:  175s  user:  172s     OK
Starting work on data_to_word_bignumProofTheory
word_elimProofTheory                            real:   71s  user:   69s     OK
Starting work on README.md
README.md                                       real:    1s  user:    0s     OK
data_to_word_bignumProofTheory                  real:   12s  user:   11sFAIL<1>
 error in quse /home/cur/sao/cakeml/regression/cakeml-1047/compiler/backend/proofs/data_to_word_bignumProofScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load data_to_word_bignumProofScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Proof of 
 
 xs a frame m dm.
     (word_list a xs * frame) (fun2set (m,dm))  store_list a xs m dm = SOME m
 
 failed.
 Failed to prove theorem word_list_IMP_store_list.
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
stack_allocProofTheory                                                  M-KILLED
word_to_stackProofTheory                                                M-KILLED