Job 1416

CakeML:8fc7c581583405794ed78c48a20df2834e0a1747
  Various fixes in response to changes in HOL [Dec 17 14:27:13]
HOL:a4312426afc04b5e4d7aa33a72ef1fb535e4cf6a
  Tidy up Kolmogorov uncomputable script file (deleting much) [Dec 14 06:39:51]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 17 14:27:27 Claimed job
Dec 17 14:27:35 Reusing HOL
Dec 17 14:27:45 Starting developers
Dec 17 14:27:45 Finished developers                                               0s  36MB
Dec 17 14:27:45 Starting developers/bin
Dec 17 14:27:52 Finished developers/bin                                           6s   1GB
Dec 17 14:27:52 Starting semantics/ffi
Dec 17 14:28:03 Finished semantics/ffi                                           10s 290MB
Dec 17 14:28:03 Starting semantics
Dec 17 14:29:29 Finished semantics                                             1m25s   1GB
Dec 17 14:29:29 Starting semantics/proofs
Dec 17 14:32:47 Finished semantics/proofs                                      3m18s   1GB
Dec 17 14:32:48 Starting semantics/alt_semantics
Dec 17 14:32:56 Finished semantics/alt_semantics                                  7s 353MB
Dec 17 14:32:56 Starting semantics/alt_semantics/proofs
Dec 17 14:35:03 Finished semantics/alt_semantics/proofs                        2m06s   1GB
Dec 17 14:35:03 Starting basis/pure
Dec 17 14:37:48 Finished basis/pure                                            2m44s   1GB
Dec 17 14:37:48 Starting translator
Dec 17 14:40:23 Finished translator                                            2m34s   2GB
Dec 17 14:40:23 Starting compiler/parsing
Dec 17 14:41:29 Finished compiler/parsing                                      1m06s   4GB
Dec 17 14:41:29 Starting characteristic
Dec 17 14:47:24 Finished characteristic                                        5m54s   3GB
Dec 17 14:47:24 Starting translator/monadic
Dec 17 14:49:09 Finished translator/monadic                                    1m44s   3GB
Dec 17 14:49:09 Starting basis
Dec 17 15:23:32 Finished basis                                                34m22s  24GB
Dec 17 15:23:33 Starting compiler/inference
Dec 17 15:24:39 Finished compiler/inference                                    1m06s   1GB
Dec 17 15:24:39 Starting compiler/backend/reg_alloc
Dec 17 15:25:43 Finished compiler/backend/reg_alloc                            1m03s   1GB
Dec 17 15:25:43 Starting compiler/backend/gc
Dec 17 15:29:17 Finished compiler/backend/gc                                   3m34s   3GB
Dec 17 15:29:18 Starting compiler/backend
Dec 17 15:34:10 Finished compiler/backend                                      4m52s   5GB
Dec 17 15:34:10 Starting compiler/encoders/asm
Dec 17 15:34:32 Finished compiler/encoders/asm                                   21s   1GB
Dec 17 15:34:33 Starting compiler/encoders/x64
Dec 17 15:35:36 Finished compiler/encoders/x64                                 1m02s   1GB
Dec 17 15:35:36 Starting compiler/encoders/arm7
Dec 17 15:37:37 Finished compiler/encoders/arm7                                2m01s   1GB
Dec 17 15:37:37 Starting compiler/encoders/arm8
Dec 17 15:38:16 Finished compiler/encoders/arm8                                  38s 928MB
Dec 17 15:38:16 Starting compiler/encoders/mips
Dec 17 15:39:40 Finished compiler/encoders/mips                                1m24s   1GB
Dec 17 15:39:40 Starting compiler/encoders/riscv
Dec 17 15:41:15 Finished compiler/encoders/riscv                               1m34s   1GB
Dec 17 15:41:15 Starting compiler/encoders/ag32
Dec 17 15:41:33 Finished compiler/encoders/ag32                                  18s 934MB
Dec 17 15:41:34 Starting compiler/backend/x64
Dec 17 15:41:53 Finished compiler/backend/x64                                    19s   1GB
Dec 17 15:41:53 Starting compiler/backend/arm7
Dec 17 15:42:15 Finished compiler/backend/arm7                                   21s   1GB
Dec 17 15:42:15 Starting compiler/backend/arm8
Dec 17 15:42:35 Finished compiler/backend/arm8                                   20s   1GB
Dec 17 15:42:35 Starting compiler/backend/mips
Dec 17 15:42:57 Finished compiler/backend/mips                                   20s   1GB
Dec 17 15:42:57 Starting compiler/backend/riscv
Dec 17 15:43:17 Finished compiler/backend/riscv                                  19s   1GB
Dec 17 15:43:17 Starting compiler/backend/ag32
Dec 17 15:44:27 Finished compiler/backend/ag32                                 1m09s   1GB
Dec 17 15:44:27 Starting compiler/parsing/proofs
Dec 17 15:49:52 Finished compiler/parsing/proofs                               5m25s   2GB
Dec 17 15:49:53 Starting compiler/inference/proofs
Dec 18 05:49:41 Resuming compiler/inference/proofs
Dec 18 05:49:41 Finished compiler/inference/proofs                                0s  67MB
Dec 18 05:49:41 Starting compiler/backend/semantics
Dec 18 06:16:54 Finished compiler/backend/semantics                           27m12s   4GB
Dec 18 06:16:54 Starting compiler/backend/reg_alloc/proofs
Dec 18 06:20:14 Finished compiler/backend/reg_alloc/proofs                     3m20s   1GB
Dec 18 06:20:14 Starting compiler/backend/proofs
Dec 18 07:14:22 Finished compiler/backend/proofs                              54m07s  30GB
Dec 18 07:14:22 Starting compiler/encoders/x64/proofs
Dec 18 07:23:48 Finished compiler/encoders/x64/proofs                          9m26s   5GB
Dec 18 07:23:49 Starting compiler/encoders/arm7/proofs
Dec 18 07:36:17 Finished compiler/encoders/arm7/proofs                        12m27s  10GB
Dec 18 07:36:17 Starting compiler/encoders/arm8/proofs
Dec 18 07:42:45 Finished compiler/encoders/arm8/proofs                         6m27s   3GB
Dec 18 07:42:45 Starting compiler/encoders/mips/proofs
Dec 18 07:52:33 Finished compiler/encoders/mips/proofs                         9m47s   6GB
Dec 18 07:52:33 Starting compiler/encoders/riscv/proofs
Dec 18 08:00:46 Finished compiler/encoders/riscv/proofs                        8m12s   3GB
Dec 18 08:00:46 Starting compiler/encoders/ag32/proofs
Dec 18 08:03:07 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Dec 18 08:03:08 Starting compiler/backend/x64/proofs
Dec 18 08:03:29 Finished compiler/backend/x64/proofs                             21s   2GB
Dec 18 08:03:29 Starting compiler/backend/arm7/proofs
Dec 18 08:03:52 Finished compiler/backend/arm7/proofs                            22s   1GB
Dec 18 08:03:52 Starting compiler/backend/arm8/proofs
Dec 18 08:04:11 Finished compiler/backend/arm8/proofs                            19s   1GB
Dec 18 08:04:12 Starting compiler/backend/mips/proofs
Dec 18 08:04:33 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 18 08:04:33 Starting compiler/backend/riscv/proofs
Dec 18 08:04:56 Finished compiler/backend/riscv/proofs                           22s   2GB
Dec 18 08:04:56 Starting compiler/backend/ag32/proofs
Dec 18 08:17:01 Finished compiler/backend/ag32/proofs                         12m04s   5GB
Dec 18 08:17:01 Starting compiler/proofs
Dec 18 08:18:54 Finished compiler/proofs                                       1m52s   6GB
Dec 18 08:18:54 Starting candle/set-theory
Dec 18 08:19:23 Finished candle/set-theory                                       28s   1GB
Dec 18 08:19:23 Starting candle/syntax-lib
Dec 18 08:19:34 Finished candle/syntax-lib                                       10s 813MB
Dec 18 08:19:34 Starting candle/standard/syntax
Dec 18 08:21:26 Finished candle/standard/syntax                                1m51s   1GB
Dec 18 08:21:26 Starting candle/standard/semantics
Dec 18 08:23:11 Finished candle/standard/semantics                             1m45s   2GB
Dec 18 08:23:11 Starting candle/standard/monadic
Dec 18 08:24:51 Finished candle/standard/monadic                               1m39s   1GB
Dec 18 08:24:51 Starting candle/standard/ml_kernel
Dec 18 08:30:06 Finished candle/standard/ml_kernel                             5m14s   7GB
Dec 18 08:30:07 Starting candle/overloading/syntax
Dec 18 08:32:53 FAILED: candle/overloading/syntax
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)/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/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Starting work on README.md
Starting work on holSyntaxTheory
Starting work on holSyntaxRenamingTheory
README.md              real:    0s  user:    0s     OK
...yntaxRenamingTheory real:   10s  user:    9s     OK
holSyntaxTheory        real:   26s  user:   25s     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory   real:  108s  user:  104s     OK
Starting work on holBoolSyntaxTheory
Starting work on holSyntaxRenamingTyvarTheory
...RenamingTyvarTheory real:   12s  user:   11s     OK
Starting work on holSyntaxCyclicityTheory
...ntaxCyclicityTheory real:   17s  user:   16sFAIL<1>
   rs. mg_sol_seq rs (TAKE n pqs)  path_starting_at ctxt 0 rs (TAKE n pqs)
 
 failed.
 Failed to prove theorem seq_asc_mg_sol_path.
 
 Exception raised at BasicProvers.by:
 by's tactic failed to prove subgoal on line 1780 (THEN1 on line 1849) (THEN1 on line 1850) (THEN1 on line 1854)
 error in quse /home/myreen/regression/cakeml-1416/candle/overloading/syntax/holSyntaxCyclicityScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 1780 (THEN1 on line 1849) (THEN1 on line 1850) (THEN1 on line 1854)", origin_function = "by", origin_structure = "BasicProvers"}
 error in load /home/myreen/regression/cakeml-1416/candle/overloading/syntax/holSyntaxCyclicityScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 1780 (THEN1 on line 1849) (THEN1 on line 1850) (THEN1 on line 1854)", origin_function = "by", origin_structure = "BasicProvers"}
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 1780 (THEN1 on line 1849) (THEN1 on line 1850) (THEN1 on line 1854)", origin_function = "by", origin_structure = "BasicProvers"}
holBoolSyntaxTheory                            M-KILLED