Job 605

CakeML:8b46c3a87cb343ec13b54a05bfb531841eb60955
  Fix bug in tag_name (picks an unused cons name) [Dec 03 04:19:52]
HOL:3b1533784f7fffc28ed4e79c482094ece73094e5
  Remove Unicode violations in new sptree theorems [Dec 03 23:48:00]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 04 00:58:16 Claimed job
Dec 04 01:03:31 Building HOL
Dec 04 01:12:31 Starting developers
Dec 04 01:12:34 Finished developers                                               2s  20MB
Dec 04 01:12:34 Starting developers/bin
Dec 04 01:13:47 Finished developers/bin                                        1m12s 916MB
Dec 04 01:13:48 Starting semantics/ffi
Dec 04 01:14:26 Finished semantics/ffi                                           37s 480MB
Dec 04 01:14:26 Starting semantics
Dec 04 01:15:58 Finished semantics                                             1m30s 881MB
Dec 04 01:15:58 Starting semantics/proofs
Dec 04 01:18:49 Finished semantics/proofs                                      2m50s   1GB
Dec 04 01:18:50 Starting basis/pure
Dec 04 01:22:26 Finished basis/pure                                            3m35s 616MB
Dec 04 01:22:27 Starting translator
Dec 04 01:23:41 Finished translator                                            1m13s 955MB
Dec 04 01:23:42 Starting compiler/parsing
Dec 04 01:24:58 Finished compiler/parsing                                      1m16s   2GB
Dec 04 01:24:59 Starting characteristic
Dec 04 01:27:32 Finished characteristic                                        2m32s   1GB
Dec 04 01:27:33 Starting translator/monadic
Dec 04 01:28:59 Finished translator/monadic                                    1m24s   1GB
Dec 04 01:28:59 Starting basis
Dec 04 01:44:59 Finished basis                                                15m59s   2GB
Dec 04 01:45:00 Starting compiler/inference
Dec 04 01:46:43 Finished compiler/inference                                    1m42s   1GB
Dec 04 01:46:43 Starting compiler/backend/reg_alloc
Dec 04 01:47:31 Finished compiler/backend/reg_alloc                              46s   1GB
Dec 04 01:47:31 Starting compiler/backend/gc
Dec 04 01:54:54 Finished compiler/backend/gc                                   7m21s   2GB
Dec 04 01:54:54 Starting compiler/backend
Dec 04 01:54:57 Finished compiler/backend                                         2s  18MB
Dec 04 01:54:58 Starting compiler/encoders/asm
Dec 04 01:55:00 Finished compiler/encoders/asm                                    1s  15MB
Dec 04 01:55:01 Starting compiler/encoders/x64
Dec 04 01:55:51 Finished compiler/encoders/x64                                   50s 523MB
Dec 04 01:55:52 Starting compiler/encoders/arm6
Dec 04 01:57:34 Finished compiler/encoders/arm6                                1m41s   1GB
Dec 04 01:57:35 Starting compiler/encoders/arm8
Dec 04 01:58:02 Finished compiler/encoders/arm8                                  26s 476MB
Dec 04 01:58:03 Starting compiler/encoders/mips
Dec 04 01:59:01 Finished compiler/encoders/mips                                  57s 850MB
Dec 04 01:59:02 Starting compiler/encoders/riscv
Dec 04 02:00:03 Finished compiler/encoders/riscv                               1m00s 690MB
Dec 04 02:00:04 Starting compiler/encoders/ag32
Dec 04 02:00:21 Finished compiler/encoders/ag32                                  16s 661MB
Dec 04 02:00:22 Starting compiler/backend/x64
Dec 04 02:00:40 Finished compiler/backend/x64                                    17s   1GB
Dec 04 02:00:41 Starting compiler/backend/arm6
Dec 04 02:01:02 Finished compiler/backend/arm6                                   20s   1GB
Dec 04 02:01:02 Starting compiler/backend/arm8
Dec 04 02:01:20 Finished compiler/backend/arm8                                   17s 873MB
Dec 04 02:01:21 Starting compiler/backend/mips
Dec 04 02:01:41 Finished compiler/backend/mips                                   19s 904MB
Dec 04 02:01:41 Starting compiler/backend/riscv
Dec 04 02:02:00 Finished compiler/backend/riscv                                  18s   1GB
Dec 04 02:02:01 Starting compiler/backend/ag32
Dec 04 02:03:12 Finished compiler/backend/ag32                                 1m10s   1GB
Dec 04 02:03:13 Starting compiler/parsing/proofs
Dec 04 02:09:12 Finished compiler/parsing/proofs                               5m58s 846MB
Dec 04 02:09:13 Starting compiler/inference/proofs
Dec 04 02:12:05 Finished compiler/inference/proofs                             2m51s 983MB
Dec 04 02:12:06 Starting compiler/backend/semantics
Dec 04 02:20:54 Finished compiler/backend/semantics                            8m47s   1GB
Dec 04 02:20:55 Starting compiler/backend/reg_alloc/proofs
Dec 04 02:23:40 Finished compiler/backend/reg_alloc/proofs                     2m44s 622MB
Dec 04 02:23:40 Starting compiler/backend/proofs
Dec 04 02:24:02 FAILED: compiler/backend/proofs
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../../basis/pure]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/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-3b1533784f7fffc28ed4e79c482094ece73094e5/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-3b1533784f7fffc28ed4e79c482094ece73094e5/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-605/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