Job 1792

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:9ca376e4b966f480ad209d4c7b8a42e2ae1e71ac
  Fix ag32_ffi_memoryProof for DIV_NUMERAL_THM (becomes simpler) [Feb 24 00:18: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 07:18:14 Claimed job
Feb 24 07:18:17 Reusing HOL
Feb 24 07:18:29 Starting developers
Feb 24 07:18:34 Finished developers                                               4s 160MB
Feb 24 07:18:34 Starting developers/bin
Feb 24 07:18:38 Finished developers/bin                                           4s 675MB
Feb 24 07:18:38 Starting semantics/ffi
Feb 24 07:18:48 Finished semantics/ffi                                            9s 237MB
Feb 24 07:18:48 Starting semantics
Feb 24 07:20:50 Finished semantics                                             2m02s   1GB
Feb 24 07:20:50 Starting semantics/proofs
Feb 24 07:24:28 Finished semantics/proofs                                      3m37s   1GB
Feb 24 07:24:28 Starting semantics/alt_semantics
Feb 24 07:24:45 Finished semantics/alt_semantics                                 16s 536MB
Feb 24 07:24:45 Starting semantics/alt_semantics/proofs
Feb 24 07:27:14 Finished semantics/alt_semantics/proofs                        2m28s   1GB
Feb 24 07:27:14 Starting basis/pure
Feb 24 07:28:17 Finished basis/pure                                            1m03s 895MB
Feb 24 07:28:17 Starting translator
Feb 24 07:31:19 Finished translator                                            3m01s   1GB
Feb 24 07:31:19 Starting compiler/parsing
Feb 24 07:32:32 Finished compiler/parsing                                      1m13s   3GB
Feb 24 07:32:32 Starting characteristic
Feb 24 07:38:54 Finished characteristic                                        6m21s   1GB
Feb 24 07:38:54 Starting translator/monadic
Feb 24 07:40:50 Finished translator/monadic                                    1m56s   1GB
Feb 24 07:40:50 Starting basis
Feb 24 08:26:55 Finished basis                                                46m03s  25GB
Feb 24 08:26:55 Starting compiler/inference
Feb 24 08:28:15 Finished compiler/inference                                    1m19s   1GB
Feb 24 08:28:15 Starting compiler/backend/reg_alloc
Feb 24 08:29:58 Finished compiler/backend/reg_alloc                            1m43s   1GB
Feb 24 08:29:58 Starting compiler/backend/gc
Feb 24 08:34:18 Finished compiler/backend/gc                                   4m20s   2GB
Feb 24 08:34:19 Starting compiler/backend
Feb 24 08:39:44 Finished compiler/backend                                      5m24s   2GB
Feb 24 08:39:44 Starting compiler/encoders/asm
Feb 24 08:40:14 Finished compiler/encoders/asm                                   29s 714MB
Feb 24 08:40:14 Starting compiler/encoders/x64
Feb 24 08:40:43 Finished compiler/encoders/x64                                   29s 848MB
Feb 24 08:40:43 Starting compiler/encoders/arm7
Feb 24 08:41:37 Finished compiler/encoders/arm7                                  53s   1GB
Feb 24 08:41:37 Starting compiler/encoders/arm8
Feb 24 08:41:54 Finished compiler/encoders/arm8                                  16s 931MB
Feb 24 08:41:54 Starting compiler/encoders/arm8_asl
Feb 24 08:44:26 Finished compiler/encoders/arm8_asl                            2m31s   1GB
Feb 24 08:44:26 Starting compiler/encoders/mips
Feb 24 08:44:47 Finished compiler/encoders/mips                                  21s   1GB
Feb 24 08:44:48 Starting compiler/encoders/riscv
Feb 24 08:45:08 Finished compiler/encoders/riscv                                 19s 865MB
Feb 24 08:45:08 Starting compiler/encoders/ag32
Feb 24 08:45:30 Finished compiler/encoders/ag32                                  21s 689MB
Feb 24 08:45:30 Starting compiler/backend/x64
Feb 24 08:45:53 Finished compiler/backend/x64                                    23s   1GB
Feb 24 08:45:53 Starting compiler/backend/arm7
Feb 24 08:46:17 Finished compiler/backend/arm7                                   23s   1GB
Feb 24 08:46:17 Starting compiler/backend/arm8
Feb 24 08:46:40 Finished compiler/backend/arm8                                   23s   1GB
Feb 24 08:46:41 Starting compiler/backend/mips
Feb 24 08:47:02 Finished compiler/backend/mips                                   21s   1GB
Feb 24 08:47:02 Starting compiler/backend/riscv
Feb 24 08:47:24 Finished compiler/backend/riscv                                  21s   1GB
Feb 24 08:47:24 Starting compiler/backend/ag32
Feb 24 08:48:50 Finished compiler/backend/ag32                                 1m26s   1GB
Feb 24 08:48:50 Starting compiler/parsing/proofs
Feb 24 08:52:36 Finished compiler/parsing/proofs                               3m45s   1GB
Feb 24 08:52:36 Starting compiler/inference/proofs
Feb 24 08:55:05 Finished compiler/inference/proofs                             2m28s   1GB
Feb 24 08:55:05 Starting compiler/backend/semantics
Feb 24 09:24:04 Finished compiler/backend/semantics                           28m59s   2GB
Feb 24 09:24:04 Starting compiler/backend/reg_alloc/proofs
Feb 24 09:27:38 Finished compiler/backend/reg_alloc/proofs                     3m32s 764MB
Feb 24 09:27:38 Starting compiler/backend/proofs
Feb 24 10:19:49 Finished compiler/backend/proofs                              52m11s  14GB
Feb 24 10:19:50 Starting compiler/backend/serialiser
Feb 24 10:21:28 Finished compiler/backend/serialiser                           1m38s   2GB
Feb 24 10:21:28 Starting compiler/encoders/x64/proofs
Feb 24 10:31:18 Finished compiler/encoders/x64/proofs                          9m48s   5GB
Feb 24 10:31:18 Starting compiler/encoders/arm7/proofs
Feb 24 10:44:17 Finished compiler/encoders/arm7/proofs                        12m59s   3GB
Feb 24 10:44:17 Starting compiler/encoders/arm8/proofs
Feb 24 10:50:59 Finished compiler/encoders/arm8/proofs                         6m41s   1GB
Feb 24 10:50:59 Starting compiler/encoders/arm8_asl/proofs
Feb 24 11:06:02 Finished compiler/encoders/arm8_asl/proofs                    15m02s   1GB
Feb 24 11:06:02 Starting compiler/encoders/mips/proofs
Feb 24 11:16:04 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Feb 24 11:16:04 Starting compiler/encoders/riscv/proofs
Feb 24 11:24:52 Finished compiler/encoders/riscv/proofs                        8m47s   1GB
Feb 24 11:24:52 Starting compiler/encoders/ag32/proofs
Feb 24 11:27:28 Finished compiler/encoders/ag32/proofs                         2m35s 742MB
Feb 24 11:27:28 Starting compiler/backend/x64/proofs
Feb 24 11:27:56 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 24 11:27:56 Starting compiler/backend/arm7/proofs
Feb 24 11:28:24 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 24 11:28:24 Starting compiler/backend/arm8/proofs
Feb 24 11:28:51 Finished compiler/backend/arm8/proofs                            26s   1GB
Feb 24 11:28:51 Starting compiler/backend/arm8_asl
Feb 24 11:29:14 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 24 11:29:14 Starting compiler/backend/mips/proofs
Feb 24 11:29:42 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 24 11:29:42 Starting compiler/backend/riscv/proofs
Feb 24 11:30:10 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 24 11:30:10 Starting compiler/backend/ag32/proofs
Feb 24 11:42:59 Finished compiler/backend/ag32/proofs                         12m45s   2GB
Feb 24 11:42:59 Starting compiler/proofs
Feb 24 11:45:24 Finished compiler/proofs                                       2m24s   3GB
Feb 24 11:45:24 Starting candle/set-theory
Feb 24 11:45:58 Finished candle/set-theory                                       34s   1GB
Feb 24 11:45:59 Starting candle/syntax-lib
Feb 24 11:46:11 Finished candle/syntax-lib                                       12s 630MB
Feb 24 11:46:11 Starting candle/standard/syntax
Feb 24 11:48:13 Finished candle/standard/syntax                                2m02s   1GB
Feb 24 11:48:14 Starting candle/standard/semantics
Feb 24 11:50:01 Finished candle/standard/semantics                             1m47s   1GB
Feb 24 11:50:01 Starting candle/standard/monadic
Feb 24 11:51:55 Finished candle/standard/monadic                               1m53s   1GB
Feb 24 11:51:55 Starting candle/standard/ml_kernel
Feb 24 11:58:14 Finished candle/standard/ml_kernel                             6m19s   3GB
Feb 24 11:58:14 Starting candle/overloading/syntax
Feb 24 12:01:26 Finished candle/overloading/syntax                             3m11s   1GB
Feb 24 12:01:27 Starting candle/overloading/semantics
Feb 24 12:13:20 Finished candle/overloading/semantics                         11m53s   2GB
Feb 24 12:13:20 Starting candle/overloading/monadic
Feb 24 12:15:53 Finished candle/overloading/monadic                            2m32s   1GB
Feb 24 12:15:54 Starting candle/overloading/ml_kernel
Feb 24 12:22:55 Finished candle/overloading/ml_kernel                          7m01s   3GB
Feb 24 12:22:55 Starting candle/overloading/ml_checker
Feb 24 12:25:20 Finished candle/overloading/ml_checker                         2m25s   3GB
Feb 24 12:25:21 Starting candle/prover
Feb 24 12:27:12 FAILED: candle/prover
Scanning [1m$(HOLDIR)/src/sort[0m
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)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[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$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanned 35 directories
Starting work on README.md
Starting work on ast_extrasTheory
README.md                                                                                                                                                                         (0s)     OK
ast_extrasTheory                                                                                                                                                                 (10s)     OK
Starting work on permsTheory
permsTheory                                                                                                                                                                      (33s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                                                                                                                                         (61s)FAIL<1>
       res = Rerr (Rabort Rtimeout_error)))  UNIT_TYPE () v
 
 failed.
 Failed to prove theorem types_v_head.
 
 Exception raised at Tactical.FIRST_ASSUM:
 
 error in quse /home/cug/hk324/cml-regression/cakeml-1792/candle/prover/candle_kernel_valsScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-1792/candle/prover/candle_kernel_valsScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}