Job 1880

CakeML:cb39c39f29bab8b1614ca13bd1ed7f7aa9affcfc
  Merge branch 'mlmap-additions' into Iced_cake [Apr 29 05:36:36]
#865 (Iced_cake)
Merging into:c2be5d64270ec1538eded2eed51612b7708c5d50
  Merge pull request #872 from talsewell/printing-type-check-each-dec [Apr 26 09:47:56]
HOL:a161807cb4e0ea25b8781f3307a590b78703da6f
  Fix some overlong lines [Apr 20 03:46:17]
Machine:oven3

Apr 29 05:38:10 Claimed job
Apr 29 05:38:18 Reusing HOL
Apr 29 05:39:11 Starting developers
Apr 29 05:39:21 Finished developers                                              10s 121MB
Apr 29 05:39:21 Starting developers/bin
Apr 29 05:40:13 Finished developers/bin                                          51s   1GB
Apr 29 05:40:13 Starting semantics/ffi
Apr 29 05:40:38 Finished semantics/ffi                                           24s 228MB
Apr 29 05:40:38 Starting semantics
Apr 29 05:45:36 Finished semantics                                             4m57s   1GB
Apr 29 05:45:36 Starting semantics/proofs
Apr 29 06:00:56 Finished semantics/proofs                                     15m20s   1GB
Apr 29 06:00:56 Starting semantics/alt_semantics
Apr 29 06:02:00 Finished semantics/alt_semantics                               1m03s 532MB
Apr 29 06:02:00 Starting semantics/alt_semantics/proofs
Apr 29 06:27:28 Finished semantics/alt_semantics/proofs                       25m27s   1GB
Apr 29 06:27:28 Starting basis/pure
Apr 29 06:29:46 Finished basis/pure                                            2m17s 883MB
Apr 29 06:29:46 Starting translator
Apr 29 06:37:39 Finished translator                                            7m52s   1GB
Apr 29 06:37:39 Starting compiler/parsing
Apr 29 06:40:26 Finished compiler/parsing                                      2m46s   3GB
Apr 29 06:40:27 Starting characteristic
Apr 29 06:55:03 Finished characteristic                                       14m35s   3GB
Apr 29 06:55:03 Starting translator/monadic
Apr 29 06:59:11 Finished translator/monadic                                    4m08s   1GB
Apr 29 06:59:11 Starting basis
Apr 29 08:52:39 Finished basis                                              1h53m27s  14GB
Apr 29 08:52:39 Starting compiler/inference
Apr 29 08:56:09 Finished compiler/inference                                    3m29s   1GB
Apr 29 08:56:10 Starting compiler/backend/reg_alloc
Apr 29 08:59:22 Finished compiler/backend/reg_alloc                            3m11s   1GB
Apr 29 08:59:22 Starting compiler/backend/gc
Apr 29 09:07:55 Finished compiler/backend/gc                                   8m32s   1GB
Apr 29 09:07:55 Starting compiler/backend
Apr 29 09:19:04 Finished compiler/backend                                     11m08s   2GB
Apr 29 09:19:04 Starting compiler/encoders/asm
Apr 29 09:20:10 Finished compiler/encoders/asm                                 1m05s 744MB
Apr 29 09:20:10 Starting compiler/encoders/x64
Apr 29 09:22:42 Finished compiler/encoders/x64                                 2m32s 671MB
Apr 29 09:22:43 Starting compiler/encoders/arm7
Apr 29 09:27:26 Finished compiler/encoders/arm7                                4m42s   1GB
Apr 29 09:27:26 Starting compiler/encoders/arm8
Apr 29 09:28:59 Finished compiler/encoders/arm8                                1m32s   1GB
Apr 29 09:28:59 Starting compiler/encoders/arm8_asl
Apr 29 13:38:09 Finished compiler/encoders/arm8_asl                         4h09m10s  39GB
Apr 29 13:38:10 Starting compiler/encoders/mips
Apr 29 13:41:35 Finished compiler/encoders/mips                                3m25s   1GB
Apr 29 13:41:36 Starting compiler/encoders/riscv
Apr 29 13:45:26 Finished compiler/encoders/riscv                               3m50s 789MB
Apr 29 13:45:26 Starting compiler/encoders/ag32
Apr 29 13:46:16 Finished compiler/encoders/ag32                                  49s 887MB
Apr 29 13:46:16 Starting compiler/backend/x64
Apr 29 13:47:02 Finished compiler/backend/x64                                    46s   1GB
Apr 29 13:47:02 Starting compiler/backend/arm7
Apr 29 13:47:57 Finished compiler/backend/arm7                                   54s   1GB
Apr 29 13:47:57 Starting compiler/backend/arm8
Apr 29 13:48:45 Finished compiler/backend/arm8                                   47s   1GB
Apr 29 13:48:45 Starting compiler/backend/mips
Apr 29 13:49:34 Finished compiler/backend/mips                                   48s   1GB
Apr 29 13:49:34 Starting compiler/backend/riscv
Apr 29 13:50:23 Finished compiler/backend/riscv                                  48s   1GB
Apr 29 13:50:23 Starting compiler/backend/ag32
Apr 29 13:53:21 Finished compiler/backend/ag32                                 2m57s   1GB
Apr 29 13:53:21 Starting compiler/parsing/proofs
Apr 29 14:01:50 Finished compiler/parsing/proofs                               8m29s   1GB
Apr 29 14:01:51 Starting compiler/inference/proofs
Apr 29 14:07:55 Finished compiler/inference/proofs                             6m04s   1GB
Apr 29 14:07:55 Starting compiler/backend/semantics
Apr 29 15:19:48 Finished compiler/backend/semantics                         1h11m52s   2GB
Apr 29 15:19:49 Starting compiler/backend/reg_alloc/proofs
Apr 29 15:27:50 Finished compiler/backend/reg_alloc/proofs                     8m01s 847MB
Apr 29 15:27:51 Starting compiler/backend/proofs
Apr 29 17:16:01 Finished compiler/backend/proofs                            1h48m10s  18GB
Apr 29 17:16:01 Starting compiler/backend/serialiser
Apr 29 17:19:25 Finished compiler/backend/serialiser                           3m23s   2GB
Apr 29 17:19:25 Starting compiler/encoders/x64/proofs
Apr 29 17:40:46 Finished compiler/encoders/x64/proofs                         21m20s   5GB
Apr 29 17:40:47 Starting compiler/encoders/arm7/proofs
Apr 29 18:10:20 Finished compiler/encoders/arm7/proofs                        29m33s   4GB
Apr 29 18:10:21 Starting compiler/encoders/arm8/proofs
Apr 29 18:25:38 Finished compiler/encoders/arm8/proofs                        15m17s   1GB
Apr 29 18:25:38 Starting compiler/encoders/arm8_asl/proofs
Apr 29 20:18:00 Finished compiler/encoders/arm8_asl/proofs                  1h52m21s   5GB
Apr 29 20:18:01 Starting compiler/encoders/mips/proofs
Apr 29 20:40:44 Finished compiler/encoders/mips/proofs                        22m42s   2GB
Apr 29 20:40:44 Starting compiler/encoders/riscv/proofs
Apr 29 21:00:46 Finished compiler/encoders/riscv/proofs                       20m01s   1GB
Apr 29 21:00:46 Starting compiler/encoders/ag32/proofs
Apr 29 21:06:27 Finished compiler/encoders/ag32/proofs                         5m41s 892MB
Apr 29 21:06:27 Starting compiler/backend/x64/proofs
Apr 29 21:07:29 Finished compiler/backend/x64/proofs                           1m01s   1GB
Apr 29 21:07:30 Starting compiler/backend/arm7/proofs
Apr 29 21:08:31 Finished compiler/backend/arm7/proofs                          1m01s   1GB
Apr 29 21:08:32 Starting compiler/backend/arm8/proofs
Apr 29 21:09:35 Finished compiler/backend/arm8/proofs                          1m02s   1GB
Apr 29 21:09:35 Starting compiler/backend/arm8_asl
Apr 29 21:10:40 Finished compiler/backend/arm8_asl                             1m04s   1GB
Apr 29 21:10:40 Starting compiler/backend/mips/proofs
Apr 29 21:11:42 Finished compiler/backend/mips/proofs                          1m02s   1GB
Apr 29 21:11:43 Starting compiler/backend/riscv/proofs
Apr 29 21:12:44 Finished compiler/backend/riscv/proofs                         1m01s   1GB
Apr 29 21:12:44 Starting compiler/backend/ag32/proofs
Apr 29 21:43:32 Finished compiler/backend/ag32/proofs                         30m47s   2GB
Apr 29 21:43:33 Starting compiler/proofs
Apr 29 21:48:42 Finished compiler/proofs                                       5m09s   2GB
Apr 29 21:48:43 Starting candle/set-theory
Apr 29 21:49:54 Finished candle/set-theory                                     1m11s 978MB
Apr 29 21:49:54 Starting candle/syntax-lib
Apr 29 21:50:24 Finished candle/syntax-lib                                       29s 652MB
Apr 29 21:50:24 Starting candle/standard/syntax
Apr 29 21:54:48 Finished candle/standard/syntax                                4m23s   1GB
Apr 29 21:54:48 Starting candle/standard/semantics
Apr 29 21:58:56 Finished candle/standard/semantics                             4m07s   1GB
Apr 29 21:58:56 Starting candle/standard/monadic
Apr 29 22:02:56 Finished candle/standard/monadic                               3m59s   1GB
Apr 29 22:02:56 Starting candle/standard/ml_kernel
Apr 29 22:16:43 Finished candle/standard/ml_kernel                            13m46s   3GB
Apr 29 22:16:43 Starting candle/overloading/syntax
Apr 29 22:23:35 Finished candle/overloading/syntax                             6m51s   1GB
Apr 29 22:23:36 Starting candle/overloading/semantics
Apr 29 22:49:27 Finished candle/overloading/semantics                         25m51s   3GB
Apr 29 22:49:27 Starting candle/overloading/monadic
Apr 29 22:55:01 Finished candle/overloading/monadic                            5m33s   2GB
Apr 29 22:55:02 Starting candle/overloading/ml_kernel
Apr 29 23:10:26 Finished candle/overloading/ml_kernel                         15m23s   4GB
Apr 29 23:10:26 Starting candle/overloading/ml_checker
Apr 29 23:15:47 Finished candle/overloading/ml_checker                         5m21s   3GB
Apr 29 23:15:47 Starting candle/prover
Apr 29 23:33:04 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                                                                                                                                                                                     (25s)     OK
Starting work on permsTheory
permsTheory                                                                                                                                                                                         (212s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                                                                                                                                                            (222s)     OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_prover_invTheory                                                                                                                                                                              (55s)     OK
candle_kernel_permsTheory                                                                                                                                                                           (303s)     OK
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                                                                                                                                                            (170s)     OK
Starting work on candle_prover_evaluateTheory
candle_prover_evaluateTheory                                                                                                                                                                         (70s)FAIL<1>
   (loc r. loc  kernel_locs  LLOOKUP refs1 loc = SOME r  ref_ok ctxt r) 
   EVERY ok_event ffi1.io_events 
   case list_result res of
     Rval vs => EVERY (v_ok ctxt) vs
   | Rerr (Rraise v) => v_ok ctxt v
   | Rerr (Rabort v8) => T
 
 failed.
 Failed to prove theorem do_app_ok.
 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"}