Job 1046

CakeML:30193e4df86fc6ee1df59c8baf4b125c84ba01d4
  Merge pull request #690 from CakeML/close-files [Sep 13 07:50:45]
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 09:16:50 Claimed job
Oct 03 09:16:55 Building HOL
Oct 03 09:27:08 Starting developers
Oct 03 09:27:12 Finished developers                                               3s 120MB
Oct 03 09:27:12 Starting developers/bin
Oct 03 09:27:18 Finished developers/bin                                           5s 964MB
Oct 03 09:27:18 Starting semantics/ffi
Oct 03 09:27:54 Finished semantics/ffi                                           35s 490MB
Oct 03 09:27:54 Starting semantics
Oct 03 09:29:25 Finished semantics                                             1m30s   1GB
Oct 03 09:29:25 Starting semantics/proofs
Oct 03 09:32:14 Finished semantics/proofs                                      2m49s   1GB
Oct 03 09:32:15 Starting semantics/alt_semantics
Oct 03 09:32:22 Finished semantics/alt_semantics                                  7s 310MB
Oct 03 09:32:22 Starting semantics/alt_semantics/proofs
Oct 03 09:34:07 Finished semantics/alt_semantics/proofs                        1m44s 828MB
Oct 03 09:34:07 Starting basis/pure
Oct 03 09:37:41 Finished basis/pure                                            3m32s 826MB
Oct 03 09:37:41 Starting translator
Oct 03 09:39:24 Finished translator                                            1m42s   1GB
Oct 03 09:39:24 Starting compiler/parsing
Oct 03 09:40:18 Finished compiler/parsing                                        54s   2GB
Oct 03 09:40:18 Starting characteristic
Oct 03 09:45:30 Finished characteristic                                        5m11s   1GB
Oct 03 09:45:30 Starting translator/monadic
Oct 03 09:46:58 Finished translator/monadic                                    1m27s   1GB
Oct 03 09:46:58 Starting basis
Oct 03 10:05:47 Finished basis                                                18m49s   2GB
Oct 03 10:05:47 Starting compiler/inference
Oct 03 10:07:37 Finished compiler/inference                                    1m50s   1GB
Oct 03 10:07:37 Starting compiler/backend/reg_alloc
Oct 03 10:08:34 Finished compiler/backend/reg_alloc                              56s   1GB
Oct 03 10:08:34 Starting compiler/backend/gc
Oct 03 10:17:18 Finished compiler/backend/gc                                   8m43s   1GB
Oct 03 10:17:18 Starting compiler/backend
Oct 03 10:17:20 Finished compiler/backend                                         2s  23MB
Oct 03 10:17:20 Starting compiler/encoders/asm
Oct 03 10:17:22 Finished compiler/encoders/asm                                    1s  21MB
Oct 03 10:17:22 Starting compiler/encoders/x64
Oct 03 10:18:19 Finished compiler/encoders/x64                                   57s 936MB
Oct 03 10:18:19 Starting compiler/encoders/arm7
Oct 03 10:19:56 Finished compiler/encoders/arm7                                1m36s   1GB
Oct 03 10:19:56 Starting compiler/encoders/arm8
Oct 03 10:20:27 Finished compiler/encoders/arm8                                  30s 575MB
Oct 03 10:20:27 Starting compiler/encoders/mips
Oct 03 10:21:31 Finished compiler/encoders/mips                                1m04s 971MB
Oct 03 10:21:31 Starting compiler/encoders/riscv
Oct 03 10:22:48 Finished compiler/encoders/riscv                               1m16s   1GB
Oct 03 10:22:48 Starting compiler/encoders/ag32
Oct 03 10:23:04 Finished compiler/encoders/ag32                                  15s 850MB
Oct 03 10:23:04 Starting compiler/backend/x64
Oct 03 10:23:22 Finished compiler/backend/x64                                    18s   1GB
Oct 03 10:23:23 Starting compiler/backend/arm7
Oct 03 10:23:42 Finished compiler/backend/arm7                                   18s   1GB
Oct 03 10:23:42 Starting compiler/backend/arm8
Oct 03 10:23:59 Finished compiler/backend/arm8                                   17s   1GB
Oct 03 10:23:59 Starting compiler/backend/mips
Oct 03 10:24:17 Finished compiler/backend/mips                                   18s   1GB
Oct 03 10:24:17 Starting compiler/backend/riscv
Oct 03 10:24:36 Finished compiler/backend/riscv                                  18s   1GB
Oct 03 10:24:36 Starting compiler/backend/ag32
Oct 03 10:25:39 Finished compiler/backend/ag32                                 1m03s   1GB
Oct 03 10:25:39 Starting compiler/parsing/proofs
Oct 03 10:31:10 Finished compiler/parsing/proofs                               5m29s 926MB
Oct 03 10:31:10 Starting compiler/inference/proofs
Oct 03 10:33:50 Finished compiler/inference/proofs                             2m40s   1GB
Oct 03 10:33:50 Starting compiler/backend/semantics
Oct 03 10:39:22 Finished compiler/backend/semantics                            5m31s   2GB
Oct 03 10:39:22 Starting compiler/backend/reg_alloc/proofs
Oct 03 10:42:26 Finished compiler/backend/reg_alloc/proofs                     3m03s 795MB
Oct 03 10:42:26 Starting compiler/backend/proofs
Oct 03 10:59:33 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-1046/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-1046/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-1046/basis/pure]0;Holmake: ~/cakeml/regression/cakeml-1046/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-1046/misc]0;Holmake: ~/cakeml/regression/cakeml-1046/developers]0;Holmake: ~/cakeml/regression/cakeml-1046/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/misc]0;Holmake: ~/cakeml/regression/cakeml-1046/misc/lem_lib_stub]0;Holmake: ~/cakeml/regression/cakeml-1046/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/misc]0;Holmake: ~/cakeml/regression/cakeml-1046/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/basis/pure]0;Holmake: ~/cakeml/regression/cakeml-1046/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ~/cakeml/regression/cakeml-1046/translator/monadic/monad_base]0;Holmake: ~/cakeml/regression/cakeml-1046/semantics]0;Holmake: ~/cakeml/regression/cakeml-1046/semantics/ffi]0;Holmake: ~/cakeml/regression/cakeml-1046/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/semantics]0;Holmake: ~/cakeml/regression/cakeml-1046/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/translator/monadic/monad_base]0;Holmake: ~/cakeml/regression/cakeml-1046/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ../reg_alloc]0;Holmake: ~/cakeml/regression/cakeml-1046/unverified/reg_alloc]0;Holmake: ~/cakeml/regression/cakeml-1046/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-1046/semantics/proofs]0;Holmake: ~/cakeml/regression/cakeml-1046/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-1046/translator/monadic]0;Holmake: ~/cakeml/regression/cakeml-1046/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1046/compiler/parsing]0;Holmake: ~/cakeml/regression/cakeml-1046/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1046/translator]0;Holmake: ~/cakeml/regression/cakeml-1046/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1046/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/cakeml/regression/cakeml-1046/translator/monadic]0;Holmake: ~/cakeml/regression/cakeml-1046/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:   11s  user:   10s     OK
Starting work on bvl_constProofTheory
data_spaceProofTheory                           real:   19s  user:   18s     OK
Starting work on bvi_letProofTheory
bvi_letProofTheory                              real:   16s  user:   15s     OK
Starting work on clos_annotateProofTheory
data_liveProofTheory                            real:   39s  user:   38s     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:   28s  user:   26s     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:   88s  user:   86s     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:  156s  user:  154s     OK
Starting work on bvl_to_bviProofTheory
clos_mtiProofTheory                             real:   32s  user:   31s     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:  154s  user:  152s     OK
Starting work on word_bignumProofTheory
word_simpProofTheory                            real:   47s  user:   45s     OK
Starting work on word_gcFunctionsTheory
clos_knownProofTheory                           real:  114s  user:  112s     OK
Starting work on clos_to_bvlProofTheory
word_gcFunctionsTheory                          real:   25s  user:   24s     OK
Starting work on data_to_word_memoryProofTheory
bvl_to_bviProofTheory                           real:  170s  user:  166s     OK
Starting work on word_allocProofTheory
word_bignumProofTheory                          real:  185s  user:  181s     OK
Starting work on word_instProofTheory
word_instProofTheory                            real:   42s  user:   40s     OK
Starting work on word_removeProofTheory
clos_to_bvlProofTheory                          real:  181s  user:  177s     OK
Starting work on flat_to_patProofTheory
word_removeProofTheory                          real:   23s  user:   22s     OK
Starting work on lab_filterProofTheory
lab_filterProofTheory                           real:   52s  user:   50s     OK
Starting work on stack_removeProofTheory
flat_to_patProofTheory                          real:   93s  user:   91s     OK
Starting work on pat_to_closProofTheory
pat_to_closProofTheory                          real:   31s  user:   30s     OK
Starting work on flat_elimProofTheory
flat_elimProofTheory                            real:   39s  user:   37s     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:   22s  user:   21s     OK
Starting work on source_to_flatProofTheory
stack_removeProofTheory                         real:  222s  user:  219s     OK
Starting work on lab_to_targetProofTheory
word_allocProofTheory                           real:  425s  user:  420s     OK
Starting work on word_to_wordProofTheory
source_to_flatProofTheory                       real:   73s  user:   71s     OK
Starting work on stack_allocProofTheory
word_to_wordProofTheory                         real:   53s  user:   52s     OK
Starting work on stack_namesProofTheory
stack_namesProofTheory                          real:   27s  user:   26s     OK
Starting work on word_to_stackProofTheory
data_to_word_memoryProofTheory                  real:  553s  user:  549s     OK
Starting work on data_to_word_gcProofTheory
lab_to_targetProofTheory                        real:  205s  user:  202s     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:   69s  user:   67s     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-1046/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