Job 603

CakeML:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name) [Dec 03 04:19:52]
HOL:c9c61af817d969987f437812efd5a7ee6f91a372
  Make emacs mode's temp files have Script.sml suffix [Dec 03 05:41:48]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 03 09:52:01 Claimed job
Dec 03 09:53:05 Building HOL
Dec 03 10:02:05 Starting developers
Dec 03 10:02:08 Finished developers                                               2s  20MB
Dec 03 10:02:09 Starting developers/bin
Dec 03 10:03:13 Finished developers/bin                                        1m03s 916MB
Dec 03 10:03:13 Starting semantics/ffi
Dec 03 10:03:52 Finished semantics/ffi                                           37s 312MB
Dec 03 10:03:52 Starting semantics
Dec 03 10:05:24 Finished semantics                                             1m30s 989MB
Dec 03 10:05:24 Starting semantics/proofs
Dec 03 10:08:18 Finished semantics/proofs                                      2m52s   1GB
Dec 03 10:08:18 Starting basis/pure
Dec 03 10:11:57 Finished basis/pure                                            3m38s 679MB
Dec 03 10:11:58 Starting translator
Dec 03 10:13:12 Finished translator                                            1m13s 951MB
Dec 03 10:13:13 Starting compiler/parsing
Dec 03 10:14:30 Finished compiler/parsing                                      1m16s   1GB
Dec 03 10:14:30 Starting characteristic
Dec 03 10:17:01 Finished characteristic                                        2m30s   1GB
Dec 03 10:17:02 Starting translator/monadic
Dec 03 10:18:31 Finished translator/monadic                                    1m28s   1GB
Dec 03 10:18:32 Starting basis
Dec 03 10:34:40 Finished basis                                                16m07s   3GB
Dec 03 10:34:41 Starting compiler/inference
Dec 03 10:36:24 Finished compiler/inference                                    1m42s   1GB
Dec 03 10:36:24 Starting compiler/backend/reg_alloc
Dec 03 10:37:12 Finished compiler/backend/reg_alloc                              46s 951MB
Dec 03 10:37:13 Starting compiler/backend/gc
Dec 03 10:44:39 Finished compiler/backend/gc                                   7m25s   1GB
Dec 03 10:44:40 Starting compiler/backend
Dec 03 10:44:43 Finished compiler/backend                                         2s  21MB
Dec 03 10:44:44 Starting compiler/encoders/asm
Dec 03 10:44:46 Finished compiler/encoders/asm                                    1s  22MB
Dec 03 10:44:47 Starting compiler/encoders/x64
Dec 03 10:45:37 Finished compiler/encoders/x64                                   50s 522MB
Dec 03 10:45:38 Starting compiler/encoders/arm6
Dec 03 10:47:20 Finished compiler/encoders/arm6                                1m41s   1GB
Dec 03 10:47:21 Starting compiler/encoders/arm8
Dec 03 10:47:48 Finished compiler/encoders/arm8                                  26s 476MB
Dec 03 10:47:49 Starting compiler/encoders/mips
Dec 03 10:48:47 Finished compiler/encoders/mips                                  57s 895MB
Dec 03 10:48:48 Starting compiler/encoders/riscv
Dec 03 10:49:50 Finished compiler/encoders/riscv                               1m01s 863MB
Dec 03 10:49:50 Starting compiler/encoders/ag32
Dec 03 10:50:08 Finished compiler/encoders/ag32                                  17s 744MB
Dec 03 10:50:09 Starting compiler/backend/x64
Dec 03 10:50:28 Finished compiler/backend/x64                                    18s   1GB
Dec 03 10:50:28 Starting compiler/backend/arm6
Dec 03 10:50:47 Finished compiler/backend/arm6                                   18s   1GB
Dec 03 10:50:48 Starting compiler/backend/arm8
Dec 03 10:51:06 Finished compiler/backend/arm8                                   17s 951MB
Dec 03 10:51:06 Starting compiler/backend/mips
Dec 03 10:51:26 Finished compiler/backend/mips                                   18s 857MB
Dec 03 10:51:26 Starting compiler/backend/riscv
Dec 03 10:51:46 Finished compiler/backend/riscv                                  18s   1GB
Dec 03 10:51:46 Starting compiler/backend/ag32
Dec 03 10:53:01 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 03 10:53:02 Starting compiler/parsing/proofs
Dec 03 10:59:08 Finished compiler/parsing/proofs                               6m05s 789MB
Dec 03 10:59:08 Starting compiler/inference/proofs
Dec 03 11:01:59 Finished compiler/inference/proofs                             2m50s 981MB
Dec 03 11:02:00 Starting compiler/backend/semantics
Dec 03 11:10:49 Finished compiler/backend/semantics                            8m48s   1GB
Dec 03 11:10:49 Starting compiler/backend/reg_alloc/proofs
Dec 03 11:13:33 Finished compiler/backend/reg_alloc/proofs                     2m42s 543MB
Dec 03 11:13:33 Starting compiler/backend/proofs
Dec 03 11:13:55 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ..]0;Holmake: ../reg_alloc]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../translator/monadic/monad_base]0;Holmake: ../../../translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ../reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../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-c9c61af817d969987f437812efd5a7ee6f91a372/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-c9c61af817d969987f437812efd5a7ee6f91a372/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: ..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: ../../../translator/monadic]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../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 heap
Starting work on README.md
README.md                                                                    OK
heap                                                                         OK
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_liveProofTheory                                                FAILED! <1>
 error in quse /home/cake/oven/regression/cakeml-603/compiler/backend/proofs/data_liveProofScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 77", origin_function = "by", origin_structure = "BasicProvers"}
 error in load data_liveProofScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 77", origin_function = "by", origin_structure = "BasicProvers"}
 Proof of 
 
 args s1 t1 t xs.
     state_rel s1 t1 (list_insert args t)  get_vars args s1.locals = SOME xs 
     get_vars args t1.locals = SOME xs
 
 failed.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 77", origin_function = "by", origin_structure = "BasicProvers"}
bvi_tailrecProofTheory                                                 M-KILLED
data_spaceProofTheory                                                  M-KILLED
bvl_constProofTheory                                                   M-KILLED