Job 1794

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into: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:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 24 12:47:15 Claimed job
Feb 24 12:47:16 Reusing HOL
Feb 24 12:47:29 Starting developers
Feb 24 12:47:33 Finished developers                                               4s 115MB
Feb 24 12:47:33 Starting developers/bin
Feb 24 12:47:38 Finished developers/bin                                           4s 675MB
Feb 24 12:47:38 Starting semantics/ffi
Feb 24 12:47:48 Finished semantics/ffi                                            9s 251MB
Feb 24 12:47:48 Starting semantics
Feb 24 12:49:50 Finished semantics                                             2m02s   1GB
Feb 24 12:49:50 Starting semantics/proofs
Feb 24 12:53:29 Finished semantics/proofs                                      3m38s   1GB
Feb 24 12:53:29 Starting semantics/alt_semantics
Feb 24 12:53:46 Finished semantics/alt_semantics                                 16s 494MB
Feb 24 12:53:46 Starting semantics/alt_semantics/proofs
Feb 24 12:56:13 Finished semantics/alt_semantics/proofs                        2m27s 814MB
Feb 24 12:56:14 Starting basis/pure
Feb 24 12:57:16 Finished basis/pure                                            1m02s 877MB
Feb 24 12:57:16 Starting translator
Feb 24 13:00:20 Finished translator                                            3m03s   2GB
Feb 24 13:00:21 Starting compiler/parsing
Feb 24 13:01:34 Finished compiler/parsing                                      1m13s   2GB
Feb 24 13:01:34 Starting characteristic
Feb 24 13:07:57 Finished characteristic                                        6m23s   1GB
Feb 24 13:07:57 Starting translator/monadic
Feb 24 13:09:53 Finished translator/monadic                                    1m55s   1GB
Feb 24 13:09:53 Starting basis
Feb 24 13:56:03 Finished basis                                                46m09s  18GB
Feb 24 13:56:03 Starting compiler/inference
Feb 24 13:57:23 Finished compiler/inference                                    1m19s   1GB
Feb 24 13:57:23 Starting compiler/backend/reg_alloc
Feb 24 13:59:07 Finished compiler/backend/reg_alloc                            1m44s   1GB
Feb 24 13:59:08 Starting compiler/backend/gc
Feb 24 14:03:27 Finished compiler/backend/gc                                   4m18s   1GB
Feb 24 14:03:27 Starting compiler/backend
Feb 24 14:08:53 Finished compiler/backend                                      5m25s   2GB
Feb 24 14:08:53 Starting compiler/encoders/asm
Feb 24 14:09:22 Finished compiler/encoders/asm                                   29s 694MB
Feb 24 14:09:22 Starting compiler/encoders/x64
Feb 24 14:09:52 Finished compiler/encoders/x64                                   29s   1GB
Feb 24 14:09:52 Starting compiler/encoders/arm7
Feb 24 14:10:46 Finished compiler/encoders/arm7                                  54s 809MB
Feb 24 14:10:46 Starting compiler/encoders/arm8
Feb 24 14:11:03 Finished compiler/encoders/arm8                                  16s 955MB
Feb 24 14:11:03 Starting compiler/encoders/arm8_asl
Feb 24 14:13:36 Finished compiler/encoders/arm8_asl                            2m32s 956MB
Feb 24 14:13:36 Starting compiler/encoders/mips
Feb 24 14:13:57 Finished compiler/encoders/mips                                  21s   1GB
Feb 24 14:13:57 Starting compiler/encoders/riscv
Feb 24 14:14:16 Finished compiler/encoders/riscv                                 18s 866MB
Feb 24 14:14:16 Starting compiler/encoders/ag32
Feb 24 14:14:38 Finished compiler/encoders/ag32                                  22s 690MB
Feb 24 14:14:38 Starting compiler/backend/x64
Feb 24 14:15:01 Finished compiler/backend/x64                                    22s   1GB
Feb 24 14:15:01 Starting compiler/backend/arm7
Feb 24 14:15:25 Finished compiler/backend/arm7                                   24s   1GB
Feb 24 14:15:25 Starting compiler/backend/arm8
Feb 24 14:15:47 Finished compiler/backend/arm8                                   21s   1GB
Feb 24 14:15:47 Starting compiler/backend/mips
Feb 24 14:16:09 Finished compiler/backend/mips                                   21s   1GB
Feb 24 14:16:09 Starting compiler/backend/riscv
Feb 24 14:16:31 Finished compiler/backend/riscv                                  21s   1GB
Feb 24 14:16:31 Starting compiler/backend/ag32
Feb 24 14:17:57 Finished compiler/backend/ag32                                 1m25s   1GB
Feb 24 14:17:57 Starting compiler/parsing/proofs
Feb 24 14:21:43 Finished compiler/parsing/proofs                               3m45s   1GB
Feb 24 14:21:43 Starting compiler/inference/proofs
Feb 24 14:24:14 Finished compiler/inference/proofs                             2m31s   1GB
Feb 24 14:24:14 Starting compiler/backend/semantics
Feb 24 14:52:23 Finished compiler/backend/semantics                           28m08s   2GB
Feb 24 14:52:23 Starting compiler/backend/reg_alloc/proofs
Feb 24 14:55:55 Finished compiler/backend/reg_alloc/proofs                     3m31s 845MB
Feb 24 14:55:55 Starting compiler/backend/proofs
Feb 24 15:48:10 Finished compiler/backend/proofs                              52m10s  15GB
Feb 24 15:48:10 Starting compiler/backend/serialiser
Feb 24 15:49:48 Finished compiler/backend/serialiser                           1m38s   2GB
Feb 24 15:49:48 Starting compiler/encoders/x64/proofs
Feb 24 15:59:19 Finished compiler/encoders/x64/proofs                          9m31s   4GB
Feb 24 15:59:20 Starting compiler/encoders/arm7/proofs
Feb 24 16:12:32 Finished compiler/encoders/arm7/proofs                        13m12s   7GB
Feb 24 16:12:33 Starting compiler/encoders/arm8/proofs
Feb 24 16:19:19 Finished compiler/encoders/arm8/proofs                         6m46s   1GB
Feb 24 16:19:19 Starting compiler/encoders/arm8_asl/proofs
Feb 24 16:34:41 Finished compiler/encoders/arm8_asl/proofs                    15m21s   2GB
Feb 24 16:34:41 Starting compiler/encoders/mips/proofs
Feb 24 16:44:46 Finished compiler/encoders/mips/proofs                        10m04s   2GB
Feb 24 16:44:46 Starting compiler/encoders/riscv/proofs
Feb 24 16:53:26 Finished compiler/encoders/riscv/proofs                        8m39s   1GB
Feb 24 16:53:26 Starting compiler/encoders/ag32/proofs
Feb 24 16:56:01 Finished compiler/encoders/ag32/proofs                         2m35s 716MB
Feb 24 16:56:02 Starting compiler/backend/x64/proofs
Feb 24 16:56:28 Finished compiler/backend/x64/proofs                             26s   1GB
Feb 24 16:56:28 Starting compiler/backend/arm7/proofs
Feb 24 16:56:56 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 24 16:56:56 Starting compiler/backend/arm8/proofs
Feb 24 16:57:24 Finished compiler/backend/arm8/proofs                            27s   1GB
Feb 24 16:57:24 Starting compiler/backend/arm8_asl
Feb 24 16:57:54 Finished compiler/backend/arm8_asl                               30s   1GB
Feb 24 16:57:54 Starting compiler/backend/mips/proofs
Feb 24 16:58:22 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 24 16:58:22 Starting compiler/backend/riscv/proofs
Feb 24 16:58:50 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 24 16:58:50 Starting compiler/backend/ag32/proofs
Feb 24 17:11:38 Finished compiler/backend/ag32/proofs                         12m47s   3GB
Feb 24 17:11:38 Starting compiler/proofs
Feb 24 17:13:48 Finished compiler/proofs                                       2m09s   3GB
Feb 24 17:13:48 Starting candle/set-theory
Feb 24 17:14:23 Finished candle/set-theory                                       34s   1GB
Feb 24 17:14:23 Starting candle/syntax-lib
Feb 24 17:14:36 Finished candle/syntax-lib                                       13s 573MB
Feb 24 17:14:36 Starting candle/standard/syntax
Feb 24 17:16:40 Finished candle/standard/syntax                                2m03s   1GB
Feb 24 17:16:40 Starting candle/standard/semantics
Feb 24 17:18:27 Finished candle/standard/semantics                             1m47s 988MB
Feb 24 17:18:27 Starting candle/standard/monadic
Feb 24 17:20:22 Finished candle/standard/monadic                               1m54s   1GB
Feb 24 17:20:22 Starting candle/standard/ml_kernel
Feb 24 17:26:29 Finished candle/standard/ml_kernel                             6m06s   4GB
Feb 24 17:26:29 Starting candle/overloading/syntax
Feb 24 17:29:40 Finished candle/overloading/syntax                             3m11s   1GB
Feb 24 17:29:41 Starting candle/overloading/semantics
Feb 24 17:41:24 Finished candle/overloading/semantics                         11m43s   3GB
Feb 24 17:41:24 Starting candle/overloading/monadic
Feb 24 17:43:56 Finished candle/overloading/monadic                            2m31s   1GB
Feb 24 17:43:56 Starting candle/overloading/ml_kernel
Feb 24 17:51:09 Finished candle/overloading/ml_kernel                          7m13s   3GB
Feb 24 17:51:09 Starting candle/overloading/ml_checker
Feb 24 17:53:35 Finished candle/overloading/ml_checker                         2m23s   3GB
Feb 24 17:53:35 Starting candle/prover
Feb 24 18:01:02 Finished candle/prover                                         7m26s   3GB
Feb 24 18:01:02 Starting pancake
Feb 24 18:03:41 Finished pancake                                               2m39s   2GB
Feb 24 18:03:41 Starting pancake/ffi
Feb 24 18:03:41 Finished pancake/ffi                                              0s  35MB
Feb 24 18:03:42 Starting pancake/semantics
Feb 24 18:06:08 Finished pancake/semantics                                     2m26s   1GB
Feb 24 18:06:08 Starting pancake/proofs
Feb 24 18:07:53 FAILED: pancake/proofs
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/pancake/semantics[0m
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                                                                                                                                                             (26s)     OK
Starting work on loop_liveProofTheory
pan_simpProofTheory                                                                                                                                                              (36s)     OK
Starting work on time_to_panProofTheory
loop_liveProofTheory                                                                                                                                                             (27s)     OK
Starting work on crep_to_loopProofTheory
loop_removeProofTheory                                                                                                                                                           (82s)     OK
Starting work on loop_to_wordProofTheory
loop_to_wordProofTheory                                                                                                                                                          (15s)FAIL<1>
 
 EL (k + 1) (retv::l) = EL k l
 
 Failed to prove theorem locals_rel_make_ctxt.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cug/hk324/cml-regression/cakeml-1794/pancake/proofs/loop_to_wordProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-1794/pancake/proofs/loop_to_wordProofScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
pan_to_crepProofTheory                                                                                                                                                          (100s)MKILLED
time_to_panProofTheory                                                                                                                                                           (62s)MKILLED
crep_to_loopProofTheory                                                                                                                                                          (44s)MKILLED