Job 1664

CakeML:07642b01deb0d98b98741ce007124df3d45cf166
  Adjust to change in gs [Nov 25 10:28:29]
#846 (pattern-aliases)
Merging into:99fb6df32493efb4c9ae4d7f6675e49fc2628b2b
  Merge pull request #842 from CakeML/ramsey [Nov 18 19:39:38]
HOL:5c150bdc68d4b444c3b771ee27080aaa077b3204
  emacs-mode: adjust holmake command to get to use ANSI magic [Nov 23 06:58:28]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Nov 25 10:41:27 Claimed job
Nov 25 10:41:37 Reusing HOL
Nov 25 10:42:15 Starting developers
Nov 25 10:42:19 Finished developers                                               4s 158MB
Nov 25 10:42:19 Starting developers/bin
Nov 25 10:42:26 Finished developers/bin                                           6s   1GB
Nov 25 10:42:26 Starting semantics/ffi
Nov 25 10:42:34 Finished semantics/ffi                                            8s 238MB
Nov 25 10:42:34 Starting semantics
Nov 25 10:43:59 Finished semantics                                             1m24s   1GB
Nov 25 10:43:59 Starting semantics/proofs
Nov 25 10:47:34 Finished semantics/proofs                                      3m35s   1GB
Nov 25 10:47:34 Starting semantics/alt_semantics
Nov 25 10:47:46 Finished semantics/alt_semantics                                 11s 362MB
Nov 25 10:47:46 Starting semantics/alt_semantics/proofs
Nov 25 10:50:14 Finished semantics/alt_semantics/proofs                        2m27s 802MB
Nov 25 10:50:14 Starting basis/pure
Nov 25 10:53:11 Finished basis/pure                                            2m57s 874MB
Nov 25 10:53:12 Starting translator
Nov 25 10:56:07 Finished translator                                            2m55s   1GB
Nov 25 10:56:07 Starting compiler/parsing
Nov 25 10:57:26 Finished compiler/parsing                                      1m18s   2GB
Nov 25 10:57:26 Starting characteristic
Nov 25 11:03:13 Finished characteristic                                        5m47s   1GB
Nov 25 11:03:14 Starting translator/monadic
Nov 25 11:04:57 Finished translator/monadic                                    1m43s   1GB
Nov 25 11:04:57 Starting basis
Nov 25 11:51:17 Finished basis                                                46m18s  17GB
Nov 25 11:51:17 Starting compiler/inference
Nov 25 11:52:33 Finished compiler/inference                                    1m15s   1GB
Nov 25 11:52:33 Starting compiler/backend/reg_alloc
Nov 25 11:53:41 Finished compiler/backend/reg_alloc                            1m08s   1GB
Nov 25 11:53:41 Starting compiler/backend/gc
Nov 25 11:57:05 Finished compiler/backend/gc                                   3m23s   1GB
Nov 25 11:57:05 Starting compiler/backend
Nov 25 12:01:20 Finished compiler/backend                                      4m14s   2GB
Nov 25 12:01:20 Starting compiler/encoders/asm
Nov 25 12:01:43 Finished compiler/encoders/asm                                   23s 731MB
Nov 25 12:01:43 Starting compiler/encoders/x64
Nov 25 12:02:46 Finished compiler/encoders/x64                                 1m02s   1GB
Nov 25 12:02:46 Starting compiler/encoders/arm7
Nov 25 12:04:47 Finished compiler/encoders/arm7                                2m01s   1GB
Nov 25 12:04:48 Starting compiler/encoders/arm8
Nov 25 12:05:25 Finished compiler/encoders/arm8                                  37s 964MB
Nov 25 12:05:25 Starting compiler/encoders/mips
Nov 25 12:06:53 Finished compiler/encoders/mips                                1m27s   1GB
Nov 25 12:06:53 Starting compiler/encoders/riscv
Nov 25 12:08:37 Finished compiler/encoders/riscv                               1m43s   1GB
Nov 25 12:08:37 Starting compiler/encoders/ag32
Nov 25 12:08:56 Finished compiler/encoders/ag32                                  18s 586MB
Nov 25 12:08:56 Starting compiler/backend/x64
Nov 25 12:09:15 Finished compiler/backend/x64                                    18s   1GB
Nov 25 12:09:15 Starting compiler/backend/arm7
Nov 25 12:09:35 Finished compiler/backend/arm7                                   19s   1GB
Nov 25 12:09:35 Starting compiler/backend/arm8
Nov 25 12:09:55 Finished compiler/backend/arm8                                   19s   1GB
Nov 25 12:09:56 Starting compiler/backend/mips
Nov 25 12:10:16 Finished compiler/backend/mips                                   20s   1GB
Nov 25 12:10:16 Starting compiler/backend/riscv
Nov 25 12:10:36 Finished compiler/backend/riscv                                  20s   1GB
Nov 25 12:10:36 Starting compiler/backend/ag32
Nov 25 12:11:44 Finished compiler/backend/ag32                                 1m07s   1GB
Nov 25 12:11:44 Starting compiler/parsing/proofs
Nov 25 12:15:24 Finished compiler/parsing/proofs                               3m39s   1GB
Nov 25 12:15:24 Starting compiler/inference/proofs
Nov 25 12:17:47 Finished compiler/inference/proofs                             2m23s   1GB
Nov 25 12:17:47 Starting compiler/backend/semantics
Nov 25 12:46:03 Finished compiler/backend/semantics                           28m15s   2GB
Nov 25 12:46:03 Starting compiler/backend/reg_alloc/proofs
Nov 25 12:49:30 Finished compiler/backend/reg_alloc/proofs                     3m27s   1GB
Nov 25 12:49:30 Starting compiler/backend/proofs
Nov 25 13:40:16 Finished compiler/backend/proofs                              50m45s  17GB
Nov 25 13:40:17 Starting compiler/backend/serialiser
Nov 25 13:41:30 Finished compiler/backend/serialiser                           1m13s   2GB
Nov 25 13:41:30 Starting compiler/encoders/x64/proofs
Nov 25 13:51:04 Finished compiler/encoders/x64/proofs                          9m33s   4GB
Nov 25 13:51:04 Starting compiler/encoders/arm7/proofs
Nov 25 14:04:04 Finished compiler/encoders/arm7/proofs                        12m59s   3GB
Nov 25 14:04:04 Starting compiler/encoders/arm8/proofs
Nov 25 14:10:47 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Nov 25 14:10:47 Starting compiler/encoders/mips/proofs
Nov 25 14:20:50 Finished compiler/encoders/mips/proofs                        10m03s   2GB
Nov 25 14:20:50 Starting compiler/encoders/riscv/proofs
Nov 25 14:29:35 Finished compiler/encoders/riscv/proofs                        8m44s   1GB
Nov 25 14:29:35 Starting compiler/encoders/ag32/proofs
Nov 25 14:32:09 Finished compiler/encoders/ag32/proofs                         2m34s 705MB
Nov 25 14:32:09 Starting compiler/backend/x64/proofs
Nov 25 14:32:32 Finished compiler/backend/x64/proofs                             22s   1GB
Nov 25 14:32:32 Starting compiler/backend/arm7/proofs
Nov 25 14:32:56 Finished compiler/backend/arm7/proofs                            24s   1GB
Nov 25 14:32:56 Starting compiler/backend/arm8/proofs
Nov 25 14:33:20 Finished compiler/backend/arm8/proofs                            23s   1GB
Nov 25 14:33:21 Starting compiler/backend/mips/proofs
Nov 25 14:33:44 Finished compiler/backend/mips/proofs                            23s   1GB
Nov 25 14:33:44 Starting compiler/backend/riscv/proofs
Nov 25 14:34:07 Finished compiler/backend/riscv/proofs                           22s   1GB
Nov 25 14:34:07 Starting compiler/backend/ag32/proofs
Nov 25 14:46:39 Finished compiler/backend/ag32/proofs                         12m30s   2GB
Nov 25 14:46:39 Starting compiler/proofs
Nov 25 14:48:39 Finished compiler/proofs                                       1m59s   3GB
Nov 25 14:48:39 Starting candle/set-theory
Nov 25 14:49:08 Finished candle/set-theory                                       29s 885MB
Nov 25 14:49:08 Starting candle/syntax-lib
Nov 25 14:49:19 Finished candle/syntax-lib                                       10s 731MB
Nov 25 14:49:19 Starting candle/standard/syntax
Nov 25 14:51:09 Finished candle/standard/syntax                                1m49s 984MB
Nov 25 14:51:09 Starting candle/standard/semantics
Nov 25 14:52:52 Finished candle/standard/semantics                             1m42s   1GB
Nov 25 14:52:53 Starting candle/standard/monadic
Nov 25 14:54:35 Finished candle/standard/monadic                               1m41s   1GB
Nov 25 14:54:35 Starting candle/standard/ml_kernel
Nov 25 14:59:51 Finished candle/standard/ml_kernel                             5m16s   3GB
Nov 25 14:59:51 Starting candle/overloading/syntax
Nov 25 15:02:11 FAILED: candle/overloading/syntax
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/src/bag[0m
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/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[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/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)/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                                                                                                   (0s)     OK
holSyntaxRenamingTheory                                                                                     (7s)     OK
holSyntaxTheory                                                                                            (26s)     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                                                                       (98s)     OK
Starting work on holBoolSyntaxTheory
Starting work on holSyntaxRenamingTyvarTheory
holSyntaxRenamingTyvarTheory                                                                                (9s)FAIL<1>
      LNTH (n + k) ll = LNTH n ll  IS_SOME (LNTH (n + k) ll)  0 < k 
      THE (LNTH (PRE k) ll) = x)
 
 failed.
 First unsolved sub-goal is
 
 x''. f x'' = SOME x''
 
 Failed to prove theorem LUNFOLD_f_iter_inj.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
holBoolSyntaxTheory                                                                                        (10s)MKILLED