Job 1775

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:102ad026c83257cfe0dcaf7fd11bede5a8c034b9
  Change indentation after a :: (cons) to be 2 spaces instead of 4 [Feb 14 03:48:56]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 16 20:17:18 Claimed job
Feb 16 20:17:25 Building HOL
Feb 16 20:26:15 Starting developers
Feb 16 20:26:16 Finished developers                                               0s  36MB
Feb 16 20:26:16 Starting developers/bin
Feb 16 20:26:21 Finished developers/bin                                           5s 675MB
Feb 16 20:26:21 Starting semantics/ffi
Feb 16 20:26:30 Finished semantics/ffi                                            9s 258MB
Feb 16 20:26:30 Starting semantics
Feb 16 20:28:19 Finished semantics                                             1m48s   1GB
Feb 16 20:28:19 Starting semantics/proofs
Feb 16 20:31:50 Finished semantics/proofs                                      3m30s   2GB
Feb 16 20:31:50 Starting semantics/alt_semantics
Feb 16 20:32:03 Finished semantics/alt_semantics                                 12s 515MB
Feb 16 20:32:03 Starting semantics/alt_semantics/proofs
Feb 16 20:34:25 Finished semantics/alt_semantics/proofs                        2m21s   1GB
Feb 16 20:34:26 Starting basis/pure
Feb 16 20:37:24 Finished basis/pure                                            2m57s   1GB
Feb 16 20:37:24 Starting translator
Feb 16 20:40:07 Finished translator                                            2m42s   2GB
Feb 16 20:40:07 Starting compiler/parsing
Feb 16 20:41:23 Finished compiler/parsing                                      1m15s   4GB
Feb 16 20:41:23 Starting characteristic
Feb 16 20:47:10 Finished characteristic                                        5m47s   4GB
Feb 16 20:47:10 Starting translator/monadic
Feb 16 20:48:59 Finished translator/monadic                                    1m49s   1GB
Feb 16 20:49:00 Starting basis
Feb 16 21:35:32 Finished basis                                                46m32s  31GB
Feb 16 21:35:33 Starting compiler/inference
Feb 16 21:37:27 Finished compiler/inference                                    1m53s   2GB
Feb 16 21:37:27 Starting compiler/backend/reg_alloc
Feb 16 21:39:17 Finished compiler/backend/reg_alloc                            1m49s   1GB
Feb 16 21:39:17 Starting compiler/backend/gc
Feb 16 21:46:19 Finished compiler/backend/gc                                   7m01s   2GB
Feb 16 21:46:19 Starting compiler/backend
Feb 16 21:56:36 Finished compiler/backend                                     10m16s   3GB
Feb 16 21:56:36 Starting compiler/encoders/asm
Feb 16 21:57:19 Finished compiler/encoders/asm                                   43s   1GB
Feb 16 21:57:19 Starting compiler/encoders/x64
Feb 16 21:59:19 Finished compiler/encoders/x64                                 1m59s   1GB
Feb 16 21:59:19 Starting compiler/encoders/arm7
Feb 16 22:03:34 Finished compiler/encoders/arm7                                4m14s   1GB
Feb 16 22:03:34 Starting compiler/encoders/arm8
Feb 16 22:04:49 Finished compiler/encoders/arm8                                1m14s   1GB
Feb 16 22:04:49 Starting compiler/encoders/arm8_asl
Feb 16 23:28:07 Finished compiler/encoders/arm8_asl                         1h23m17s  24GB
Feb 16 23:28:07 Starting compiler/encoders/mips
Feb 16 23:29:36 Finished compiler/encoders/mips                                1m29s   1GB
Feb 16 23:29:36 Starting compiler/encoders/riscv
Feb 16 23:31:19 Finished compiler/encoders/riscv                               1m42s   1GB
Feb 16 23:31:19 Starting compiler/encoders/ag32
Feb 16 23:31:40 Finished compiler/encoders/ag32                                  20s 884MB
Feb 16 23:31:40 Starting compiler/backend/x64
Feb 16 23:32:02 Finished compiler/backend/x64                                    21s   1GB
Feb 16 23:32:03 Starting compiler/backend/arm7
Feb 16 23:32:27 Finished compiler/backend/arm7                                   24s   1GB
Feb 16 23:32:27 Starting compiler/backend/arm8
Feb 16 23:32:50 Finished compiler/backend/arm8                                   22s   1GB
Feb 16 23:32:50 Starting compiler/backend/mips
Feb 16 23:33:12 Finished compiler/backend/mips                                   22s   1GB
Feb 16 23:33:13 Starting compiler/backend/riscv
Feb 16 23:33:36 Finished compiler/backend/riscv                                  23s   1GB
Feb 16 23:33:36 Starting compiler/backend/ag32
Feb 16 23:34:46 Finished compiler/backend/ag32                                 1m09s   1GB
Feb 16 23:34:46 Starting compiler/parsing/proofs
Feb 16 23:37:27 Finished compiler/parsing/proofs                               2m40s   1GB
Feb 16 23:37:27 Starting compiler/inference/proofs
Feb 16 23:39:49 Finished compiler/inference/proofs                             2m21s   1GB
Feb 16 23:39:49 Starting compiler/backend/semantics
Feb 17 00:08:02 Finished compiler/backend/semantics                           28m11s   5GB
Feb 17 00:08:02 Starting compiler/backend/reg_alloc/proofs
Feb 17 00:13:29 Finished compiler/backend/reg_alloc/proofs                     5m27s   1GB
Feb 17 00:13:29 Starting compiler/backend/proofs
Feb 17 01:49:41 Finished compiler/backend/proofs                            1h36m08s  19GB
Feb 17 01:49:41 Starting compiler/backend/serialiser
Feb 17 01:51:12 Finished compiler/backend/serialiser                           1m31s   2GB
Feb 17 01:51:13 Starting compiler/encoders/x64/proofs
Feb 17 02:00:58 Finished compiler/encoders/x64/proofs                          9m45s   8GB
Feb 17 02:00:58 Starting compiler/encoders/arm7/proofs
Feb 17 02:14:18 Finished compiler/encoders/arm7/proofs                        13m19s   7GB
Feb 17 02:14:18 Starting compiler/encoders/arm8/proofs
Feb 17 02:21:20 Finished compiler/encoders/arm8/proofs                         7m02s   3GB
Feb 17 02:21:21 Starting compiler/encoders/arm8_asl/proofs
Feb 17 03:12:14 Finished compiler/encoders/arm8_asl/proofs                    50m52s   9GB
Feb 17 03:12:14 Starting compiler/encoders/mips/proofs
Feb 17 03:22:06 Finished compiler/encoders/mips/proofs                         9m52s   5GB
Feb 17 03:22:06 Starting compiler/encoders/riscv/proofs
Feb 17 03:30:43 Finished compiler/encoders/riscv/proofs                        8m36s   3GB
Feb 17 03:30:43 Starting compiler/encoders/ag32/proofs
Feb 17 03:33:04 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Feb 17 03:33:04 Starting compiler/backend/x64/proofs
Feb 17 03:33:32 Finished compiler/backend/x64/proofs                             27s   2GB
Feb 17 03:33:32 Starting compiler/backend/arm7/proofs
Feb 17 03:34:00 Finished compiler/backend/arm7/proofs                            27s   1GB
Feb 17 03:34:00 Starting compiler/backend/arm8/proofs
Feb 17 03:34:28 Finished compiler/backend/arm8/proofs                            27s   2GB
Feb 17 03:34:28 Starting compiler/backend/arm8_asl
Feb 17 03:34:49 Finished compiler/backend/arm8_asl                               20s   1GB
Feb 17 03:34:49 Starting compiler/backend/mips/proofs
Feb 17 03:35:16 Finished compiler/backend/mips/proofs                            26s   1GB
Feb 17 03:35:16 Starting compiler/backend/riscv/proofs
Feb 17 03:35:45 Finished compiler/backend/riscv/proofs                           28s   2GB
Feb 17 03:35:45 Starting compiler/backend/ag32/proofs
Feb 17 03:47:35 Finished compiler/backend/ag32/proofs                         11m49s   4GB
Feb 17 03:47:35 Starting compiler/proofs
Feb 17 03:49:46 Finished compiler/proofs                                       2m10s   6GB
Feb 17 03:49:46 Starting candle/set-theory
Feb 17 03:50:16 Finished candle/set-theory                                       30s   1GB
Feb 17 03:50:16 Starting candle/syntax-lib
Feb 17 03:50:29 Finished candle/syntax-lib                                       12s 757MB
Feb 17 03:50:29 Starting candle/standard/syntax
Feb 17 03:52:20 Finished candle/standard/syntax                                1m51s   1GB
Feb 17 03:52:21 Starting candle/standard/semantics
Feb 17 03:54:10 Finished candle/standard/semantics                             1m49s   1GB
Feb 17 03:54:10 Starting candle/standard/monadic
Feb 17 03:55:47 Finished candle/standard/monadic                               1m36s   1GB
Feb 17 03:55:47 Starting candle/standard/ml_kernel
Feb 17 04:02:11 Finished candle/standard/ml_kernel                             6m23s   4GB
Feb 17 04:02:11 Starting candle/overloading/syntax
Feb 17 04:05:20 Finished candle/overloading/syntax                             3m07s   2GB
Feb 17 04:05:20 Starting candle/overloading/semantics
Feb 17 04:16:03 Finished candle/overloading/semantics                         10m43s   5GB
Feb 17 04:16:03 Starting candle/overloading/monadic
Feb 17 04:18:11 Finished candle/overloading/monadic                            2m07s   2GB
Feb 17 04:18:11 Starting candle/overloading/ml_kernel
Feb 17 04:25:25 Finished candle/overloading/ml_kernel                          7m14s   5GB
Feb 17 04:25:25 Starting candle/overloading/ml_checker
Feb 17 04:27:45 Finished candle/overloading/ml_checker                         2m19s   5GB
Feb 17 04:27:45 Starting candle/prover
Feb 17 04:32:27 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 ast_extrasTheory
ast_extrasTheory                          (11s)     OK
Starting work on permsTheory
permsTheory                               (32s)     OK
Starting work on candle_kernel_valsTheory
candle_kernel_valsTheory                  (88s)     OK
Starting work on candle_kernel_permsTheory
Starting work on candle_prover_invTheory
candle_prover_invTheory                   (25s)     OK
candle_kernel_permsTheory                (109s)     OK
Starting work on candle_kernel_funsTheory
candle_kernel_funsTheory                  (28s)FAIL<1>
   v. res = Rerr (Rraise v)  v_ok ctxt' v
 
 failed.
 Failed to prove theorem inferred_ok.
 
 Exception raised at Tactical.FIRST_ASSUM:
  (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)
 error in quse /home/myreen/regression/cakeml-1775/candle/prover/candle_kernel_funsScript.sml : 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"}
 error in load /home/myreen/regression/cakeml-1775/candle/prover/candle_kernel_funsScript : 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"}
 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"}