Job 1873

CakeML:ef9bc8a353452a3138710e44ca593e7cd6043828
  Remove stale code from compilerProof [Apr 25 08:07:42]
#865 (Iced_cake)
Merging into:915403669818aaaea2c42cd400fad0542de3fa99
  Merge pull request #878 from CakeML/array-appi-fix [Apr 20 08:36:39]
HOL:cb44cc2412d08a2baf1dd127ba6dc5f565e2834b
  "orthogonal edge routing" style of core theory hierarchy graph [Apr 14 03:45:39]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Apr 25 08:21:06 Claimed job
Apr 25 08:21:09 Reusing HOL
Apr 25 08:21:22 Starting developers
Apr 25 08:21:23 Finished developers                                               1s  36MB
Apr 25 08:21:23 Starting developers/bin
Apr 25 08:22:00 Finished developers/bin                                          37s   1GB
Apr 25 08:22:01 Starting semantics/ffi
Apr 25 08:22:12 Finished semantics/ffi                                           10s 242MB
Apr 25 08:22:12 Starting semantics
Apr 25 08:24:37 Finished semantics                                             2m25s   1GB
Apr 25 08:24:37 Starting semantics/proofs
Apr 25 08:31:38 Finished semantics/proofs                                      7m00s   1GB
Apr 25 08:31:38 Starting semantics/alt_semantics
Apr 25 08:32:05 Finished semantics/alt_semantics                                 26s 572MB
Apr 25 08:32:06 Starting semantics/alt_semantics/proofs
Apr 25 08:43:36 Finished semantics/alt_semantics/proofs                       11m30s   1GB
Apr 25 08:43:36 Starting basis/pure
Apr 25 08:44:41 Finished basis/pure                                            1m05s 863MB
Apr 25 08:44:41 Starting translator
Apr 25 08:48:23 Finished translator                                            3m41s   1GB
Apr 25 08:48:23 Starting compiler/parsing
Apr 25 08:49:49 Finished compiler/parsing                                      1m25s   5GB
Apr 25 08:49:49 Starting characteristic
Apr 25 08:56:43 Finished characteristic                                        6m54s   1GB
Apr 25 08:56:44 Starting translator/monadic
Apr 25 08:58:41 Finished translator/monadic                                    1m57s   1GB
Apr 25 08:58:41 Starting basis
Apr 25 09:49:27 Finished basis                                                50m44s  23GB
Apr 25 09:49:27 Starting compiler/inference
Apr 25 09:50:58 Finished compiler/inference                                    1m30s   1GB
Apr 25 09:50:58 Starting compiler/backend/reg_alloc
Apr 25 09:52:43 Finished compiler/backend/reg_alloc                            1m45s   1GB
Apr 25 09:52:44 Starting compiler/backend/gc
Apr 25 09:57:10 Finished compiler/backend/gc                                   4m26s   2GB
Apr 25 09:57:10 Starting compiler/backend
Apr 25 10:02:58 Finished compiler/backend                                      5m48s   2GB
Apr 25 10:02:59 Starting compiler/encoders/asm
Apr 25 10:03:29 Finished compiler/encoders/asm                                   30s 683MB
Apr 25 10:03:29 Starting compiler/encoders/x64
Apr 25 10:03:59 Finished compiler/encoders/x64                                   30s   1GB
Apr 25 10:04:00 Starting compiler/encoders/arm7
Apr 25 10:04:53 Finished compiler/encoders/arm7                                  53s 753MB
Apr 25 10:04:54 Starting compiler/encoders/arm8
Apr 25 10:05:11 Finished compiler/encoders/arm8                                  16s   1GB
Apr 25 10:05:11 Starting compiler/encoders/arm8_asl
Apr 25 10:07:42 Finished compiler/encoders/arm8_asl                            2m31s 984MB
Apr 25 10:07:42 Starting compiler/encoders/mips
Apr 25 10:08:04 Finished compiler/encoders/mips                                  21s   1GB
Apr 25 10:08:04 Starting compiler/encoders/riscv
Apr 25 10:08:24 Finished compiler/encoders/riscv                                 19s 961MB
Apr 25 10:08:24 Starting compiler/encoders/ag32
Apr 25 10:08:46 Finished compiler/encoders/ag32                                  21s 713MB
Apr 25 10:08:46 Starting compiler/backend/x64
Apr 25 10:09:09 Finished compiler/backend/x64                                    22s   1GB
Apr 25 10:09:09 Starting compiler/backend/arm7
Apr 25 10:09:33 Finished compiler/backend/arm7                                   23s   1GB
Apr 25 10:09:34 Starting compiler/backend/arm8
Apr 25 10:09:56 Finished compiler/backend/arm8                                   22s   1GB
Apr 25 10:09:56 Starting compiler/backend/mips
Apr 25 10:10:20 Finished compiler/backend/mips                                   23s   1GB
Apr 25 10:10:20 Starting compiler/backend/riscv
Apr 25 10:10:43 Finished compiler/backend/riscv                                  23s   1GB
Apr 25 10:10:43 Starting compiler/backend/ag32
Apr 25 10:12:11 Finished compiler/backend/ag32                                 1m27s   1GB
Apr 25 10:12:11 Starting compiler/parsing/proofs
Apr 25 10:15:55 Finished compiler/parsing/proofs                               3m43s   1GB
Apr 25 10:15:55 Starting compiler/inference/proofs
Apr 25 10:18:41 Finished compiler/inference/proofs                             2m45s 995MB
Apr 25 10:18:41 Starting compiler/backend/semantics
Apr 25 10:52:13 Finished compiler/backend/semantics                           33m31s   2GB
Apr 25 10:52:13 Starting compiler/backend/reg_alloc/proofs
Apr 25 10:55:48 Finished compiler/backend/reg_alloc/proofs                     3m35s 996MB
Apr 25 10:55:49 Starting compiler/backend/proofs
Apr 25 11:51:10 Finished compiler/backend/proofs                              55m21s  15GB
Apr 25 11:51:10 Starting compiler/backend/serialiser
Apr 25 11:52:54 Finished compiler/backend/serialiser                           1m43s   2GB
Apr 25 11:52:54 Starting compiler/encoders/x64/proofs
Apr 25 12:02:39 Finished compiler/encoders/x64/proofs                          9m45s   4GB
Apr 25 12:02:40 Starting compiler/encoders/arm7/proofs
Apr 25 12:15:59 Finished compiler/encoders/arm7/proofs                        13m19s   4GB
Apr 25 12:15:59 Starting compiler/encoders/arm8/proofs
Apr 25 12:22:55 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Apr 25 12:22:55 Starting compiler/encoders/arm8_asl/proofs
Apr 25 12:38:22 Finished compiler/encoders/arm8_asl/proofs                    15m26s   2GB
Apr 25 12:38:22 Starting compiler/encoders/mips/proofs
Apr 25 12:48:29 Finished compiler/encoders/mips/proofs                        10m06s   1GB
Apr 25 12:48:29 Starting compiler/encoders/riscv/proofs
Apr 25 12:57:18 Finished compiler/encoders/riscv/proofs                        8m48s   1GB
Apr 25 12:57:18 Starting compiler/encoders/ag32/proofs
Apr 25 12:59:56 Finished compiler/encoders/ag32/proofs                         2m37s 753MB
Apr 25 12:59:56 Starting compiler/backend/x64/proofs
Apr 25 13:00:25 Finished compiler/backend/x64/proofs                             28s   1GB
Apr 25 13:00:25 Starting compiler/backend/arm7/proofs
Apr 25 13:00:55 Finished compiler/backend/arm7/proofs                            29s   1GB
Apr 25 13:00:55 Starting compiler/backend/arm8/proofs
Apr 25 13:01:25 Finished compiler/backend/arm8/proofs                            29s   1GB
Apr 25 13:01:25 Starting compiler/backend/arm8_asl
Apr 25 13:01:48 Finished compiler/backend/arm8_asl                               23s   1GB
Apr 25 13:01:48 Starting compiler/backend/mips/proofs
Apr 25 13:02:18 Finished compiler/backend/mips/proofs                            30s   1GB
Apr 25 13:02:18 Starting compiler/backend/riscv/proofs
Apr 25 13:02:48 Finished compiler/backend/riscv/proofs                           29s   1GB
Apr 25 13:02:48 Starting compiler/backend/ag32/proofs
Apr 25 13:16:44 Finished compiler/backend/ag32/proofs                         13m55s   2GB
Apr 25 13:16:44 Starting compiler/proofs
Apr 25 13:18:56 Finished compiler/proofs                                       2m12s   3GB
Apr 25 13:18:56 Starting candle/set-theory
Apr 25 13:19:31 Finished candle/set-theory                                       34s   1GB
Apr 25 13:19:31 Starting candle/syntax-lib
Apr 25 13:19:44 Finished candle/syntax-lib                                       13s 694MB
Apr 25 13:19:44 Starting candle/standard/syntax
Apr 25 13:21:46 Finished candle/standard/syntax                                2m01s   1GB
Apr 25 13:21:46 Starting candle/standard/semantics
Apr 25 13:23:36 Finished candle/standard/semantics                             1m49s 911MB
Apr 25 13:23:36 Starting candle/standard/monadic
Apr 25 13:25:32 Finished candle/standard/monadic                               1m56s   1GB
Apr 25 13:25:33 Starting candle/standard/ml_kernel
Apr 25 13:32:07 Finished candle/standard/ml_kernel                             6m34s   4GB
Apr 25 13:32:07 Starting candle/overloading/syntax
Apr 25 13:35:20 Finished candle/overloading/syntax                             3m12s   1GB
Apr 25 13:35:20 Starting candle/overloading/semantics
Apr 25 13:47:11 Finished candle/overloading/semantics                         11m51s   2GB
Apr 25 13:47:11 Starting candle/overloading/monadic
Apr 25 13:49:47 Finished candle/overloading/monadic                            2m35s   1GB
Apr 25 13:49:47 Starting candle/overloading/ml_kernel
Apr 25 13:57:01 Finished candle/overloading/ml_kernel                          7m13s   5GB
Apr 25 13:57:01 Starting candle/overloading/ml_checker
Apr 25 13:59:31 Finished candle/overloading/ml_checker                         2m29s   3GB
Apr 25 13:59:31 Starting candle/prover
Apr 25 14:00:11 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)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[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/standard/ml_kernel/lisp[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 36 directories
Starting work on README.md
Starting work on ast_extrasTheory
README.md                                                                                                                                                                         (0s)     OK
ast_extrasTheory                                                                                                                                                                 (11s)     OK
Starting work on permsTheory
permsTheory                                                                                                                                                                      (23s)FAIL<1>
 | Rerr (Rabort err) => T
 
 failed.
 Failed to prove theorem do_app_perms.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 491) (THEN1 on line 495) (THEN1 on line 499) (THEN1 on line 503) (THEN1 on line 508) (THEN1 on line 512) (THEN1 on line 517) (THEN1 on line 521) (THEN1 on line 525) (THEN1 on line 530) (THEN1 on line 535) (THEN1 on line 540)
 error in quse /home/cug/hk324/cml-regression/cakeml-1873/candle/prover/permsScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 491) (THEN1 on line 495) (THEN1 on line 499) (THEN1 on line 503) (THEN1 on line 508) (THEN1 on line 512) (THEN1 on line 517) (THEN1 on line 521) (THEN1 on line 525) (THEN1 on line 530) (THEN1 on line 535) (THEN1 on line 540)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-1873/candle/prover/permsScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 491) (THEN1 on line 495) (THEN1 on line 499) (THEN1 on line 503) (THEN1 on line 508) (THEN1 on line 512) (THEN1 on line 517) (THEN1 on line 521) (THEN1 on line 525) (THEN1 on line 530) (THEN1 on line 535) (THEN1 on line 540)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 491) (THEN1 on line 495) (THEN1 on line 499) (THEN1 on line 503) (THEN1 on line 508) (THEN1 on line 512) (THEN1 on line 517) (THEN1 on line 521) (THEN1 on line 525) (THEN1 on line 530) (THEN1 on line 535) (THEN1 on line 540)", origin_function = "THEN1", origin_structure = "Tactical"}