Job 1663

CakeML:b906a5a503573461f19efba32a6fd5db8503ea69
  Fix pegCompleteScript for changes to gs [Nov 25 03:28:36]
#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:oven3 4.19.67.1.amd64-smp

Nov 25 06:18:23 Claimed job
Nov 25 06:18:30 Reusing HOL
Nov 25 06:19:21 Starting developers
Nov 25 06:19:29 Finished developers                                               7s 140MB
Nov 25 06:19:29 Starting developers/bin
Nov 25 06:19:41 Finished developers/bin                                          12s   1GB
Nov 25 06:19:41 Starting semantics/ffi
Nov 25 06:20:01 Finished semantics/ffi                                           19s 255MB
Nov 25 06:20:01 Starting semantics
Nov 25 06:22:56 Finished semantics                                             2m54s   1GB
Nov 25 06:22:56 Starting semantics/proofs
Nov 25 06:30:39 Finished semantics/proofs                                      7m43s   1GB
Nov 25 06:30:40 Starting semantics/alt_semantics
Nov 25 06:31:05 Finished semantics/alt_semantics                                 25s 399MB
Nov 25 06:31:06 Starting semantics/alt_semantics/proofs
Nov 25 06:36:25 Finished semantics/alt_semantics/proofs                        5m18s 975MB
Nov 25 06:36:25 Starting basis/pure
Nov 25 06:38:15 Finished basis/pure                                            1m49s   1GB
Nov 25 06:38:15 Starting translator
Nov 25 06:44:08 Finished translator                                            5m52s   1GB
Nov 25 06:44:08 Starting compiler/parsing
Nov 25 06:46:48 Finished compiler/parsing                                      2m40s   3GB
Nov 25 06:46:49 Starting characteristic
Nov 25 06:58:49 Finished characteristic                                       11m58s   2GB
Nov 25 06:58:49 Starting translator/monadic
Nov 25 07:02:22 Finished translator/monadic                                    3m33s   1GB
Nov 25 07:02:22 Starting basis
Nov 25 08:42:22 Finished basis                                              1h39m59s  20GB
Nov 25 08:42:23 Starting compiler/inference
Nov 25 08:44:59 Finished compiler/inference                                    2m35s   1GB
Nov 25 08:44:59 Starting compiler/backend/reg_alloc
Nov 25 08:47:06 Finished compiler/backend/reg_alloc                            2m06s   1GB
Nov 25 08:47:06 Starting compiler/backend/gc
Nov 25 08:53:42 Finished compiler/backend/gc                                   6m35s   1GB
Nov 25 08:53:42 Starting compiler/backend
Nov 25 09:02:01 Finished compiler/backend                                      8m18s   2GB
Nov 25 09:02:01 Starting compiler/encoders/asm
Nov 25 09:02:52 Finished compiler/encoders/asm                                   50s 741MB
Nov 25 09:02:52 Starting compiler/encoders/x64
Nov 25 09:03:48 Finished compiler/encoders/x64                                   55s   1GB
Nov 25 09:03:48 Starting compiler/encoders/arm7
Nov 25 09:05:43 Finished compiler/encoders/arm7                                1m54s 956MB
Nov 25 09:05:43 Starting compiler/encoders/arm8
Nov 25 09:06:13 Finished compiler/encoders/arm8                                  30s 601MB
Nov 25 09:06:14 Starting compiler/encoders/mips
Nov 25 09:06:51 Finished compiler/encoders/mips                                  37s   1GB
Nov 25 09:06:51 Starting compiler/encoders/riscv
Nov 25 09:07:24 Finished compiler/encoders/riscv                                 32s 726MB
Nov 25 09:07:24 Starting compiler/encoders/ag32
Nov 25 09:08:05 Finished compiler/encoders/ag32                                  40s 667MB
Nov 25 09:08:05 Starting compiler/backend/x64
Nov 25 09:08:48 Finished compiler/backend/x64                                    42s   1GB
Nov 25 09:08:48 Starting compiler/backend/arm7
Nov 25 09:09:34 Finished compiler/backend/arm7                                   45s   1GB
Nov 25 09:09:34 Starting compiler/backend/arm8
Nov 25 09:10:16 Finished compiler/backend/arm8                                   41s   1GB
Nov 25 09:10:17 Starting compiler/backend/mips
Nov 25 09:11:00 Finished compiler/backend/mips                                   42s   1GB
Nov 25 09:11:00 Starting compiler/backend/riscv
Nov 25 09:11:40 Finished compiler/backend/riscv                                  40s   1GB
Nov 25 09:11:41 Starting compiler/backend/ag32
Nov 25 09:14:07 Finished compiler/backend/ag32                                 2m25s   1GB
Nov 25 09:14:07 Starting compiler/parsing/proofs
Nov 25 09:22:27 Finished compiler/parsing/proofs                               8m19s   1GB
Nov 25 09:22:27 Starting compiler/inference/proofs
Nov 25 09:27:42 Finished compiler/inference/proofs                             5m14s 979MB
Nov 25 09:27:42 Starting compiler/backend/semantics
Nov 25 10:29:38 Finished compiler/backend/semantics                         1h01m55s   3GB
Nov 25 10:29:38 Starting compiler/backend/reg_alloc/proofs
Nov 25 10:37:15 Finished compiler/backend/reg_alloc/proofs                     7m37s 908MB
Nov 25 10:37:16 Starting compiler/backend/proofs
Nov 25 12:18:48 Finished compiler/backend/proofs                            1h41m31s  16GB
Nov 25 12:18:48 Starting compiler/backend/serialiser
Nov 25 12:21:21 Finished compiler/backend/serialiser                           2m32s   1GB
Nov 25 12:21:21 Starting compiler/encoders/x64/proofs
Nov 25 12:42:37 Finished compiler/encoders/x64/proofs                         21m16s   5GB
Nov 25 12:42:37 Starting compiler/encoders/arm7/proofs
Nov 25 13:12:01 Finished compiler/encoders/arm7/proofs                        29m23s   6GB
Nov 25 13:12:01 Starting compiler/encoders/arm8/proofs
Nov 25 13:27:34 Finished compiler/encoders/arm8/proofs                        15m31s   1GB
Nov 25 13:27:34 Starting compiler/encoders/mips/proofs
Nov 25 13:50:16 Finished compiler/encoders/mips/proofs                        22m42s   2GB
Nov 25 13:50:16 Starting compiler/encoders/riscv/proofs
Nov 25 14:10:23 Finished compiler/encoders/riscv/proofs                       20m06s   1GB
Nov 25 14:10:23 Starting compiler/encoders/ag32/proofs
Nov 25 14:16:07 Finished compiler/encoders/ag32/proofs                         5m44s 856MB
Nov 25 14:16:08 Starting compiler/backend/x64/proofs
Nov 25 14:16:59 Finished compiler/backend/x64/proofs                             51s   1GB
Nov 25 14:16:59 Starting compiler/backend/arm7/proofs
Nov 25 14:17:50 Finished compiler/backend/arm7/proofs                            51s   1GB
Nov 25 14:17:51 Starting compiler/backend/arm8/proofs
Nov 25 14:18:41 Finished compiler/backend/arm8/proofs                            50s   1GB
Nov 25 14:18:41 Starting compiler/backend/mips/proofs
Nov 25 14:19:32 Finished compiler/backend/mips/proofs                            50s   1GB
Nov 25 14:19:32 Starting compiler/backend/riscv/proofs
Nov 25 14:20:23 Finished compiler/backend/riscv/proofs                           50s   1GB
Nov 25 14:20:23 Starting compiler/backend/ag32/proofs
Nov 25 14:47:23 Finished compiler/backend/ag32/proofs                         27m00s   2GB
Nov 25 14:47:24 Starting compiler/proofs
Nov 25 14:51:35 Finished compiler/proofs                                       4m11s   3GB
Nov 25 14:51:36 Starting candle/set-theory
Nov 25 14:52:36 Finished candle/set-theory                                       59s 852MB
Nov 25 14:52:36 Starting candle/syntax-lib
Nov 25 14:53:00 Finished candle/syntax-lib                                       24s 647MB
Nov 25 14:53:01 Starting candle/standard/syntax
Nov 25 14:56:58 Finished candle/standard/syntax                                3m57s   1GB
Nov 25 14:56:58 Starting candle/standard/semantics
Nov 25 15:00:41 Finished candle/standard/semantics                             3m41s   1GB
Nov 25 15:00:41 Starting candle/standard/monadic
Nov 25 15:04:21 Finished candle/standard/monadic                               3m40s   1GB
Nov 25 15:04:21 Starting candle/standard/ml_kernel
Nov 25 15:16:00 Finished candle/standard/ml_kernel                            11m38s   3GB
Nov 25 15:16:01 Starting candle/overloading/syntax
Nov 25 15:21:01 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                                                                                                                                                                                                         (17s)     OK
holSyntaxTheory                                                                                                                                                                                                                 (46s)     OK
Starting work on holSyntaxExtraTheory
holSyntaxExtraTheory                                                                                                                                                                                                           (220s)     OK
Starting work on holBoolSyntaxTheory
Starting work on holSyntaxRenamingTyvarTheory
holSyntaxRenamingTyvarTheory                                                                                                                                                                                                    (22s)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                                                                                                                                                                                                             (22s)MKILLED