Job 2763

CakeML:f8f23fa799727775c9097635ac1f25e719a57113
  fix wording [Jan 04 02:55:34]
#1119 (ordinarymath-patch-1)
Merging into:1fc6f802c664dfdaa2bbfb1e5e4a2051bcf68756
  Update COPYING for 2025 [Jan 01 03:05:36]
HOL:5c113170525b75be2ec405b1079ec20d2008f2c4
  Remove some more adjoin_to* (from pairScript.sml) [Jan 20 23:55:48]
Machine:pavlova

Jan 22 07:40:05 Claimed job
Jan 22 07:40:13 Building HOL
Jan 22 07:51:10 Starting developers
Jan 22 07:51:14 Finished developers                                               3s 154MB
Jan 22 07:51:15 Starting developers/bin
Jan 22 07:51:22 Finished developers/bin                                           5s 746MB
Jan 22 07:51:23 Starting misc
Jan 22 07:52:22 Finished misc                                                    58s   2GB
Jan 22 07:52:23 Starting compiler/proofs
Jan 22 09:34:44 Finished compiler/proofs                                    1h42m19s  33GB
Jan 22 09:34:45 Starting compiler/bootstrap/translation
Jan 22 15:25:06 Finished compiler/bootstrap/translation                     5h50m20s  66GB
Jan 22 15:25:07 Starting semantics/ffi
Jan 22 15:25:17 Finished semantics/ffi                                            9s 580MB
Jan 22 15:25:18 Starting semantics
Jan 22 15:25:20 Finished semantics                                                0s  52MB
Jan 22 15:25:21 Starting semantics/proofs
Jan 22 15:25:45 Finished semantics/proofs                                        23s 746MB
Jan 22 15:25:46 Starting semantics/alt_semantics
Jan 22 15:26:07 Finished semantics/alt_semantics                                 20s 898MB
Jan 22 15:26:08 Starting semantics/alt_semantics/proofs
Jan 22 15:36:39 Finished semantics/alt_semantics/proofs                       10m29s   2GB
Jan 22 15:36:40 Starting basis/pure
Jan 22 15:36:41 Finished basis/pure                                               0s  60MB
Jan 22 15:36:42 Starting translator
Jan 22 15:38:21 Finished translator                                            1m38s   2GB
Jan 22 15:38:22 Starting compiler/parsing
Jan 22 15:38:23 Finished compiler/parsing                                         0s  61MB
Jan 22 15:38:24 Starting characteristic
Jan 22 15:38:26 Finished characteristic                                           0s  80MB
Jan 22 15:38:27 Starting translator/monadic
Jan 22 15:38:29 Finished translator/monadic                                       0s  88MB
Jan 22 15:38:29 Starting translator/monadic/monad_base
Jan 22 15:38:31 Finished translator/monadic/monad_base                            0s  52MB
Jan 22 15:38:32 Starting basis
Jan 22 15:40:52 Finished basis                                                 2m19s   3GB
Jan 22 15:40:53 Starting compiler
Jan 22 15:40:56 Finished compiler                                                 1s 188MB
Jan 22 15:40:57 Starting compiler/inference
Jan 22 15:40:59 Finished compiler/inference                                       0s  84MB
Jan 22 15:41:00 Starting compiler/backend/reg_alloc
Jan 22 15:41:01 Finished compiler/backend/reg_alloc                               0s  53MB
Jan 22 15:41:02 Starting compiler/backend/gc
Jan 22 15:41:04 Finished compiler/backend/gc                                      1s 129MB
Jan 22 15:41:05 Starting compiler/backend
Jan 22 15:41:10 Finished compiler/backend                                         4s 267MB
Jan 22 15:41:11 Starting compiler/encoders/asm
Jan 22 15:41:12 Finished compiler/encoders/asm                                    0s  84MB
Jan 22 15:41:13 Starting compiler/encoders/x64
Jan 22 15:41:15 Finished compiler/encoders/x64                                    0s  89MB
Jan 22 15:41:16 Starting compiler/encoders/arm7
Jan 22 15:41:18 Finished compiler/encoders/arm7                                   0s  86MB
Jan 22 15:41:19 Starting compiler/encoders/arm8
Jan 22 15:41:20 Finished compiler/encoders/arm8                                   0s  88MB
Jan 22 15:41:21 Starting compiler/encoders/arm8_asl
Jan 22 17:41:03 Finished compiler/encoders/arm8_asl                         1h59m41s  41GB
Jan 22 17:41:04 Starting compiler/encoders/mips
Jan 22 17:41:06 Finished compiler/encoders/mips                                   0s  87MB
Jan 22 17:41:07 Starting compiler/encoders/riscv
Jan 22 17:41:09 Finished compiler/encoders/riscv                                  0s  84MB
Jan 22 17:41:09 Starting compiler/encoders/ag32
Jan 22 17:41:11 Finished compiler/encoders/ag32                                   0s  82MB
Jan 22 17:41:12 Starting compiler/encoders/tests
Jan 22 17:41:14 Finished compiler/encoders/tests                                  1s 114MB
Jan 22 17:41:15 Starting compiler/encoders/monadic_enc
Jan 22 17:41:17 Finished compiler/encoders/monadic_enc                            1s 125MB
Jan 22 17:41:18 Starting compiler/backend/x64
Jan 22 17:41:20 Finished compiler/backend/x64                                     1s 131MB
Jan 22 17:41:21 Starting compiler/backend/arm7
Jan 22 17:41:23 Finished compiler/backend/arm7                                    1s 125MB
Jan 22 17:41:24 Starting compiler/backend/arm8
Jan 22 17:41:26 Finished compiler/backend/arm8                                    1s 125MB
Jan 22 17:41:27 Starting compiler/backend/mips
Jan 22 17:41:29 Finished compiler/backend/mips                                    1s 125MB
Jan 22 17:41:30 Starting compiler/backend/riscv
Jan 22 17:41:32 Finished compiler/backend/riscv                                   1s 125MB
Jan 22 17:41:33 Starting compiler/backend/ag32
Jan 22 17:42:39 Finished compiler/backend/ag32                                 1m05s   1GB
Jan 22 17:42:40 Starting compiler/backend/pattern_matching
Jan 22 17:42:41 Finished compiler/backend/pattern_matching                        0s  51MB
Jan 22 17:42:42 Starting compiler/parsing/ocaml
Jan 22 17:44:24 Finished compiler/parsing/ocaml                                1m40s   1GB
Jan 22 17:44:25 Starting compiler/printing
Jan 22 17:44:26 Finished compiler/printing                                        0s  81MB
Jan 22 17:44:27 Starting compiler/parsing/proofs
Jan 22 17:44:29 Finished compiler/parsing/proofs                                  0s  59MB
Jan 22 17:44:30 Starting compiler/inference/proofs
Jan 22 17:44:31 Finished compiler/inference/proofs                                0s  90MB
Jan 22 17:44:32 Starting compiler/backend/semantics
Jan 22 17:47:37 Finished compiler/backend/semantics                            3m03s   3GB
Jan 22 17:47:37 Starting compiler/backend/reg_alloc/proofs
Jan 22 17:47:39 Finished compiler/backend/reg_alloc/proofs                        0s  84MB
Jan 22 17:47:40 Starting compiler/backend/proofs
Jan 22 17:48:29 Finished compiler/backend/proofs                                 48s   3GB
Jan 22 17:48:30 Starting compiler/backend/serialiser
Jan 22 17:48:32 Finished compiler/backend/serialiser                              1s 132MB
Jan 22 17:48:33 Starting compiler/encoders/x64/proofs
Jan 22 17:58:53 Finished compiler/encoders/x64/proofs                         10m19s   5GB
Jan 22 17:58:54 Starting compiler/encoders/arm7/proofs
Jan 22 18:12:04 Finished compiler/encoders/arm7/proofs                        13m08s   5GB
Jan 22 18:12:05 Starting compiler/encoders/arm8/proofs
Jan 22 18:19:19 Finished compiler/encoders/arm8/proofs                         7m12s   4GB
Jan 22 18:19:20 Starting compiler/encoders/arm8_asl/proofs
Jan 22 19:09:01 Finished compiler/encoders/arm8_asl/proofs                    49m40s  18GB
Jan 22 19:09:02 Starting compiler/encoders/mips/proofs
Jan 22 19:19:23 Finished compiler/encoders/mips/proofs                        10m20s   9GB
Jan 22 19:19:24 Starting compiler/encoders/riscv/proofs
Jan 22 19:27:41 Finished compiler/encoders/riscv/proofs                        8m16s   4GB
Jan 22 19:27:42 Starting compiler/encoders/ag32/proofs
Jan 22 19:30:35 Finished compiler/encoders/ag32/proofs                         2m51s   1GB
Jan 22 19:30:36 Starting compiler/backend/x64/proofs
Jan 22 19:31:07 Finished compiler/backend/x64/proofs                             30s   2GB
Jan 22 19:31:08 Starting compiler/backend/arm7/proofs
Jan 22 19:31:39 Finished compiler/backend/arm7/proofs                            30s   2GB
Jan 22 19:31:40 Starting compiler/backend/arm8/proofs
Jan 22 19:32:11 Finished compiler/backend/arm8/proofs                            29s   2GB
Jan 22 19:32:12 Starting compiler/backend/arm8_asl
Jan 22 19:32:31 Finished compiler/backend/arm8_asl                               18s   1GB
Jan 22 19:32:32 Starting compiler/backend/mips/proofs
Jan 22 19:33:04 Finished compiler/backend/mips/proofs                            30s   2GB
Jan 22 19:33:05 Starting compiler/backend/riscv/proofs
Jan 22 19:33:38 Finished compiler/backend/riscv/proofs                           32s   2GB
Jan 22 19:33:38 Starting compiler/backend/ag32/proofs
Jan 22 19:47:34 Finished compiler/backend/ag32/proofs                         13m54s   5GB
Jan 22 19:47:35 Starting compiler/backend/cv_compute
Jan 22 19:48:46 Finished compiler/backend/cv_compute                           1m10s   2GB
Jan 22 19:48:47 Starting cv_translator
Jan 22 20:09:48 Finished cv_translator                                        21m00s   6GB
Jan 22 20:09:49 Starting candle
Jan 22 20:09:50 Finished candle                                                   0s  12MB
Jan 22 20:09:51 Starting candle/set-theory
Jan 22 20:10:27 Finished candle/set-theory                                       34s   1GB
Jan 22 20:10:28 Starting candle/syntax-lib
Jan 22 20:10:29 Finished candle/syntax-lib                                        0s  59MB
Jan 22 20:10:30 Starting candle/standard
Jan 22 20:10:31 Finished candle/standard                                          0s  11MB
Jan 22 20:10:32 Starting candle/standard/syntax
Jan 22 20:10:44 Finished candle/standard/syntax                                  11s 776MB
Jan 22 20:10:45 Starting candle/standard/semantics
Jan 22 20:12:48 Finished candle/standard/semantics                             2m01s   1GB
Jan 22 20:12:49 Starting candle/standard/monadic
Jan 22 20:12:51 Finished candle/standard/monadic                                  0s  96MB
Jan 22 20:12:52 Starting candle/standard/ml_kernel
Jan 22 20:14:36 Finished candle/standard/ml_kernel                             1m43s   4GB
Jan 22 20:14:37 Starting candle/standard/ml_kernel/lisp
Jan 22 20:14:39 Finished candle/standard/ml_kernel/lisp                           0s  45MB
Jan 22 20:14:40 Starting candle/overloading
Jan 22 20:14:41 Finished candle/overloading                                       0s  12MB
Jan 22 20:14:42 Starting candle/overloading/syntax
Jan 22 20:17:55 Finished candle/overloading/syntax                             3m12s   2GB
Jan 22 20:17:56 Starting candle/overloading/semantics
Jan 22 20:29:03 Finished candle/overloading/semantics                         11m06s   6GB
Jan 22 20:29:04 Starting candle/overloading/monadic
Jan 22 20:31:22 Finished candle/overloading/monadic                            2m16s   2GB
Jan 22 20:31:23 Starting candle/overloading/ml_kernel
Jan 22 20:38:35 Finished candle/overloading/ml_kernel                          7m10s   5GB
Jan 22 20:38:36 Starting candle/overloading/ml_checker
Jan 22 20:40:48 Finished candle/overloading/ml_checker                         2m11s   6GB
Jan 22 20:40:49 Starting candle/prover
Jan 22 20:50:31 Finished candle/prover                                         9m41s   5GB
Jan 22 20:50:32 Starting candle/prover/compute
Jan 22 20:50:34 Finished candle/prover/compute                                    1s 118MB
Jan 22 20:50:35 Starting pancake
Jan 22 20:50:57 Finished pancake                                                 20s 739MB
Jan 22 20:50:57 Starting pancake/semantics
Jan 22 20:53:08 Finished pancake/semantics                                     2m09s   2GB
Jan 22 20:53:09 Starting pancake/parser
Jan 22 20:53:33 Finished pancake/parser                                          23s 455MB
Jan 22 20:53:34 Starting pancake/proofs
Jan 22 21:09:47 Finished pancake/proofs                                       16m11s   7GB
Jan 22 21:09:48 Starting pancake/ta_progs
Jan 22 21:09:49 Finished pancake/ta_progs                                         0s  11MB
Jan 22 21:09:50 Starting compiler/dafny
Jan 22 21:12:35 Finished compiler/dafny                                        2m44s   9GB
Jan 22 21:12:36 Starting compiler/dafny/translation
Jan 22 21:30:42 Finished compiler/dafny/translation                           18m04s  23GB
Jan 22 21:30:43 Starting compiler/dafny/compilation
Jan 22 21:33:22 Finished compiler/dafny/compilation                            2m38s   9GB
Jan 22 21:33:23 Starting compiler/dafny/semantics
Jan 22 21:33:58 Finished compiler/dafny/semantics                                34s   1GB
Jan 22 21:33:59 Starting characteristic/examples
Jan 22 21:35:24 Finished characteristic/examples                               1m23s   4GB
Jan 22 21:35:24 Starting tutorial/solutions
Jan 22 21:37:46 Finished tutorial/solutions                                    2m20s   3GB
Jan 22 21:37:47 Starting translator/monadic/examples
Jan 22 21:40:45 Finished translator/monadic/examples                           2m56s   4GB
Jan 22 21:40:45 Starting examples
Jan 22 21:46:53 Finished examples                                              6m06s   4GB
Jan 22 21:46:54 Starting examples/compilation
Jan 22 21:46:54 Finished examples/compilation                                     0s  11MB
Jan 22 21:46:55 Starting examples/compilation/x64
Jan 22 21:53:30 Finished examples/compilation/x64                              6m33s   3GB
Jan 22 21:53:31 Starting examples/compilation/x64/proofs
Jan 22 21:56:00 Finished examples/compilation/x64/proofs                       2m28s   4GB
Jan 22 21:56:01 Starting examples/compilation/ag32
Jan 22 21:57:50 Finished examples/compilation/ag32                             1m48s   3GB
Jan 22 21:57:51 Starting examples/compilation/ag32/proofs
Jan 22 21:58:52 Finished examples/compilation/ag32/proofs                      1m00s   5GB
Jan 22 21:58:53 Starting examples/lpr_checker
Jan 22 21:59:23 Finished examples/lpr_checker                                    29s   1GB
Jan 22 21:59:24 Starting examples/lpr_checker/array
Jan 22 22:25:39 Finished examples/lpr_checker/array                           26m13s  25GB
Jan 22 22:25:39 Starting examples/lpr_checker/array/compilation
Jan 22 22:33:58 Finished examples/lpr_checker/array/compilation                8m18s  36GB
Jan 22 22:33:59 Starting examples/lpr_checker/array/compilation/proofs
Jan 22 22:35:11 Finished examples/lpr_checker/array/compilation/proofs         1m11s   6GB
Jan 22 22:35:12 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 22 22:36:21 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
Jan 22 22:36:22 Starting .
Jan 22 22:36:25 Finished .                                                        2s 281MB
Jan 22 22:36:26 Starting examples/xlrup_checker
Jan 22 22:37:01 Finished examples/xlrup_checker                                  34s   1GB
Jan 22 22:37:02 Starting examples/xlrup_checker/array
Jan 22 22:50:07 Finished examples/xlrup_checker/array                         13m04s   9GB
Jan 22 22:50:08 Starting examples/xlrup_checker/array/compilation
Jan 22 22:51:07 Finished examples/xlrup_checker/array/compilation                57s   4GB
Jan 22 22:51:07 Starting examples/xlrup_checker/array/compilation/proofs
Jan 22 22:52:04 Finished examples/xlrup_checker/array/compilation/proofs         55s   4GB
Jan 22 22:52:05 Starting examples/pseudo_bool
Jan 22 22:53:35 Finished examples/pseudo_bool                                  1m29s   2GB
Jan 22 22:53:36 Starting examples/pseudo_bool/cnf_encoding
Jan 22 22:54:05 Finished examples/pseudo_bool/cnf_encoding                       27s   1GB
Jan 22 22:54:06 Starting examples/pseudo_bool/graph_encoding
Jan 22 22:54:51 Finished examples/pseudo_bool/graph_encoding                     44s   1GB
Jan 22 22:54:52 Starting examples/pseudo_bool/array
Jan 23 00:03:08 Finished examples/pseudo_bool/array                         1h08m15s  37GB
Jan 23 00:03:09 Starting examples/pseudo_bool/array/compilation
Jan 23 00:11:54 Finished examples/pseudo_bool/array/compilation                8m43s  15GB
Jan 23 00:11:55 Starting examples/pseudo_bool/array/compilation/proofs
Jan 23 00:14:32 Finished examples/pseudo_bool/array/compilation/proofs         2m36s   6GB
Jan 23 00:14:33 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jan 23 00:15:40 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m05s   6GB
Jan 23 00:15:41 Starting examples/opentheory
Jan 23 00:24:12 Finished examples/opentheory                                   8m30s   5GB
Jan 23 00:24:12 Starting examples/opentheory/compilation
Jan 23 00:25:37 Finished examples/opentheory/compilation                       1m23s   5GB
Jan 23 00:25:38 Starting examples/opentheory/compilation/proofs
Jan 23 00:26:40 Finished examples/opentheory/compilation/proofs                1m00s   4GB
Jan 23 00:26:41 Starting examples/opentheory/compilation/ag32
Jan 23 00:28:07 Finished examples/opentheory/compilation/ag32                  1m25s   5GB
Jan 23 00:28:08 Starting examples/opentheory/compilation/ag32/proofs
Jan 23 00:29:47 Finished examples/opentheory/compilation/ag32/proofs           1m37s   7GB
Jan 23 00:29:48 Starting examples/sat_encodings
Jan 23 00:30:47 Finished examples/sat_encodings                                  58s 805MB
Jan 23 00:30:48 Starting examples/sat_encodings/demo
Jan 23 00:30:49 Finished examples/sat_encodings/demo                              0s  11MB
Jan 23 00:30:50 Starting examples/sat_encodings/case_studies
Jan 23 00:32:34 Finished examples/sat_encodings/case_studies                   1m43s   1GB
Jan 23 00:32:35 Starting examples/sat_encodings/translation
Jan 23 00:36:08 Finished examples/sat_encodings/translation                    3m31s   2GB
Jan 23 00:36:09 Starting examples/sat_encodings/translation/compilation
Jan 23 00:37:58 Finished examples/sat_encodings/translation/compilation        1m48s   4GB
Jan 23 00:37:59 Starting examples/deflate
Jan 23 00:38:27 Finished examples/deflate                                        27s 701MB
Jan 23 00:38:28 Starting examples/deflate/translation
Jan 23 00:39:32 Finished examples/deflate/translation                          1m03s   4GB
Jan 23 00:39:33 Starting examples/deflate/translation/compilation
Jan 23 00:40:20 Finished examples/deflate/translation/compilation                45s   3GB
Jan 23 00:40:21 Starting examples/vipr
Jan 23 00:43:48 Finished examples/vipr                                         3m25s   4GB
Jan 23 00:43:49 Starting examples/vipr/compilation
Jan 23 00:44:44 Finished examples/vipr/compilation                               54s   3GB
Jan 23 00:44:45 Starting translator/okasaki-examples
Jan 23 00:48:47 Finished translator/okasaki-examples                           4m01s   3GB
Jan 23 00:48:48 Starting translator/other-examples
Jan 23 00:51:51 Finished translator/other-examples                             3m01s   3GB
Jan 23 00:51:52 Starting translator/other-examples/auxiliary
Jan 23 00:51:53 Finished translator/other-examples/auxiliary                      0s  11MB
Jan 23 00:51:54 Starting compiler/parsing/tests
Jan 23 00:52:29 Finished compiler/parsing/tests                                  34s   1GB
Jan 23 00:52:30 Starting compiler/inference/tests
Jan 23 00:53:03 Finished compiler/inference/tests                                32s   2GB
Jan 23 00:53:04 Starting compiler/printing/test
Jan 23 00:54:17 Finished compiler/printing/test                                1m12s   5GB
Jan 23 00:54:18 Starting icing/flover
Jan 23 01:28:48 Finished icing/flover                                         34m28s   2GB
Jan 23 01:28:49 Starting icing/flover/Infra
Jan 23 01:28:50 Finished icing/flover/Infra                                       0s  11MB
Jan 23 01:28:51 Starting icing/flover/semantics
Jan 23 01:28:51 Finished icing/flover/semantics                                   0s  11MB
Jan 23 01:28:52 Starting icing/
Jan 23 01:56:04 Finished icing/                                               27m11s   4GB
Jan 23 01:56:05 Starting icing/examples
Jan 23 01:57:39 Finished icing/examples                                        1m32s   7GB
Jan 23 01:57:40 Starting compiler/repl
Jan 23 02:05:41 Finished compiler/repl                                         8m00s   7GB
Jan 23 02:05:42 Starting unverified/sexpr-bootstrap/x64/64
Jan 23 02:09:34 Finished unverified/sexpr-bootstrap/x64/64                     3m50s  16GB
Jan 23 02:09:35 Starting unverified/sexpr-bootstrap/x64/32
Jan 23 02:12:56 Finished unverified/sexpr-bootstrap/x64/32                     3m20s  14GB
Jan 23 02:12:57 Starting compiler/benchmarks
Jan 23 02:13:43 Finished compiler/benchmarks                                     45s 711MB
Jan 23 02:13:44 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Jan 23 02:13:47 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 255MB
Jan 23 02:13:48 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Jan 23 02:13:52 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 247MB
Jan 23 02:13:53 Starting compiler/bootstrap/compilation/x64/64
Jan 23 02:38:09 Finished compiler/bootstrap/compilation/x64/64                24m15s  79GB
Jan 23 02:38:10 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 23 03:02:09 Finished compiler/bootstrap/compilation/x64/64/proofs         23m57s  45GB
Jan 23 03:02:10 Starting compiler/bootstrap/compilation/x64/32
Jan 23 03:25:39 Finished compiler/bootstrap/compilation/x64/32                23m28s  39GB
Jan 23 03:25:40 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 23 03:29:40 Finished compiler/bootstrap/compilation/x64/32/proofs          3m58s  21GB
Jan 23 03:29:41 Starting compiler/bootstrap/compilation/arm8/64
Jan 23 04:05:48 Finished compiler/bootstrap/compilation/arm8/64               36m05s  74GB
Jan 23 04:05:48 Starting compiler/bootstrap/compilation/arm8/64/proofs
Jan 23 04:11:01 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m11s  30GB
Jan 23 04:11:02 Starting compiler/bootstrap/compilation/ag32/32
Jan 23 04:36:51 Finished compiler/bootstrap/compilation/ag32/32               25m48s  67GB
Jan 23 04:36:52 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 23 04:41:52 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m59s  29GB
Jan 23 04:41:53 SUCCESS