Job 2025

CakeML:8f0d65ee6ef75967a24c98e0efcaef83606cbafe
  Fix some breakage [Oct 26 12:53:15]
HOL:d0be848293e4de8a9b3179ad479e5ee5e184cb35
  Minor update to documentation of splitting fields. [Oct 19 02:06:16]
Machine:oven3
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Oct 27 13:37:08 Claimed job
Oct 27 13:37:13 Reusing HOL
Oct 27 13:38:06 Starting developers
Oct 27 13:38:15 Finished developers                                               8s 104MB
Oct 27 13:38:15 Starting developers/bin
Oct 27 13:38:28 Finished developers/bin                                          12s   1GB
Oct 27 13:38:28 Starting compiler/proofs
Oct 27 16:59:25 Finished compiler/proofs                                    3h20m56s  15GB
Oct 27 16:59:25 Starting compiler/bootstrap/translation
Oct 28 03:25:16 Finished compiler/bootstrap/translation                    10h25m51s  64GB
Oct 28 03:25:17 Starting semantics/ffi
Oct 28 03:25:25 Finished semantics/ffi                                            7s 216MB
Oct 28 03:25:25 Starting semantics
Oct 28 03:25:28 Finished semantics                                                2s  16MB
Oct 28 03:25:28 Starting semantics/proofs
Oct 28 03:26:38 Finished semantics/proofs                                      1m09s 616MB
Oct 28 03:26:38 Starting semantics/alt_semantics
Oct 28 03:27:35 Finished semantics/alt_semantics                                 56s 570MB
Oct 28 03:27:36 Starting semantics/alt_semantics/proofs
Oct 28 03:53:48 Finished semantics/alt_semantics/proofs                       26m11s   1GB
Oct 28 03:53:48 Starting basis/pure
Oct 28 03:53:51 Finished basis/pure                                               2s  33MB
Oct 28 03:53:51 Starting translator
Oct 28 03:57:29 Finished translator                                            3m38s   1GB
Oct 28 03:57:29 Starting compiler/parsing
Oct 28 03:57:32 Finished compiler/parsing                                         2s  33MB
Oct 28 03:57:32 Starting characteristic
Oct 28 03:57:35 Finished characteristic                                           3s  26MB
Oct 28 03:57:36 Starting translator/monadic
Oct 28 03:57:39 Finished translator/monadic                                       2s  26MB
Oct 28 03:57:39 Starting basis
Oct 28 04:05:05 Finished basis                                                 7m25s   3GB
Oct 28 04:05:05 Starting compiler/inference
Oct 28 04:05:08 Finished compiler/inference                                       2s  33MB
Oct 28 04:05:08 Starting compiler/backend/reg_alloc
Oct 28 04:05:10 Finished compiler/backend/reg_alloc                               2s  17MB
Oct 28 04:05:10 Starting compiler/backend/gc
Oct 28 04:05:14 Finished compiler/backend/gc                                      3s  32MB
Oct 28 04:05:15 Starting compiler/backend
Oct 28 04:05:38 Finished compiler/backend                                        23s 588MB
Oct 28 04:05:38 Starting compiler/encoders/asm
Oct 28 04:05:41 Finished compiler/encoders/asm                                    2s  23MB
Oct 28 04:05:41 Starting compiler/encoders/x64
Oct 28 04:05:44 Finished compiler/encoders/x64                                    2s  31MB
Oct 28 04:05:44 Starting compiler/encoders/arm7
Oct 28 04:05:47 Finished compiler/encoders/arm7                                   2s  22MB
Oct 28 04:05:48 Starting compiler/encoders/arm8
Oct 28 04:05:50 Finished compiler/encoders/arm8                                   2s  28MB
Oct 28 04:05:51 Starting compiler/encoders/arm8_asl
Oct 28 04:12:23 Finished compiler/encoders/arm8_asl                            6m31s   1GB
Oct 28 04:12:23 Starting compiler/encoders/mips
Oct 28 04:12:25 Finished compiler/encoders/mips                                   2s  31MB
Oct 28 04:12:26 Starting compiler/encoders/riscv
Oct 28 04:12:28 Finished compiler/encoders/riscv                                  2s  29MB
Oct 28 04:12:29 Starting compiler/encoders/ag32
Oct 28 04:12:32 Finished compiler/encoders/ag32                                   2s  27MB
Oct 28 04:12:32 Starting compiler/backend/x64
Oct 28 04:12:36 Finished compiler/backend/x64                                     3s  33MB
Oct 28 04:12:36 Starting compiler/backend/arm7
Oct 28 04:12:39 Finished compiler/backend/arm7                                    2s  31MB
Oct 28 04:12:39 Starting compiler/backend/arm8
Oct 28 04:12:43 Finished compiler/backend/arm8                                    3s  32MB
Oct 28 04:12:43 Starting compiler/backend/mips
Oct 28 04:12:47 Finished compiler/backend/mips                                    3s  25MB
Oct 28 04:12:47 Starting compiler/backend/riscv
Oct 28 04:12:51 Finished compiler/backend/riscv                                   3s  33MB
Oct 28 04:12:51 Starting compiler/backend/ag32
Oct 28 04:15:48 Finished compiler/backend/ag32                                 2m56s   1GB
Oct 28 04:15:49 Starting compiler/parsing/proofs
Oct 28 04:15:52 Finished compiler/parsing/proofs                                  2s  29MB
Oct 28 04:15:52 Starting compiler/inference/proofs
Oct 28 04:15:55 Finished compiler/inference/proofs                                2s  30MB
Oct 28 04:15:55 Starting compiler/backend/semantics
Oct 28 04:18:18 Finished compiler/backend/semantics                            2m22s   1GB
Oct 28 04:18:18 Starting compiler/backend/reg_alloc/proofs
Oct 28 04:18:22 Finished compiler/backend/reg_alloc/proofs                        3s  32MB
Oct 28 04:18:22 Starting compiler/backend/proofs
Oct 28 04:20:17 Finished compiler/backend/proofs                               1m55s   2GB
Oct 28 04:20:18 Starting compiler/backend/serialiser
Oct 28 04:20:23 Finished compiler/backend/serialiser                              5s  47MB
Oct 28 04:20:23 Starting compiler/encoders/x64/proofs
Oct 28 04:42:13 Finished compiler/encoders/x64/proofs                         21m49s   5GB
Oct 28 04:42:13 Starting compiler/encoders/arm7/proofs
Oct 28 05:12:44 Finished compiler/encoders/arm7/proofs                        30m30s   3GB
Oct 28 05:12:44 Starting compiler/encoders/arm8/proofs
Oct 28 05:28:41 Finished compiler/encoders/arm8/proofs                        15m57s   1GB
Oct 28 05:28:42 Starting compiler/encoders/arm8_asl/proofs
Oct 28 06:04:35 Finished compiler/encoders/arm8_asl/proofs                    35m52s   2GB
Oct 28 06:04:35 Starting compiler/encoders/mips/proofs
Oct 28 06:28:20 Finished compiler/encoders/mips/proofs                        23m44s   2GB
Oct 28 06:28:21 Starting compiler/encoders/riscv/proofs
Oct 28 06:48:35 Finished compiler/encoders/riscv/proofs                       20m13s   1GB
Oct 28 06:48:35 Starting compiler/encoders/ag32/proofs
Oct 28 06:54:33 Finished compiler/encoders/ag32/proofs                         5m57s   1GB
Oct 28 06:54:33 Starting compiler/backend/x64/proofs
Oct 28 06:55:29 Finished compiler/backend/x64/proofs                             55s   1GB
Oct 28 06:55:30 Starting compiler/backend/arm7/proofs
Oct 28 06:56:23 Finished compiler/backend/arm7/proofs                            53s   1GB
Oct 28 06:56:24 Starting compiler/backend/arm8/proofs
Oct 28 06:57:20 Finished compiler/backend/arm8/proofs                            55s   1GB
Oct 28 06:57:20 Starting compiler/backend/arm8_asl
Oct 28 06:58:03 Finished compiler/backend/arm8_asl                               43s   1GB
Oct 28 06:58:04 Starting compiler/backend/mips/proofs
Oct 28 06:58:58 Finished compiler/backend/mips/proofs                            54s   1GB
Oct 28 06:58:59 Starting compiler/backend/riscv/proofs
Oct 28 06:59:55 Finished compiler/backend/riscv/proofs                           56s   1GB
Oct 28 06:59:55 Starting compiler/backend/ag32/proofs
Oct 28 07:29:45 Finished compiler/backend/ag32/proofs                         29m49s   2GB
Oct 28 07:29:46 Starting candle/set-theory
Oct 28 07:30:52 Finished candle/set-theory                                     1m06s   1GB
Oct 28 07:30:53 Starting candle/syntax-lib
Oct 28 07:30:55 Finished candle/syntax-lib                                        2s  35MB
Oct 28 07:30:55 Starting candle/standard/syntax
Oct 28 07:31:14 Finished candle/standard/syntax                                  18s 543MB
Oct 28 07:31:14 Starting candle/standard/semantics
Oct 28 07:34:58 Finished candle/standard/semantics                             3m43s   1GB
Oct 28 07:34:58 Starting candle/standard/monadic
Oct 28 07:35:01 Finished candle/standard/monadic                                  3s  33MB
Oct 28 07:35:01 Starting candle/standard/ml_kernel
Oct 28 07:37:56 Finished candle/standard/ml_kernel                             2m54s   2GB
Oct 28 07:37:56 Starting candle/overloading/syntax
Oct 28 07:45:00 Finished candle/overloading/syntax                             7m03s   1GB
Oct 28 07:45:00 Starting candle/overloading/semantics
Oct 28 08:12:08 Finished candle/overloading/semantics                         27m07s   2GB
Oct 28 08:12:08 Starting candle/overloading/monadic
Oct 28 08:17:39 Finished candle/overloading/monadic                            5m31s   2GB
Oct 28 08:17:40 Starting candle/overloading/ml_kernel
Oct 28 08:33:16 Finished candle/overloading/ml_kernel                         15m36s   3GB
Oct 28 08:33:16 Starting candle/overloading/ml_checker
Oct 28 08:38:36 Finished candle/overloading/ml_checker                         5m19s   3GB
Oct 28 08:38:36 Starting candle/prover
Oct 28 09:00:03 Finished candle/prover                                        21m26s   3GB
Oct 28 09:00:03 Starting pancake
Oct 28 09:06:28 Finished pancake                                               6m24s   4GB
Oct 28 09:06:28 Starting pancake/ffi
Oct 28 09:06:29 Finished pancake/ffi                                              0s  17MB
Oct 28 09:06:29 Starting pancake/semantics
Oct 28 09:11:42 Finished pancake/semantics                                     5m12s   1GB
Oct 28 09:11:42 Starting pancake/proofs
Oct 28 09:17:56 Finished pancake/proofs                                        6m13s   2GB
Oct 28 09:17:56 Starting characteristic/examples
Oct 28 09:20:55 Finished characteristic/examples                               2m59s   2GB
Oct 28 09:20:55 Starting tutorial/solutions
Oct 28 09:55:36 Finished tutorial/solutions                                   34m40s   9GB
Oct 28 09:55:36 Starting translator/monadic/examples
Oct 28 10:02:11 Finished translator/monadic/examples                           6m34s   2GB
Oct 28 10:02:11 Starting examples
Oct 28 10:21:20 Finished examples                                             19m08s   3GB
Oct 28 10:21:21 Starting examples/compilation/x64
Oct 28 14:57:12 Finished examples/compilation/x64                           4h35m51s  20GB
Oct 28 14:57:12 Starting examples/compilation/x64/proofs
Oct 28 15:00:54 Finished examples/compilation/x64/proofs                       3m41s   3GB
Oct 28 15:00:54 Starting examples/compilation/ag32
Oct 28 16:15:02 Finished examples/compilation/ag32                          1h14m07s   9GB
Oct 28 16:15:03 Starting examples/compilation/ag32/proofs
Oct 28 16:16:47 Finished examples/compilation/ag32/proofs                      1m43s   3GB
Oct 28 16:16:47 Starting examples/compilation/to_word
Oct 28 16:23:26 Finished examples/compilation/to_word                          6m38s   6GB
Oct 28 16:23:26 Starting examples/lpr_checker
Oct 28 16:25:25 Finished examples/lpr_checker                                  1m59s 891MB
Oct 28 16:25:26 Starting examples/lpr_checker/array
Oct 28 17:43:29 Finished examples/lpr_checker/array                         1h18m03s   5GB
Oct 28 17:43:30 Starting examples/lpr_checker/array/compilation
Oct 28 19:04:14 Finished examples/lpr_checker/array/compilation             1h20m43s  35GB
Oct 28 19:04:14 Starting examples/lpr_checker/array/compilation/proofs
Oct 28 19:06:52 Finished examples/lpr_checker/array/compilation/proofs         2m37s   6GB
Oct 28 19:06:52 Starting examples/opentheory
Oct 28 19:29:26 Finished examples/opentheory                                  22m33s   4GB
Oct 28 19:29:26 Starting examples/opentheory
Oct 28 19:29:30 Finished examples/opentheory                                      3s  32MB
Oct 28 19:29:30 Starting examples/opentheory/compilation
Oct 28 20:57:22 Finished examples/opentheory/compilation                    1h27m51s  40GB
Oct 28 20:57:22 Starting examples/opentheory/compilation/proofs
Oct 28 20:59:02 Finished examples/opentheory/compilation/proofs                1m39s   4GB
Oct 28 20:59:02 Starting examples/opentheory/compilation/ag32
Oct 28 22:18:30 Finished examples/opentheory/compilation/ag32               1h19m27s  37GB
Oct 28 22:18:30 Starting examples/opentheory/compilation/ag32/proofs
Oct 28 22:22:09 Finished examples/opentheory/compilation/ag32/proofs           3m38s   6GB
Oct 28 22:22:09 Starting examples/sat_encodings
Oct 28 22:25:59 Finished examples/sat_encodings                                3m49s 838MB
Oct 28 22:25:59 Starting examples/sat_encodings/case_studies
Oct 28 22:29:21 Finished examples/sat_encodings/case_studies                   3m21s 924MB
Oct 28 22:29:21 Starting examples/sat_encodings/translation
Oct 28 22:41:21 Finished examples/sat_encodings/translation                   11m59s   3GB
Oct 28 22:41:21 Starting examples/sat_encodings/translation/compilation
Oct 29 00:05:29 Finished examples/sat_encodings/translation/compilation     1h24m07s  24GB
Oct 29 00:05:29 Starting examples/deflate
Oct 29 00:07:10 Finished examples/deflate                                      1m40s 859MB
Oct 29 00:07:10 Starting examples/deflate/translation
Oct 29 00:10:08 Finished examples/deflate/translation                          2m57s   3GB
Oct 29 00:10:09 Starting examples/deflate/translation/compilation
Oct 29 00:49:06 Finished examples/deflate/translation/compilation             38m57s  15GB
Oct 29 00:49:07 Starting translator/okasaki-examples
Oct 29 00:59:12 Finished translator/okasaki-examples                          10m05s   1GB
Oct 29 00:59:13 Starting translator/other-examples
Oct 29 01:03:55 Finished translator/other-examples                             4m42s   1GB
Oct 29 01:03:55 Starting compiler/parsing/tests
Oct 29 01:05:03 Finished compiler/parsing/tests                                1m07s 511MB
Oct 29 01:05:03 Starting compiler/inference/tests
Oct 29 01:22:08 Finished compiler/inference/tests                             17m03s   3GB
Oct 29 01:22:08 Starting compiler/printing/test
Oct 29 01:29:08 Finished compiler/printing/test                                6m59s   3GB
Oct 29 01:29:08 Starting icing/flover
Oct 29 03:00:20 Finished icing/flover                                       1h31m11s   1GB
Oct 29 03:00:20 Starting icing/
Oct 29 05:15:09 Finished icing/                                             2h14m47s   5GB
Oct 29 05:15:09 Starting icing/examples
Oct 29 05:18:34 Finished icing/examples                                        3m24s   5GB
Oct 29 05:18:34 Starting compiler/repl
Oct 29 05:36:56 Finished compiler/repl                                        18m21s   4GB
Oct 29 05:36:56 Starting unverified/sexpr-bootstrap/x64/64
Oct 29 06:00:11 Finished unverified/sexpr-bootstrap/x64/64                    23m13s  10GB
Oct 29 06:00:11 Starting unverified/sexpr-bootstrap/x64/32
Oct 29 06:18:52 Finished unverified/sexpr-bootstrap/x64/32                    18m39s  12GB
Oct 29 06:18:52 Starting compiler/benchmarks
Oct 29 06:18:58 Finished compiler/benchmarks                                      6s  33MB
Oct 29 06:18:59 Starting compiler/bootstrap/compilation/x64/64
Oct 30 08:20:44 Finished compiler/bootstrap/compilation/x64/64             26h01m43s 110GB
Oct 30 08:20:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 30 09:03:05 Finished compiler/bootstrap/compilation/x64/64/proofs         42m20s  30GB
Oct 30 09:03:05 Starting compiler/bootstrap/compilation/x64/32
Oct 30 22:54:36 Finished compiler/bootstrap/compilation/x64/32             13h51m29s  80GB
Oct 30 22:54:36 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 30 22:59:19 Finished compiler/bootstrap/compilation/x64/32/proofs          4m42s  16GB
Oct 30 22:59:19 Starting compiler/bootstrap/compilation/ag32/32
Oct 31 13:22:18 Finished compiler/bootstrap/compilation/ag32/32            14h22m57s  75GB
Oct 31 13:22:18 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 31 13:35:55 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m36s  32GB
Oct 31 13:35:56 SUCCESS