Job 1773

CakeML:4146d4f6bc5eb66a5be3b17afe4aac5f49f79aab
  Fix word_alloc theorem [Feb 15 08:08:19]
#863 (repl)
Merging into:67b312862a2b9919d20a41b16a6599ef4a7635fe
  Merge pull request #855 from CakeML/minor-reheapification [Feb 14 13:06:51]
HOL:7d8123fd0cb1e8c2b7e3fffb337516da7cb7c9df
  Reinstate sptreeTheory.lrnext_def, which 8247e5e3a465 had deleted [Feb 10 23:16:16]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 16 07:46:25 Claimed job
Feb 16 07:46:30 Reusing HOL
Feb 16 07:47:09 Starting developers
Feb 16 07:47:14 Finished developers                                               4s 118MB
Feb 16 07:47:14 Starting developers/bin
Feb 16 07:47:20 Finished developers/bin                                           5s 670MB
Feb 16 07:47:20 Starting semantics/ffi
Feb 16 07:47:31 Finished semantics/ffi                                           11s 224MB
Feb 16 07:47:31 Starting semantics
Feb 16 07:49:23 Finished semantics                                             1m51s 861MB
Feb 16 07:49:24 Starting semantics/proofs
Feb 16 07:53:29 Finished semantics/proofs                                      4m05s   1GB
Feb 16 07:53:29 Starting semantics/alt_semantics
Feb 16 07:53:45 Finished semantics/alt_semantics                                 15s 357MB
Feb 16 07:53:45 Starting semantics/alt_semantics/proofs
Feb 16 07:56:33 Finished semantics/alt_semantics/proofs                        2m47s   1GB
Feb 16 07:56:33 Starting basis/pure
Feb 16 07:57:38 Finished basis/pure                                            1m04s 751MB
Feb 16 07:57:38 Starting translator
Feb 16 08:00:52 Finished translator                                            3m13s   1GB
Feb 16 08:00:52 Starting compiler/parsing
Feb 16 08:02:26 Finished compiler/parsing                                      1m34s   2GB
Feb 16 08:02:26 Starting characteristic
Feb 16 08:09:02 Finished characteristic                                        6m35s   1GB
Feb 16 08:09:02 Starting translator/monadic
Feb 16 08:11:00 Finished translator/monadic                                    1m57s   1GB
Feb 16 08:11:00 Starting basis
Feb 16 09:04:27 Finished basis                                                53m23s  22GB
Feb 16 09:04:27 Starting compiler/inference
Feb 16 09:05:42 Finished compiler/inference                                    1m14s   1GB
Feb 16 09:05:42 Starting compiler/backend/reg_alloc
Feb 16 09:06:53 Finished compiler/backend/reg_alloc                            1m11s   1GB
Feb 16 09:06:54 Starting compiler/backend/gc
Feb 16 09:10:53 Finished compiler/backend/gc                                   3m59s   1GB
Feb 16 09:10:53 Starting compiler/backend
Feb 16 09:17:04 Finished compiler/backend                                      6m10s   2GB
Feb 16 09:17:04 Starting compiler/encoders/asm
Feb 16 09:17:31 Finished compiler/encoders/asm                                   26s 677MB
Feb 16 09:17:31 Starting compiler/encoders/x64
Feb 16 09:18:01 Finished compiler/encoders/x64                                   29s 964MB
Feb 16 09:18:01 Starting compiler/encoders/arm7
Feb 16 09:19:02 Finished compiler/encoders/arm7                                1m00s 802MB
Feb 16 09:19:02 Starting compiler/encoders/arm8
Feb 16 09:19:18 Finished compiler/encoders/arm8                                  15s 927MB
Feb 16 09:19:18 Starting compiler/encoders/arm8_asl
Feb 16 09:22:20 Finished compiler/encoders/arm8_asl                            3m02s 988MB
Feb 16 09:22:20 Starting compiler/encoders/mips
Feb 16 09:22:41 Finished compiler/encoders/mips                                  19s   1GB
Feb 16 09:22:41 Starting compiler/encoders/riscv
Feb 16 09:22:58 Finished compiler/encoders/riscv                                 17s 718MB
Feb 16 09:22:58 Starting compiler/encoders/ag32
Feb 16 09:23:20 Finished compiler/encoders/ag32                                  21s 702MB
Feb 16 09:23:20 Starting compiler/backend/x64
Feb 16 09:23:43 Finished compiler/backend/x64                                    22s   1GB
Feb 16 09:23:43 Starting compiler/backend/arm7
Feb 16 09:24:08 Finished compiler/backend/arm7                                   24s   1GB
Feb 16 09:24:08 Starting compiler/backend/arm8
Feb 16 09:24:32 Finished compiler/backend/arm8                                   23s   1GB
Feb 16 09:24:32 Starting compiler/backend/mips
Feb 16 09:24:55 Finished compiler/backend/mips                                   22s   1GB
Feb 16 09:24:55 Starting compiler/backend/riscv
Feb 16 09:25:20 Finished compiler/backend/riscv                                  24s   1GB
Feb 16 09:25:20 Starting compiler/backend/ag32
Feb 16 09:26:37 Finished compiler/backend/ag32                                 1m16s   1GB
Feb 16 09:26:37 Starting compiler/parsing/proofs
Feb 16 09:30:49 Finished compiler/parsing/proofs                               4m11s   1GB
Feb 16 09:30:49 Starting compiler/inference/proofs
Feb 16 09:33:32 Finished compiler/inference/proofs                             2m42s   1GB
Feb 16 09:33:32 Starting compiler/backend/semantics
Feb 16 10:09:26 Finished compiler/backend/semantics                           35m52s   2GB
Feb 16 10:09:26 Starting compiler/backend/reg_alloc/proofs
Feb 16 10:13:28 Finished compiler/backend/reg_alloc/proofs                     4m02s 774MB
Feb 16 10:13:28 Starting compiler/backend/proofs
Feb 16 11:20:20 Finished compiler/backend/proofs                            1h06m49s  23GB
Feb 16 11:20:20 Starting compiler/backend/serialiser
Feb 16 11:21:58 Finished compiler/backend/serialiser                           1m37s   1GB
Feb 16 11:21:58 Starting compiler/encoders/x64/proofs
Feb 16 11:32:53 Finished compiler/encoders/x64/proofs                         10m54s   4GB
Feb 16 11:32:53 Starting compiler/encoders/arm7/proofs
Feb 16 11:48:14 Finished compiler/encoders/arm7/proofs                        15m20s   3GB
Feb 16 11:48:14 Starting compiler/encoders/arm8/proofs
Feb 16 11:55:55 Finished compiler/encoders/arm8/proofs                         7m40s   1GB
Feb 16 11:55:55 Starting compiler/encoders/arm8_asl/proofs
Feb 16 12:13:30 Finished compiler/encoders/arm8_asl/proofs                    17m35s   1GB
Feb 16 12:13:30 Starting compiler/encoders/mips/proofs
Feb 16 12:24:54 Finished compiler/encoders/mips/proofs                        11m22s   2GB
Feb 16 12:24:54 Starting compiler/encoders/riscv/proofs
Feb 16 12:34:47 Finished compiler/encoders/riscv/proofs                        9m53s   1GB
Feb 16 12:34:47 Starting compiler/encoders/ag32/proofs
Feb 16 12:37:42 Finished compiler/encoders/ag32/proofs                         2m54s 780MB
Feb 16 12:37:42 Starting compiler/backend/x64/proofs
Feb 16 12:38:13 Finished compiler/backend/x64/proofs                             31s   1GB
Feb 16 12:38:14 Starting compiler/backend/arm7/proofs
Feb 16 12:38:44 Finished compiler/backend/arm7/proofs                            29s   1GB
Feb 16 12:38:44 Starting compiler/backend/arm8/proofs
Feb 16 12:39:15 Finished compiler/backend/arm8/proofs                            30s   1GB
Feb 16 12:39:15 Starting compiler/backend/arm8_asl
Feb 16 12:39:39 Finished compiler/backend/arm8_asl                               24s   1GB
Feb 16 12:39:39 Starting compiler/backend/mips/proofs
Feb 16 12:40:11 Finished compiler/backend/mips/proofs                            31s   1GB
Feb 16 12:40:11 Starting compiler/backend/riscv/proofs
Feb 16 12:40:42 Finished compiler/backend/riscv/proofs                           30s   1GB
Feb 16 12:40:42 Starting compiler/backend/ag32/proofs
Feb 16 12:55:18 Finished compiler/backend/ag32/proofs                         14m35s   3GB
Feb 16 12:55:18 Starting compiler/proofs
Feb 16 12:57:29 Finished compiler/proofs                                       2m10s   3GB
Feb 16 12:57:29 Starting candle/set-theory
Feb 16 12:58:02 Finished candle/set-theory                                       32s 747MB
Feb 16 12:58:02 Starting candle/syntax-lib
Feb 16 12:58:15 Finished candle/syntax-lib                                       12s 642MB
Feb 16 12:58:15 Starting candle/standard/syntax
Feb 16 13:00:21 Finished candle/standard/syntax                                2m05s   1GB
Feb 16 13:00:21 Starting candle/standard/semantics
Feb 16 13:02:24 Finished candle/standard/semantics                             2m02s   1GB
Feb 16 13:02:24 Starting candle/standard/monadic
Feb 16 13:04:17 Finished candle/standard/monadic                               1m53s   1GB
Feb 16 13:04:17 Starting candle/standard/ml_kernel
Feb 16 13:12:05 Finished candle/standard/ml_kernel                             7m47s   4GB
Feb 16 13:12:05 Starting candle/overloading/syntax
Feb 16 13:15:44 Finished candle/overloading/syntax                             3m38s 995MB
Feb 16 13:15:44 Starting candle/overloading/semantics
Feb 16 13:28:58 Finished candle/overloading/semantics                         13m11s   2GB
Feb 16 13:28:58 Starting candle/overloading/monadic
Feb 16 13:31:37 Finished candle/overloading/monadic                            2m39s   1GB
Feb 16 13:31:38 Starting candle/overloading/ml_kernel
Feb 16 13:40:09 Finished candle/overloading/ml_kernel                          8m30s   3GB
Feb 16 13:40:09 Starting candle/overloading/ml_checker
Feb 16 13:42:40 Finished candle/overloading/ml_checker                         2m31s   3GB
Feb 16 13:42:41 Starting candle/prover
Feb 16 13:48: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                                                        (37s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                                           (99s)     OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_prover_invTheory                                            (26s)     OK
candle_kernel_permsTheory                                         (121s)     OK
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                                           (48s)FAIL<1>
 (abort. s'.ffi = s.ffi  res = Rerr (Rabort abort)) 
 ctxt'.
   state_ok ctxt' s'  (v. v_ok ctxt v  v_ok ctxt' v) 
   (v. kernel_vals ctxt v  kernel_vals ctxt' v) 
   (vs. res = Rval vs  EVERY (v_ok ctxt') vs) 
   v. res = Rerr (Rraise v)  v_ok ctxt' v
 
 failed.
 Failed to prove theorem inferred_ok.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 521) (THEN1 on line 541) (THEN1 on line 562) (THEN1 on line 582) (THEN1 on line 623) (THEN1 on line 658) (THEN1 on line 672) (THEN1 on line 696) (THEN1 on line 718) (THEN1 on line 730) (THEN1 on line 742) (THEN1 on line 757) (THEN1 on line 781) (THEN1 on line 804) (THEN1 on line 840) (THEN1 on line 858) (THEN1 on line 870) (THEN1 on line 882) (THEN1 on line 894) (THEN1 on line 906) (THEN1 on line 933) (THEN1 on line 977) (THEN1 on line 1007) (THEN1 on line 1037) (THEN1 on line 1059) (THEN1 on line 1085) (THEN1 on line 1107) (THEN1 on line 1129) (THEN1 on line 1149) (THEN1 on line 1169) (THEN1 on line 1182) (THEN1 on line 1204) (THEN1 on line 1226) (THEN1 on line 1248) (THEN1 on line 1269) (THEN1 on line 1285) (THEN1 on line 1304) (THEN1 on line 1333) (THEN1 on line 1352) (THEN1 on line 1372) (THEN1 on line 1396) (THEN1 on line 1420) (THEN1 on line 1485) (THEN1 on line 1511)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}