Job 1793

CakeML:26729c20c2d37fa4e54e8e10d4f28715bd9da340
  Fix candle/prover for changes to translator and HOL [Feb 24 09:59:33]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 24 10:00:07 Claimed job
Feb 24 10:00:12 Reusing HOL
Feb 24 10:00:53 Starting developers
Feb 24 10:00:58 Finished developers                                               4s  77MB
Feb 24 10:00:59 Starting developers/bin
Feb 24 10:01:04 Finished developers/bin                                           5s 670MB
Feb 24 10:01:05 Starting semantics/ffi
Feb 24 10:01:17 Finished semantics/ffi                                           12s 220MB
Feb 24 10:01:18 Starting semantics
Feb 24 10:03:47 Finished semantics                                             2m29s 976MB
Feb 24 10:03:47 Starting semantics/proofs
Feb 24 10:08:36 Finished semantics/proofs                                      4m49s   1GB
Feb 24 10:08:37 Starting semantics/alt_semantics
Feb 24 10:08:56 Finished semantics/alt_semantics                                 19s 579MB
Feb 24 10:08:56 Starting semantics/alt_semantics/proofs
Feb 24 10:11:52 Finished semantics/alt_semantics/proofs                        2m55s   1GB
Feb 24 10:11:53 Starting basis/pure
Feb 24 10:13:05 Finished basis/pure                                            1m11s   1GB
Feb 24 10:13:05 Starting translator
Feb 24 10:17:03 Finished translator                                            3m58s   1GB
Feb 24 10:17:03 Starting compiler/parsing
Feb 24 10:18:45 Finished compiler/parsing                                      1m41s   2GB
Feb 24 10:18:45 Starting characteristic
Feb 24 10:25:52 Finished characteristic                                        7m06s   1GB
Feb 24 10:25:52 Starting translator/monadic
Feb 24 10:27:58 Finished translator/monadic                                    2m06s   1GB
Feb 24 10:27:58 Starting basis
Feb 24 11:24:30 Finished basis                                                56m29s   4GB
Feb 24 11:24:30 Starting compiler/inference
Feb 24 11:26:04 Finished compiler/inference                                    1m33s   1GB
Feb 24 11:26:04 Starting compiler/backend/reg_alloc
Feb 24 11:28:06 Finished compiler/backend/reg_alloc                            2m01s   1GB
Feb 24 11:28:06 Starting compiler/backend/gc
Feb 24 11:33:45 Finished compiler/backend/gc                                   5m38s   2GB
Feb 24 11:33:45 Starting compiler/backend
Feb 24 11:41:07 Finished compiler/backend                                      7m22s   2GB
Feb 24 11:41:07 Starting compiler/encoders/asm
Feb 24 11:41:41 Finished compiler/encoders/asm                                   33s 722MB
Feb 24 11:41:42 Starting compiler/encoders/x64
Feb 24 11:42:16 Finished compiler/encoders/x64                                   33s 857MB
Feb 24 11:42:16 Starting compiler/encoders/arm7
Feb 24 11:43:24 Finished compiler/encoders/arm7                                1m07s   1GB
Feb 24 11:43:24 Starting compiler/encoders/arm8
Feb 24 11:43:43 Finished compiler/encoders/arm8                                  19s   1GB
Feb 24 11:43:43 Starting compiler/encoders/arm8_asl
Feb 24 11:46:53 Finished compiler/encoders/arm8_asl                            3m09s 930MB
Feb 24 11:46:53 Starting compiler/encoders/mips
Feb 24 11:47:17 Finished compiler/encoders/mips                                  24s   1GB
Feb 24 11:47:18 Starting compiler/encoders/riscv
Feb 24 11:47:41 Finished compiler/encoders/riscv                                 22s 823MB
Feb 24 11:47:41 Starting compiler/encoders/ag32
Feb 24 11:48:06 Finished compiler/encoders/ag32                                  25s 906MB
Feb 24 11:48:06 Starting compiler/backend/x64
Feb 24 11:48:32 Finished compiler/backend/x64                                    25s   1GB
Feb 24 11:48:32 Starting compiler/backend/arm7
Feb 24 11:49:00 Finished compiler/backend/arm7                                   27s   1GB
Feb 24 11:49:00 Starting compiler/backend/arm8
Feb 24 11:49:26 Finished compiler/backend/arm8                                   25s   1GB
Feb 24 11:49:26 Starting compiler/backend/mips
Feb 24 11:49:53 Finished compiler/backend/mips                                   26s   1GB
Feb 24 11:49:54 Starting compiler/backend/riscv
Feb 24 11:50:18 Finished compiler/backend/riscv                                  24s   1GB
Feb 24 11:50:19 Starting compiler/backend/ag32
Feb 24 11:52:00 Finished compiler/backend/ag32                                 1m41s   1GB
Feb 24 11:52:00 Starting compiler/parsing/proofs
Feb 24 11:56:24 Finished compiler/parsing/proofs                               4m23s   1GB
Feb 24 11:56:24 Starting compiler/inference/proofs
Feb 24 11:59:24 Finished compiler/inference/proofs                             2m59s   1GB
Feb 24 11:59:24 Starting compiler/backend/semantics
Feb 24 12:38:04 Finished compiler/backend/semantics                           38m40s   1GB
Feb 24 12:38:05 Starting compiler/backend/reg_alloc/proofs
Feb 24 12:42:05 Finished compiler/backend/reg_alloc/proofs                     3m59s 958MB
Feb 24 12:42:05 Starting compiler/backend/proofs
Feb 24 13:55:00 Finished compiler/backend/proofs                            1h12m54s   5GB
Feb 24 13:55:00 Starting compiler/backend/serialiser
Feb 24 13:56:55 Finished compiler/backend/serialiser                           1m54s   1GB
Feb 24 13:56:55 Starting compiler/encoders/x64/proofs
Feb 24 14:09:25 Finished compiler/encoders/x64/proofs                         12m30s   1GB
Feb 24 14:09:26 Starting compiler/encoders/arm7/proofs
Feb 24 14:24:57 Finished compiler/encoders/arm7/proofs                        15m31s   3GB
Feb 24 14:24:57 Starting compiler/encoders/arm8/proofs
Feb 24 14:32:52 Finished compiler/encoders/arm8/proofs                         7m53s   1GB
Feb 24 14:32:52 Starting compiler/encoders/arm8_asl/proofs
Feb 24 14:50:18 Finished compiler/encoders/arm8_asl/proofs                    17m26s   1GB
Feb 24 14:50:18 Starting compiler/encoders/mips/proofs
Feb 24 15:01:11 Finished compiler/encoders/mips/proofs                        10m52s   2GB
Feb 24 15:01:11 Starting compiler/encoders/riscv/proofs
Feb 24 15:11:01 Finished compiler/encoders/riscv/proofs                        9m49s   1GB
Feb 24 15:11:01 Starting compiler/encoders/ag32/proofs
Feb 24 15:13:55 Finished compiler/encoders/ag32/proofs                         2m53s 766MB
Feb 24 15:13:55 Starting compiler/backend/x64/proofs
Feb 24 15:14:25 Finished compiler/backend/x64/proofs                             30s   1GB
Feb 24 15:14:25 Starting compiler/backend/arm7/proofs
Feb 24 15:14:57 Finished compiler/backend/arm7/proofs                            31s   1GB
Feb 24 15:14:57 Starting compiler/backend/arm8/proofs
Feb 24 15:15:26 Finished compiler/backend/arm8/proofs                            28s   1GB
Feb 24 15:15:26 Starting compiler/backend/arm8_asl
Feb 24 15:15:51 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 24 15:15:51 Starting compiler/backend/mips/proofs
Feb 24 15:16:21 Finished compiler/backend/mips/proofs                            29s   1GB
Feb 24 15:16:21 Starting compiler/backend/riscv/proofs
Feb 24 15:16:52 Finished compiler/backend/riscv/proofs                           30s   1GB
Feb 24 15:16:52 Starting compiler/backend/ag32/proofs
Feb 24 15:32:34 Finished compiler/backend/ag32/proofs                         15m41s   2GB
Feb 24 15:32:34 Starting compiler/proofs
Feb 24 15:35:33 Finished compiler/proofs                                       2m58s   3GB
Feb 24 15:35:33 Starting candle/set-theory
Feb 24 15:36:14 Finished candle/set-theory                                       40s   1GB
Feb 24 15:36:14 Starting candle/syntax-lib
Feb 24 15:36:29 Finished candle/syntax-lib                                       14s 645MB
Feb 24 15:36:29 Starting candle/standard/syntax
Feb 24 15:38:50 Finished candle/standard/syntax                                2m20s   1GB
Feb 24 15:38:50 Starting candle/standard/semantics
Feb 24 15:40:57 Finished candle/standard/semantics                             2m06s   1GB
Feb 24 15:40:57 Starting candle/standard/monadic
Feb 24 15:43:11 Finished candle/standard/monadic                               2m13s   1GB
Feb 24 15:43:11 Starting candle/standard/ml_kernel
Feb 24 15:51:15 Finished candle/standard/ml_kernel                             8m03s   2GB
Feb 24 15:51:15 Starting candle/overloading/syntax
Feb 24 15:54:59 Finished candle/overloading/syntax                             3m44s   1GB
Feb 24 15:54:59 Starting candle/overloading/semantics
Feb 24 16:08:20 Finished candle/overloading/semantics                         13m16s   2GB
Feb 24 16:08:20 Starting candle/overloading/monadic
Feb 24 16:11:20 Finished candle/overloading/monadic                            2m59s   2GB
Feb 24 16:11:20 Starting candle/overloading/ml_kernel
Feb 24 16:19:50 Finished candle/overloading/ml_kernel                          8m29s   3GB
Feb 24 16:19:50 Starting candle/overloading/ml_checker
Feb 24 16:22:31 Finished candle/overloading/ml_checker                         2m41s   3GB
Feb 24 16:22:31 Starting candle/prover
Feb 24 16:31:18 Finished candle/prover                                         8m46s   3GB
Feb 24 16:31:19 Starting pancake
Feb 24 16:34:39 Finished pancake                                               3m20s   1GB
Feb 24 16:34:40 Starting pancake/ffi
Feb 24 16:34:40 Finished pancake/ffi                                              0s  27MB
Feb 24 16:34:40 Starting pancake/semantics
Feb 24 16:37:55 Finished pancake/semantics                                     3m14s   1GB
Feb 24 16:37:56 Starting pancake/proofs
Feb 24 16:40:37 FAILED: pancake/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/pancake/semantics
Scanned 78 directories
Starting work on README.md
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
Starting work on pan_simpProofTheory
README.md                                                           (0s)     OK
Starting work on pan_to_crepProofTheory
loop_callProofTheory                                               (39s)     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                (55s)     OK
Starting work on time_to_panProofTheory
loop_liveProofTheory                                               (41s)     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                            (127s)     OK
Starting work on loop_to_wordProofTheory
loop_to_wordProofTheory                                            (24s)FAIL<1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cake/oven/regression/cakeml-1793/pancake/proofs/loop_to_wordProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cake/oven/regression/cakeml-1793/pancake/proofs/loop_to_wordProofScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 EL (k + 1) (retv::l) = EL k l
 
 Failed to prove theorem locals_rel_make_ctxt.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
pan_to_crepProofTheory                                            (154s)MKILLED
time_to_panProofTheory                                             (96s)MKILLED
crep_to_loopProofTheory                                            (69s)MKILLED