Job 1672

CakeML:2e67690f5f745a2fa7b80c5dae218e9861ff1ea6
  Merge pull request #847 from CakeML/clos-smart-op [Nov 30 09:57:02]
HOL:6dcb52a09341deda5c5068c06f92c6eaa2af36b6
  emacs-mode: display *Holmake* buffer better when it does its thing [Nov 26 04:28:46]
Machine:oven3 4.19.67.1.amd64-smp
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Dec 01 04:31:48 Claimed job
Dec 01 04:31:59 Building HOL
Dec 01 04:51:19 Starting developers
Dec 01 04:51:28 Finished developers                                               8s 128MB
Dec 01 04:51:28 Starting developers/bin
Dec 01 04:51:41 Finished developers/bin                                          12s   1GB
Dec 01 04:51:41 Starting semantics/ffi
Dec 01 04:52:00 Finished semantics/ffi                                           18s 248MB
Dec 01 04:52:00 Starting semantics
Dec 01 04:55:15 Finished semantics                                             3m14s   1GB
Dec 01 04:55:15 Starting semantics/proofs
Dec 01 05:03:14 Finished semantics/proofs                                      7m58s   1GB
Dec 01 05:03:14 Starting semantics/alt_semantics
Dec 01 05:03:39 Finished semantics/alt_semantics                                 24s 390MB
Dec 01 05:03:39 Starting semantics/alt_semantics/proofs
Dec 01 05:08:51 Finished semantics/alt_semantics/proofs                        5m11s   1GB
Dec 01 05:08:51 Starting basis/pure
Dec 01 05:14:59 Finished basis/pure                                            6m07s 808MB
Dec 01 05:14:59 Starting translator
Dec 01 05:20:51 Finished translator                                            5m51s   1GB
Dec 01 05:20:51 Starting compiler/parsing
Dec 01 05:23:33 Finished compiler/parsing                                      2m42s   2GB
Dec 01 05:23:34 Starting characteristic
Dec 01 05:35:35 Finished characteristic                                       12m01s   2GB
Dec 01 05:35:35 Starting translator/monadic
Dec 01 05:39:09 Finished translator/monadic                                    3m32s   1GB
Dec 01 05:39:09 Starting basis
Dec 01 07:18:39 Finished basis                                              1h39m29s  19GB
Dec 01 07:18:39 Starting compiler/inference
Dec 01 07:21:22 Finished compiler/inference                                    2m43s   1GB
Dec 01 07:21:23 Starting compiler/backend/reg_alloc
Dec 01 07:23:32 Finished compiler/backend/reg_alloc                            2m09s   1GB
Dec 01 07:23:33 Starting compiler/backend/gc
Dec 01 07:30:27 Finished compiler/backend/gc                                   6m53s   1GB
Dec 01 07:30:27 Starting compiler/backend
Dec 01 07:39:21 Finished compiler/backend                                      8m53s   2GB
Dec 01 07:39:21 Starting compiler/encoders/asm
Dec 01 07:40:10 Finished compiler/encoders/asm                                   48s 696MB
Dec 01 07:40:10 Starting compiler/encoders/x64
Dec 01 07:42:31 Finished compiler/encoders/x64                                 2m20s 782MB
Dec 01 07:42:31 Starting compiler/encoders/arm7
Dec 01 07:46:55 Finished compiler/encoders/arm7                                4m23s   1GB
Dec 01 07:46:55 Starting compiler/encoders/arm8
Dec 01 07:48:17 Finished compiler/encoders/arm8                                1m21s 941MB
Dec 01 07:48:17 Starting compiler/encoders/mips
Dec 01 07:51:36 Finished compiler/encoders/mips                                3m18s   1GB
Dec 01 07:51:36 Starting compiler/encoders/riscv
Dec 01 07:55:28 Finished compiler/encoders/riscv                               3m52s 963MB
Dec 01 07:55:28 Starting compiler/encoders/ag32
Dec 01 07:56:09 Finished compiler/encoders/ag32                                  40s 703MB
Dec 01 07:56:09 Starting compiler/backend/x64
Dec 01 07:56:48 Finished compiler/backend/x64                                    38s   1GB
Dec 01 07:56:49 Starting compiler/backend/arm7
Dec 01 07:57:34 Finished compiler/backend/arm7                                   45s   1GB
Dec 01 07:57:34 Starting compiler/backend/arm8
Dec 01 07:58:17 Finished compiler/backend/arm8                                   42s   1GB
Dec 01 07:58:18 Starting compiler/backend/mips
Dec 01 07:58:59 Finished compiler/backend/mips                                   41s   1GB
Dec 01 07:59:00 Starting compiler/backend/riscv
Dec 01 07:59:42 Finished compiler/backend/riscv                                  42s   1GB
Dec 01 07:59:42 Starting compiler/backend/ag32
Dec 01 08:02:14 Finished compiler/backend/ag32                                 2m31s   1GB
Dec 01 08:02:14 Starting compiler/parsing/proofs
Dec 01 08:10:42 Finished compiler/parsing/proofs                               8m27s   1GB
Dec 01 08:10:42 Starting compiler/inference/proofs
Dec 01 08:16:02 Finished compiler/inference/proofs                             5m19s   1GB
Dec 01 08:16:02 Starting compiler/backend/semantics
Dec 01 09:17:38 Finished compiler/backend/semantics                         1h01m35s   2GB
Dec 01 09:17:38 Starting compiler/backend/reg_alloc/proofs
Dec 01 09:25:17 Finished compiler/backend/reg_alloc/proofs                     7m38s 860MB
Dec 01 09:25:17 Starting compiler/backend/proofs
Dec 01 11:05:59 Finished compiler/backend/proofs                            1h40m41s  17GB
Dec 01 11:05:59 Starting compiler/backend/serialiser
Dec 01 11:08:29 Finished compiler/backend/serialiser                           2m29s   2GB
Dec 01 11:08:30 Starting compiler/encoders/x64/proofs
Dec 01 11:30:02 Finished compiler/encoders/x64/proofs                         21m32s   4GB
Dec 01 11:30:03 Starting compiler/encoders/arm7/proofs
Dec 01 11:59:35 Finished compiler/encoders/arm7/proofs                        29m32s   3GB
Dec 01 11:59:35 Starting compiler/encoders/arm8/proofs
Dec 01 12:14:56 Finished compiler/encoders/arm8/proofs                        15m20s   1GB
Dec 01 12:14:57 Starting compiler/encoders/mips/proofs
Dec 01 12:36:54 Finished compiler/encoders/mips/proofs                        21m57s   2GB
Dec 01 12:36:54 Starting compiler/encoders/riscv/proofs
Dec 01 12:56:54 Finished compiler/encoders/riscv/proofs                       19m59s   1GB
Dec 01 12:56:54 Starting compiler/encoders/ag32/proofs
Dec 01 13:02:35 Finished compiler/encoders/ag32/proofs                         5m40s 937MB
Dec 01 13:02:36 Starting compiler/backend/x64/proofs
Dec 01 13:03:25 Finished compiler/backend/x64/proofs                             49s   1GB
Dec 01 13:03:25 Starting compiler/backend/arm7/proofs
Dec 01 13:04:15 Finished compiler/backend/arm7/proofs                            49s   1GB
Dec 01 13:04:15 Starting compiler/backend/arm8/proofs
Dec 01 13:05:07 Finished compiler/backend/arm8/proofs                            51s   1GB
Dec 01 13:05:07 Starting compiler/backend/mips/proofs
Dec 01 13:05:59 Finished compiler/backend/mips/proofs                            51s   1GB
Dec 01 13:05:59 Starting compiler/backend/riscv/proofs
Dec 01 13:06:48 Finished compiler/backend/riscv/proofs                           48s   1GB
Dec 01 13:06:48 Starting compiler/backend/ag32/proofs
Dec 01 13:34:11 Finished compiler/backend/ag32/proofs                         27m21s   3GB
Dec 01 13:34:11 Starting compiler/proofs
Dec 01 13:38:25 Finished compiler/proofs                                       4m13s   3GB
Dec 01 13:38:25 Starting candle/set-theory
Dec 01 13:39:23 Finished candle/set-theory                                       57s 772MB
Dec 01 13:39:23 Starting candle/syntax-lib
Dec 01 13:39:48 Finished candle/syntax-lib                                       24s 451MB
Dec 01 13:39:48 Starting candle/standard/syntax
Dec 01 13:43:38 Finished candle/standard/syntax                                3m49s   1GB
Dec 01 13:43:38 Starting candle/standard/semantics
Dec 01 13:47:20 Finished candle/standard/semantics                             3m41s   2GB
Dec 01 13:47:20 Starting candle/standard/monadic
Dec 01 13:50:59 Finished candle/standard/monadic                               3m39s   1GB
Dec 01 13:51:00 Starting candle/standard/ml_kernel
Dec 01 14:02:37 Finished candle/standard/ml_kernel                            11m36s   2GB
Dec 01 14:02:37 Starting candle/overloading/syntax
Dec 01 14:09:21 Finished candle/overloading/syntax                             6m43s   1GB
Dec 01 14:09:21 Starting candle/overloading/semantics
Dec 01 14:35:16 Finished candle/overloading/semantics                         25m52s   2GB
Dec 01 14:35:16 Starting pancake
Dec 01 14:39:14 Finished pancake                                               3m58s   2GB
Dec 01 14:39:15 Starting pancake/ffi
Dec 01 14:39:15 Finished pancake/ffi                                              0s   7MB
Dec 01 14:39:15 Starting pancake/semantics
Dec 01 14:44:14 Finished pancake/semantics                                     4m58s   1GB
Dec 01 14:44:14 Starting pancake/proofs
Dec 01 15:09:52 Finished pancake/proofs                                       25m37s   5GB
Dec 01 15:09:52 Starting characteristic/examples
Dec 01 15:12:53 Finished characteristic/examples                               3m01s   2GB
Dec 01 15:12:54 Starting tutorial/solutions
Dec 01 15:49:01 Finished tutorial/solutions                                   36m07s  16GB
Dec 01 15:49:01 Starting translator/monadic/examples
Dec 01 15:54:52 Finished translator/monadic/examples                           5m50s   3GB
Dec 01 15:54:52 Starting examples
Dec 01 16:12:30 Finished examples                                             17m37s   3GB
Dec 01 16:12:30 Starting examples/compilation/x64
Dec 01 21:38:41 Finished examples/compilation/x64                           5h26m09s  17GB
Dec 01 21:38:41 Starting examples/compilation/x64/proofs
Dec 01 21:42:08 Finished examples/compilation/x64/proofs                       3m27s   3GB
Dec 01 21:42:09 Starting examples/compilation/ag32
Dec 01 22:58:37 Finished examples/compilation/ag32                          1h16m28s  10GB
Dec 01 22:58:37 Starting examples/compilation/ag32/proofs
Dec 01 23:00:29 Finished examples/compilation/ag32/proofs                      1m51s   3GB
Dec 01 23:00:29 Starting examples/cost
Dec 02 01:03:38 Finished examples/cost                                      2h03m08s   7GB
Dec 02 01:03:38 Starting examples/lpr_checker
Dec 02 01:05:20 Finished examples/lpr_checker                                  1m41s   2GB
Dec 02 01:05:20 Starting examples/lpr_checker/array
Dec 02 02:07:55 Finished examples/lpr_checker/array                         1h02m34s   7GB
Dec 02 02:07:55 Starting examples/lpr_checker/array/compilation
Dec 02 05:13:44 Finished examples/lpr_checker/array/compilation             3h05m48s  32GB
Dec 02 05:13:44 Starting examples/lpr_checker/array/compilation/proofs
Dec 02 05:16:25 Finished examples/lpr_checker/array/compilation/proofs         2m40s   6GB
Dec 02 05:16:25 Starting examples/opentheory
Dec 02 05:37:56 Finished examples/opentheory                                  21m30s   5GB
Dec 02 05:37:56 Starting examples/opentheory
Dec 02 05:37:58 Finished examples/opentheory                                      2s  33MB
Dec 02 05:37:58 Starting examples/opentheory/compilation
Dec 02 06:59:32 Finished examples/opentheory/compilation                    1h21m32s  32GB
Dec 02 06:59:32 Starting examples/opentheory/compilation/proofs
Dec 02 07:01:06 Finished examples/opentheory/compilation/proofs                1m33s   3GB
Dec 02 07:01:06 Starting examples/opentheory/compilation/ag32
Dec 02 08:30:15 Finished examples/opentheory/compilation/ag32               1h29m08s  28GB
Dec 02 08:30:16 Starting examples/opentheory/compilation/ag32/proofs
Dec 02 08:36:04 Finished examples/opentheory/compilation/ag32/proofs           5m47s   2GB
Dec 02 08:36:04 Starting examples/sat_encodings
Dec 02 08:40:46 Finished examples/sat_encodings                                4m41s   1GB
Dec 02 08:40:46 Starting examples/sat_encodings/case_studies
Dec 02 08:44:45 Finished examples/sat_encodings/case_studies                   3m59s 731MB
Dec 02 08:44:46 Starting examples/sat_encodings/translation
Dec 02 08:58:45 Finished examples/sat_encodings/translation                   13m59s   4GB
Dec 02 08:58:45 Starting examples/sat_encodings/translation/compilation
Dec 02 10:31:09 Finished examples/sat_encodings/translation/compilation     1h32m22s  32GB
Dec 02 10:31:09 Starting translator/okasaki-examples
Dec 02 10:40:32 Finished translator/okasaki-examples                           9m22s   1GB
Dec 02 10:40:32 Starting translator/other-examples
Dec 02 10:44:07 Finished translator/other-examples                             3m34s   1GB
Dec 02 10:44:07 Starting compiler/parsing/tests
Dec 02 10:45:14 Finished compiler/parsing/tests                                1m07s 610MB
Dec 02 10:45:15 Starting compiler/inference/tests
Dec 02 11:01:26 Finished compiler/inference/tests                             16m11s   6GB
Dec 02 11:01:26 Starting compiler/bootstrap/translation
Dec 02 16:36:34 Finished compiler/bootstrap/translation                     5h35m04s  26GB
Dec 02 16:36:34 Starting unverified/sexpr-bootstrap/x64/64
Dec 02 17:01:04 Finished unverified/sexpr-bootstrap/x64/64                    24m26s   9GB
Dec 02 17:01:04 Starting unverified/sexpr-bootstrap/x64/32
Dec 02 17:22:02 Finished unverified/sexpr-bootstrap/x64/32                    20m53s   8GB
Dec 02 17:22:02 Starting compiler/benchmarks
Dec 02 17:22:07 Finished compiler/benchmarks                                      4s  34MB
Dec 02 17:22:07 Starting compiler/bootstrap/compilation/x64/64
Dec 03 19:57:32 Finished compiler/bootstrap/compilation/x64/64             26h35m21s  79GB
Dec 03 19:57:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 03 20:02:09 Finished compiler/bootstrap/compilation/x64/64/proofs          4m36s  16GB
Dec 03 20:02:09 Starting compiler/bootstrap/compilation/x64/32
Dec 04 18:20:01 Finished compiler/bootstrap/compilation/x64/32             22h17m48s  87GB
Dec 04 18:20:01 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 04 18:24:24 Finished compiler/bootstrap/compilation/x64/32/proofs          4m22s  13GB
Dec 04 18:24:24 Starting compiler/bootstrap/compilation/ag32/32
Dec 05 20:16:45 Finished compiler/bootstrap/compilation/ag32/32            25h52m19s 108GB
Dec 05 20:16:45 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 05 20:51:30 Finished compiler/bootstrap/compilation/ag32/32/proofs        34m44s  18GB
Dec 05 20:51:30 SUCCESS