Job 1025

CakeML:7e2dacbb4c75091492762a0d07079ac4749c1e8d
  Merge pull request #686 from CakeML/basis-hashtable [Sep 02 06:41:01]
HOL:c740f09eb04a009a28dd954cd0dc4afb18de273d
  Make a number of theorems about real$abs automatic rewrites [Aug 30 01:40:11]
Machine:brain08 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

Sep 02 06:41:58 Claimed job
Sep 02 06:42:03 Building HOL
Sep 02 06:58:54 Starting developers
Sep 02 06:59:00 Finished developers                                               5s 107MB
Sep 02 06:59:00 Starting developers/bin
Sep 02 06:59:11 Finished developers/bin                                          10s 971MB
Sep 02 06:59:11 Starting semantics/ffi
Sep 02 07:00:24 Finished semantics/ffi                                         1m12s 683MB
Sep 02 07:00:24 Starting semantics
Sep 02 07:03:16 Finished semantics                                             2m51s   1GB
Sep 02 07:03:17 Starting semantics/proofs
Sep 02 07:08:59 Finished semantics/proofs                                      5m41s   1GB
Sep 02 07:08:59 Starting semantics/alt_semantics
Sep 02 07:09:13 Finished semantics/alt_semantics                                 13s 324MB
Sep 02 07:09:13 Starting semantics/alt_semantics/proofs
Sep 02 07:12:42 Finished semantics/alt_semantics/proofs                        3m28s   1GB
Sep 02 07:12:42 Starting basis/pure
Sep 02 07:19:28 Finished basis/pure                                            6m45s 789MB
Sep 02 07:19:28 Starting translator
Sep 02 07:22:39 Finished translator                                            3m11s   1GB
Sep 02 07:22:39 Starting compiler/parsing
Sep 02 07:24:23 Finished compiler/parsing                                      1m43s   2GB
Sep 02 07:24:24 Starting characteristic
Sep 02 07:34:26 Finished characteristic                                       10m02s   2GB
Sep 02 07:34:27 Starting translator/monadic
Sep 02 07:37:15 Finished translator/monadic                                    2m47s   1GB
Sep 02 07:37:15 Starting basis
Sep 02 08:12:10 Finished basis                                                34m55s   3GB
Sep 02 08:12:10 Starting compiler/inference
Sep 02 08:15:45 Finished compiler/inference                                    3m34s   1GB
Sep 02 08:15:45 Starting compiler/backend/reg_alloc
Sep 02 08:17:22 Finished compiler/backend/reg_alloc                            1m36s   1GB
Sep 02 08:17:22 Starting compiler/backend/gc
Sep 02 08:33:46 Finished compiler/backend/gc                                  16m24s   2GB
Sep 02 08:33:47 Starting compiler/backend
Sep 02 08:33:49 Finished compiler/backend                                         2s  29MB
Sep 02 08:33:49 Starting compiler/encoders/asm
Sep 02 08:33:51 Finished compiler/encoders/asm                                    1s  26MB
Sep 02 08:33:51 Starting compiler/encoders/x64
Sep 02 08:35:50 Finished compiler/encoders/x64                                 1m58s 949MB
Sep 02 08:35:50 Starting compiler/encoders/arm7
Sep 02 08:39:10 Finished compiler/encoders/arm7                                3m20s   1GB
Sep 02 08:39:11 Starting compiler/encoders/arm8
Sep 02 08:40:10 Finished compiler/encoders/arm8                                  58s 590MB
Sep 02 08:40:10 Starting compiler/encoders/mips
Sep 02 08:42:22 Finished compiler/encoders/mips                                2m11s   1GB
Sep 02 08:42:22 Starting compiler/encoders/riscv
Sep 02 08:44:52 Finished compiler/encoders/riscv                               2m29s 827MB
Sep 02 08:44:52 Starting compiler/encoders/ag32
Sep 02 08:45:23 Finished compiler/encoders/ag32                                  31s 555MB
Sep 02 08:45:24 Starting compiler/backend/x64
Sep 02 08:45:57 Finished compiler/backend/x64                                    32s   1GB
Sep 02 08:45:57 Starting compiler/backend/arm7
Sep 02 08:46:32 Finished compiler/backend/arm7                                   35s   1GB
Sep 02 08:46:32 Starting compiler/backend/arm8
Sep 02 08:47:07 Finished compiler/backend/arm8                                   35s   1GB
Sep 02 08:47:08 Starting compiler/backend/mips
Sep 02 08:47:44 Finished compiler/backend/mips                                   36s   1GB
Sep 02 08:47:44 Starting compiler/backend/riscv
Sep 02 08:48:20 Finished compiler/backend/riscv                                  36s   1GB
Sep 02 08:48:20 Starting compiler/backend/ag32
Sep 02 08:50:24 Finished compiler/backend/ag32                                 2m03s   1GB
Sep 02 08:50:24 Starting compiler/parsing/proofs
Sep 02 09:00:51 Finished compiler/parsing/proofs                              10m26s   1GB
Sep 02 09:00:51 Starting compiler/inference/proofs
Sep 02 09:06:11 Finished compiler/inference/proofs                             5m19s   1GB
Sep 02 09:06:11 Starting compiler/backend/semantics
Sep 02 09:16:26 Finished compiler/backend/semantics                           10m14s   1GB
Sep 02 09:16:27 Starting compiler/backend/reg_alloc/proofs
Sep 02 09:23:00 Finished compiler/backend/reg_alloc/proofs                     6m33s 862MB
Sep 02 09:23:00 Starting compiler/backend/proofs
Sep 02 10:30:26 Finished compiler/backend/proofs                            1h07m25s   4GB
Sep 02 10:30:27 Starting compiler/encoders/x64/proofs
Sep 02 10:49:29 Finished compiler/encoders/x64/proofs                         19m01s   4GB
Sep 02 10:49:29 Starting compiler/encoders/arm7/proofs
Sep 02 11:15:36 Finished compiler/encoders/arm7/proofs                        26m07s   6GB
Sep 02 11:15:37 Starting compiler/encoders/arm8/proofs
Sep 02 11:28:26 Finished compiler/encoders/arm8/proofs                        12m49s   1GB
Sep 02 11:28:27 Starting compiler/encoders/mips/proofs
Sep 02 11:47:41 Finished compiler/encoders/mips/proofs                        19m14s   3GB
Sep 02 11:47:41 Starting compiler/encoders/riscv/proofs
Sep 02 12:03:48 Finished compiler/encoders/riscv/proofs                       16m06s   1GB
Sep 02 12:03:48 Starting compiler/encoders/ag32/proofs
Sep 02 12:08:33 Finished compiler/encoders/ag32/proofs                         4m44s 802MB
Sep 02 12:08:33 Starting compiler/backend/x64/proofs
Sep 02 12:09:08 Finished compiler/backend/x64/proofs                             34s   1GB
Sep 02 12:09:08 Starting compiler/backend/arm7/proofs
Sep 02 12:09:44 Finished compiler/backend/arm7/proofs                            35s 861MB
Sep 02 12:09:44 Starting compiler/backend/arm8/proofs
Sep 02 12:10:18 Finished compiler/backend/arm8/proofs                            33s   1GB
Sep 02 12:10:18 Starting compiler/backend/mips/proofs
Sep 02 12:10:54 Finished compiler/backend/mips/proofs                            36s   1GB
Sep 02 12:10:55 Starting compiler/backend/riscv/proofs
Sep 02 12:11:29 Finished compiler/backend/riscv/proofs                           34s   1GB
Sep 02 12:11:29 Starting compiler/backend/ag32/proofs
Sep 02 12:28:21 Finished compiler/backend/ag32/proofs                         16m51s   2GB
Sep 02 12:28:21 Starting compiler/proofs
Sep 02 12:30:41 Finished compiler/proofs                                       2m19s   2GB
Sep 02 12:30:41 Starting candle/set-theory
Sep 02 12:31:27 Finished candle/set-theory                                       46s 918MB
Sep 02 12:31:28 Starting candle/syntax-lib
Sep 02 12:31:47 Finished candle/syntax-lib                                       18s 666MB
Sep 02 12:31:47 Starting candle/standard/syntax
Sep 02 12:34:59 Finished candle/standard/syntax                                3m11s   1GB
Sep 02 12:34:59 Starting candle/standard/semantics
Sep 02 12:38:04 Finished candle/standard/semantics                             3m04s   1GB
Sep 02 12:38:04 Starting candle/standard/monadic
Sep 02 12:41:00 Finished candle/standard/monadic                               2m55s   1GB
Sep 02 12:41:00 Starting candle/standard/ml_kernel
Sep 02 12:48:04 Finished candle/standard/ml_kernel                             7m04s   3GB
Sep 02 12:48:04 Starting candle/standard/opentheory
Sep 02 13:03:50 Finished candle/standard/opentheory                           15m45s   4GB
Sep 02 13:03:51 Starting candle/standard/opentheory/compilation
Sep 02 13:57:19 Finished candle/standard/opentheory/compilation               53m28s  16GB
Sep 02 13:57:19 Starting candle/standard/opentheory/compilation/proofs
Sep 02 13:58:41 Finished candle/standard/opentheory/compilation/proofs         1m21s   2GB
Sep 02 13:58:42 Starting characteristic/examples
Sep 02 14:01:30 Finished characteristic/examples                               2m48s   2GB
Sep 02 14:01:30 Starting tutorial/solutions
Sep 02 14:26:19 Finished tutorial/solutions                                   24m48s   7GB
Sep 02 14:26:20 Starting translator/monadic/examples
Sep 02 14:30:47 Finished translator/monadic/examples                           4m27s   2GB
Sep 02 14:30:47 Starting examples
Sep 02 14:44:01 Finished examples                                             13m13s   3GB
Sep 02 14:44:01 Starting examples/compilation/x64
Sep 02 18:32:33 Finished examples/compilation/x64                           3h48m31s  19GB
Sep 02 18:32:33 Starting examples/compilation/x64/proofs
Sep 02 18:35:07 Finished examples/compilation/x64/proofs                       2m34s   2GB
Sep 02 18:35:08 Starting examples/compilation/ag32
Sep 02 19:28:27 Finished examples/compilation/ag32                            53m19s   5GB
Sep 02 19:28:27 Starting examples/compilation/ag32/proofs
Sep 02 19:29:53 Finished examples/compilation/ag32/proofs                      1m25s   3GB
Sep 02 19:29:54 Starting translator/okasaki-examples
Sep 02 19:37:03 Finished translator/okasaki-examples                           7m09s   1GB
Sep 02 19:37:04 Starting translator/other-examples
Sep 02 19:43:41 Finished translator/other-examples                             6m37s   1GB
Sep 02 19:43:42 Starting compiler/parsing/tests
Sep 02 19:44:28 Finished compiler/parsing/tests                                  46s 645MB
Sep 02 19:44:28 Starting compiler/inference/tests
Sep 02 19:51:37 Finished compiler/inference/tests                              7m09s   3GB
Sep 02 19:51:37 Starting compiler/bootstrap/translation
Sep 03 00:31:19 Finished compiler/bootstrap/translation                     4h39m41s  59GB
Sep 03 00:31:19 Starting unverified/sexpr-bootstrap/x64/64
Sep 03 00:52:24 Finished unverified/sexpr-bootstrap/x64/64                    21m03s   5GB
Sep 03 00:52:24 Starting unverified/sexpr-bootstrap/x64/32
Sep 03 01:08:09 Finished unverified/sexpr-bootstrap/x64/32                    15m44s   5GB
Sep 03 01:08:10 Starting compiler/benchmarks
Sep 03 01:40:51 Finished compiler/benchmarks                                  32m41s   2GB
Sep 03 01:40:51 Starting compiler/bootstrap/compilation/x64/64
Sep 04 10:18:03 Finished compiler/bootstrap/compilation/x64/64             32h37m09s 349GB
Sep 04 10:18:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 04 10:22:24 Finished compiler/bootstrap/compilation/x64/64/proofs          4m20s  10GB
Sep 04 10:22:24 Starting compiler/bootstrap/compilation/x64/32
Sep 05 12:54:34 Finished compiler/bootstrap/compilation/x64/32             26h32m08s 225GB
Sep 05 12:54:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 05 12:58:23 Finished compiler/bootstrap/compilation/x64/32/proofs          3m48s  10GB
Sep 05 12:58:23 Starting compiler/bootstrap/compilation/ag32/32
Sep 06 17:47:53 Finished compiler/bootstrap/compilation/ag32/32            28h49m29s 253GB
Sep 06 17:47:53 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 06 18:10:06 Finished compiler/bootstrap/compilation/ag32/32/proofs        22m13s  29GB
Sep 06 18:10:06 SUCCESS