Job 1882

CakeML:cb39c39f29bab8b1614ca13bd1ed7f7aa9affcfc
  Merge branch 'mlmap-additions' into Iced_cake [Apr 29 05:36:36]
#865 (Iced_cake)
Merging into:e6f5d9527fc76a309309e3ddca8157880dcbcc87
  Merge pull request #881 from CakeML/mlmap-additions [Apr 30 15:11:09]
HOL:9ef7738eaecdb725492f0929f6b270d1f4e63a40
  Teach Holmake and Parse.sml about the tmux terminal [Apr 28 21:56:05]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 30 15:13:18 Claimed job
Apr 30 15:13:23 Building HOL
Apr 30 15:23:01 Starting developers
Apr 30 15:23:01 Finished developers                                               0s  36MB
Apr 30 15:23:01 Starting developers/bin
Apr 30 15:23:08 Finished developers/bin                                           6s   1GB
Apr 30 15:23:08 Starting semantics/ffi
Apr 30 15:23:18 Finished semantics/ffi                                            9s 304MB
Apr 30 15:23:18 Starting semantics
Apr 30 15:25:55 Finished semantics                                             2m36s   1GB
Apr 30 15:25:55 Starting semantics/proofs
Apr 30 15:32:41 Finished semantics/proofs                                      6m45s   1GB
Apr 30 15:32:41 Starting semantics/alt_semantics
Apr 30 15:33:07 Finished semantics/alt_semantics                                 25s 605MB
Apr 30 15:33:07 Starting semantics/alt_semantics/proofs
Apr 30 15:43:52 Finished semantics/alt_semantics/proofs                       10m45s   2GB
Apr 30 15:43:53 Starting basis/pure
Apr 30 15:47:24 Finished basis/pure                                            3m31s   1GB
Apr 30 15:47:24 Starting translator
Apr 30 15:51:05 Finished translator                                            3m40s   2GB
Apr 30 15:51:05 Starting compiler/parsing
Apr 30 15:52:42 Finished compiler/parsing                                      1m36s   6GB
Apr 30 15:52:42 Starting characteristic
Apr 30 15:59:36 Finished characteristic                                        6m54s   3GB
Apr 30 15:59:36 Starting translator/monadic
Apr 30 16:01:38 Finished translator/monadic                                    2m01s   2GB
Apr 30 16:01:38 Starting basis
Apr 30 16:52:40 Finished basis                                                51m01s  28GB
Apr 30 16:52:40 Starting compiler/inference
Apr 30 16:54:15 Finished compiler/inference                                    1m34s   2GB
Apr 30 16:54:15 Starting compiler/backend/reg_alloc
Apr 30 16:56:00 Finished compiler/backend/reg_alloc                            1m44s   2GB
Apr 30 16:56:00 Starting compiler/backend/gc
Apr 30 17:00:30 Finished compiler/backend/gc                                   4m29s   3GB
Apr 30 17:00:30 Starting compiler/backend
Apr 30 17:06:35 Finished compiler/backend                                      6m05s   3GB
Apr 30 17:06:35 Starting compiler/encoders/asm
Apr 30 17:07:07 Finished compiler/encoders/asm                                   31s   1GB
Apr 30 17:07:07 Starting compiler/encoders/x64
Apr 30 17:08:17 Finished compiler/encoders/x64                                 1m09s   1GB
Apr 30 17:08:17 Starting compiler/encoders/arm7
Apr 30 17:10:29 Finished compiler/encoders/arm7                                2m11s   1GB
Apr 30 17:10:29 Starting compiler/encoders/arm8
Apr 30 17:11:14 Finished compiler/encoders/arm8                                  44s   1GB
Apr 30 17:11:14 Starting compiler/encoders/arm8_asl
Apr 30 19:16:48 Finished compiler/encoders/arm8_asl                         2h05m32s  41GB
Apr 30 19:16:48 Starting compiler/encoders/mips
Apr 30 19:18:21 Finished compiler/encoders/mips                                1m32s   1GB
Apr 30 19:18:21 Starting compiler/encoders/riscv
Apr 30 19:20:06 Finished compiler/encoders/riscv                               1m45s   1GB
Apr 30 19:20:06 Starting compiler/encoders/ag32
Apr 30 19:20:29 Finished compiler/encoders/ag32                                  22s   1GB
Apr 30 19:20:29 Starting compiler/backend/x64
Apr 30 19:20:52 Finished compiler/backend/x64                                    23s   1GB
Apr 30 19:20:53 Starting compiler/backend/arm7
Apr 30 19:21:15 Finished compiler/backend/arm7                                   22s   1GB
Apr 30 19:21:16 Starting compiler/backend/arm8
Apr 30 19:21:38 Finished compiler/backend/arm8                                   22s   1GB
Apr 30 19:21:38 Starting compiler/backend/mips
Apr 30 19:22:02 Finished compiler/backend/mips                                   24s   1GB
Apr 30 19:22:03 Starting compiler/backend/riscv
Apr 30 19:22:27 Finished compiler/backend/riscv                                  24s   1GB
Apr 30 19:22:28 Starting compiler/backend/ag32
Apr 30 19:23:51 Finished compiler/backend/ag32                                 1m23s   2GB
Apr 30 19:23:52 Starting compiler/parsing/proofs
Apr 30 19:26:31 Finished compiler/parsing/proofs                               2m39s   1GB
Apr 30 19:26:31 Starting compiler/inference/proofs
Apr 30 19:29:11 Finished compiler/inference/proofs                             2m39s   1GB
Apr 30 19:29:11 Starting compiler/backend/semantics
Apr 30 19:59:23 Finished compiler/backend/semantics                           30m12s   4GB
Apr 30 19:59:23 Starting compiler/backend/reg_alloc/proofs
Apr 30 20:02:43 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
Apr 30 20:02:43 Starting compiler/backend/proofs
Apr 30 20:56:09 Finished compiler/backend/proofs                              53m24s  17GB
Apr 30 20:56:09 Starting compiler/backend/serialiser
Apr 30 20:57:45 Finished compiler/backend/serialiser                           1m35s   2GB
Apr 30 20:57:45 Starting compiler/encoders/x64/proofs
Apr 30 21:07:04 Finished compiler/encoders/x64/proofs                          9m19s  10GB
Apr 30 21:07:04 Starting compiler/encoders/arm7/proofs
Apr 30 21:19:49 Finished compiler/encoders/arm7/proofs                        12m44s   7GB
Apr 30 21:19:49 Starting compiler/encoders/arm8/proofs
Apr 30 21:26:39 Finished compiler/encoders/arm8/proofs                         6m49s   3GB
Apr 30 21:26:39 Starting compiler/encoders/arm8_asl/proofs
Apr 30 22:15:54 Finished compiler/encoders/arm8_asl/proofs                    49m12s   8GB
Apr 30 22:15:54 Starting compiler/encoders/mips/proofs
Apr 30 22:25:44 Finished compiler/encoders/mips/proofs                         9m49s   4GB
Apr 30 22:25:44 Starting compiler/encoders/riscv/proofs
Apr 30 22:34:02 Finished compiler/encoders/riscv/proofs                        8m17s   3GB
Apr 30 22:34:03 Starting compiler/encoders/ag32/proofs
Apr 30 22:36:26 Finished compiler/encoders/ag32/proofs                         2m22s   1GB
Apr 30 22:36:26 Starting compiler/backend/x64/proofs
Apr 30 22:36:55 Finished compiler/backend/x64/proofs                             28s   2GB
Apr 30 22:36:55 Starting compiler/backend/arm7/proofs
Apr 30 22:37:24 Finished compiler/backend/arm7/proofs                            28s   1GB
Apr 30 22:37:24 Starting compiler/backend/arm8/proofs
Apr 30 22:37:51 Finished compiler/backend/arm8/proofs                            27s   1GB
Apr 30 22:37:51 Starting compiler/backend/arm8_asl
Apr 30 22:38:14 Finished compiler/backend/arm8_asl                               22s   2GB
Apr 30 22:38:15 Starting compiler/backend/mips/proofs
Apr 30 22:38:44 Finished compiler/backend/mips/proofs                            29s   1GB
Apr 30 22:38:44 Starting compiler/backend/riscv/proofs
Apr 30 22:39:13 Finished compiler/backend/riscv/proofs                           28s   2GB
Apr 30 22:39:13 Starting compiler/backend/ag32/proofs
Apr 30 22:51:56 Finished compiler/backend/ag32/proofs                         12m43s   3GB
Apr 30 22:51:57 Starting compiler/proofs
Apr 30 22:54:26 Finished compiler/proofs                                       2m29s   6GB
Apr 30 22:54:27 Starting candle/set-theory
Apr 30 22:55:03 Finished candle/set-theory                                       36s   1GB
Apr 30 22:55:03 Starting candle/syntax-lib
Apr 30 22:55:18 Finished candle/syntax-lib                                       14s 857MB
Apr 30 22:55:18 Starting candle/standard/syntax
Apr 30 22:57:21 Finished candle/standard/syntax                                2m02s   1GB
Apr 30 22:57:21 Starting candle/standard/semantics
Apr 30 22:59:11 Finished candle/standard/semantics                             1m50s   2GB
Apr 30 22:59:11 Starting candle/standard/monadic
Apr 30 23:01:04 Finished candle/standard/monadic                               1m52s   2GB
Apr 30 23:01:05 Starting candle/standard/ml_kernel
Apr 30 23:07:16 Finished candle/standard/ml_kernel                             6m11s   4GB
Apr 30 23:07:16 Starting candle/overloading/syntax
Apr 30 23:10:25 Finished candle/overloading/syntax                             3m08s   1GB
Apr 30 23:10:25 Starting candle/overloading/semantics
Apr 30 23:21:15 Finished candle/overloading/semantics                         10m49s   3GB
Apr 30 23:21:15 Starting candle/overloading/monadic
Apr 30 23:23:41 Finished candle/overloading/monadic                            2m25s   2GB
Apr 30 23:23:42 Starting candle/overloading/ml_kernel
Apr 30 23:30:55 Finished candle/overloading/ml_kernel                          7m13s   6GB
Apr 30 23:30:55 Starting candle/overloading/ml_checker
Apr 30 23:33:18 Finished candle/overloading/ml_checker                         2m22s   5GB
Apr 30 23:33:18 Starting candle/prover
Apr 30 23:40:08 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                                                        (83s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                           (95s)     OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_prover_invTheory                                            (27s)     OK
candle_kernel_permsTheory                                         (119s)     OK
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                           (59s)     OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory                                       (29s)FAIL<1>
   | Rerr (Rabort v8) => T
 
 failed.
 Failed to prove theorem do_app_ok.
 
 Exception raised at Tactic.STRIP_TAC:
  (THEN1 on line 403) (THEN1 on line 417) (THEN1 on line 422) (THEN1 on line 427) (THEN1 on line 433) (THEN1 on line 438) (THEN1 on line 443) (THEN1 on line 448) (THEN1 on line 455) (THEN1 on line 460) (THEN1 on line 466) (THEN1 on line 471) (THEN1 on line 476) (THEN1 on line 484) (THEN1 on line 492) (THEN1 on line 500) (THEN1 on line 505) (THEN1 on line 510) (THEN1 on line 515) (THEN1 on line 523) (THEN1 on line 528) (THEN1 on line 533) (THEN1 on line 546) (THEN1 on line 551) (THEN1 on line 556) (THEN1 on line 561) (THEN1 on line 567) (THEN1 on line 572) (THEN1 on line 578) (THEN1 on line 583) (THEN1 on line 588) (THEN1 on line 594) (THEN1 on line 600) (THEN1 on line 608)
 error in quse /home/myreen/regression/cakeml-1882/candle/prover/candle_prover_evaluateScript.sml : HOL_ERR {message = " (THEN1 on line 403) (THEN1 on line 417) (THEN1 on line 422) (THEN1 on line 427) (THEN1 on line 433) (THEN1 on line 438) (THEN1 on line 443) (THEN1 on line 448) (THEN1 on line 455) (THEN1 on line 460) (THEN1 on line 466) (THEN1 on line 471) (THEN1 on line 476) (THEN1 on line 484) (THEN1 on line 492) (THEN1 on line 500) (THEN1 on line 505) (THEN1 on line 510) (THEN1 on line 515) (THEN1 on line 523) (THEN1 on line 528) (THEN1 on line 533) (THEN1 on line 546) (THEN1 on line 551) (THEN1 on line 556) (THEN1 on line 561) (THEN1 on line 567) (THEN1 on line 572) (THEN1 on line 578) (THEN1 on line 583) (THEN1 on line 588) (THEN1 on line 594) (THEN1 on line 600) (THEN1 on line 608)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
 error in load /home/myreen/regression/cakeml-1882/candle/prover/candle_prover_evaluateScript : HOL_ERR {message = " (THEN1 on line 403) (THEN1 on line 417) (THEN1 on line 422) (THEN1 on line 427) (THEN1 on line 433) (THEN1 on line 438) (THEN1 on line 443) (THEN1 on line 448) (THEN1 on line 455) (THEN1 on line 460) (THEN1 on line 466) (THEN1 on line 471) (THEN1 on line 476) (THEN1 on line 484) (THEN1 on line 492) (THEN1 on line 500) (THEN1 on line 505) (THEN1 on line 510) (THEN1 on line 515) (THEN1 on line 523) (THEN1 on line 528) (THEN1 on line 533) (THEN1 on line 546) (THEN1 on line 551) (THEN1 on line 556) (THEN1 on line 561) (THEN1 on line 567) (THEN1 on line 572) (THEN1 on line 578) (THEN1 on line 583) (THEN1 on line 588) (THEN1 on line 594) (THEN1 on line 600) (THEN1 on line 608)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 403) (THEN1 on line 417) (THEN1 on line 422) (THEN1 on line 427) (THEN1 on line 433) (THEN1 on line 438) (THEN1 on line 443) (THEN1 on line 448) (THEN1 on line 455) (THEN1 on line 460) (THEN1 on line 466) (THEN1 on line 471) (THEN1 on line 476) (THEN1 on line 484) (THEN1 on line 492) (THEN1 on line 500) (THEN1 on line 505) (THEN1 on line 510) (THEN1 on line 515) (THEN1 on line 523) (THEN1 on line 528) (THEN1 on line 533) (THEN1 on line 546) (THEN1 on line 551) (THEN1 on line 556) (THEN1 on line 561) (THEN1 on line 567) (THEN1 on line 572) (THEN1 on line 578) (THEN1 on line 583) (THEN1 on line 588) (THEN1 on line 594) (THEN1 on line 600) (THEN1 on line 608)", origin_function = "STRIP_TAC", origin_structure = "Tactic"}