Job 811

CakeML:ccd4671556758a3ad5ce925a7688e8618e915248
  Merge pull request #630 from talsewell/compute-thmset [Apr 20 03:03:19]
HOL:057a3046e41b50db616e5d385e9b63e940b4957e
  Deal with bad rebindings of theorems under src/ [Apr 15 07:09:08]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Apr 21 00:10:33 Claimed job
Apr 21 00:10:36 Reusing HOL
Apr 21 00:10:40 Starting developers
Apr 21 00:10:41 Finished developers                                               0s  21MB
Apr 21 00:10:41 Starting developers/bin
Apr 21 00:11:13 Finished developers/bin                                          31s 204MB
Apr 21 00:11:13 Starting semantics/ffi
Apr 21 00:11:22 Finished semantics/ffi                                            8s 221MB
Apr 21 00:11:22 Starting semantics
Apr 21 00:12:42 Finished semantics                                             1m19s   1GB
Apr 21 00:12:42 Starting semantics/proofs
Apr 21 00:15:38 Finished semantics/proofs                                      2m55s   1GB
Apr 21 00:15:38 Starting basis/pure
Apr 21 00:16:23 Finished basis/pure                                              43s 744MB
Apr 21 00:16:23 Starting translator
Apr 21 00:18:04 Finished translator                                            1m40s   1GB
Apr 21 00:18:04 Starting compiler/parsing
Apr 21 00:19:03 Finished compiler/parsing                                        58s   1GB
Apr 21 00:19:04 Starting characteristic
Apr 21 00:24:18 Finished characteristic                                        5m13s   1GB
Apr 21 00:24:18 Starting translator/monadic
Apr 21 00:25:44 Finished translator/monadic                                    1m25s   1GB
Apr 21 00:25:44 Starting basis
Apr 21 00:42:20 Finished basis                                                16m35s   3GB
Apr 21 00:42:20 Starting compiler/inference
Apr 21 00:43:52 Finished compiler/inference                                    1m31s   1GB
Apr 21 00:43:53 Starting compiler/backend/reg_alloc
Apr 21 00:44:44 Finished compiler/backend/reg_alloc                              51s   1GB
Apr 21 00:44:45 Starting compiler/backend/gc
Apr 21 00:52:49 Finished compiler/backend/gc                                   8m04s   2GB
Apr 21 00:52:49 Starting compiler/backend
Apr 21 00:52:51 Finished compiler/backend                                         0s  42MB
Apr 21 00:52:51 Starting compiler/encoders/asm
Apr 21 00:52:52 Finished compiler/encoders/asm                                    0s  32MB
Apr 21 00:52:52 Starting compiler/encoders/x64
Apr 21 00:53:15 Finished compiler/encoders/x64                                   22s 892MB
Apr 21 00:53:15 Starting compiler/encoders/arm6
Apr 21 00:54:01 Finished compiler/encoders/arm6                                  45s 681MB
Apr 21 00:54:01 Starting compiler/encoders/arm8
Apr 21 00:54:13 Finished compiler/encoders/arm8                                  11s 871MB
Apr 21 00:54:13 Starting compiler/encoders/mips
Apr 21 00:54:29 Finished compiler/encoders/mips                                  15s   1GB
Apr 21 00:54:30 Starting compiler/encoders/riscv
Apr 21 00:54:43 Finished compiler/encoders/riscv                                 13s 807MB
Apr 21 00:54:43 Starting compiler/encoders/ag32
Apr 21 00:54:59 Finished compiler/encoders/ag32                                  15s 637MB
Apr 21 00:54:59 Starting compiler/backend/x64
Apr 21 00:55:15 Finished compiler/backend/x64                                    15s   1GB
Apr 21 00:55:16 Starting compiler/backend/arm6
Apr 21 00:55:34 Finished compiler/backend/arm6                                   17s   1GB
Apr 21 00:55:34 Starting compiler/backend/arm8
Apr 21 00:55:50 Finished compiler/backend/arm8                                   15s   1GB
Apr 21 00:55:51 Starting compiler/backend/mips
Apr 21 00:56:07 Finished compiler/backend/mips                                   15s   1GB
Apr 21 00:56:08 Starting compiler/backend/riscv
Apr 21 00:56:24 Finished compiler/backend/riscv                                  15s   1GB
Apr 21 00:56:24 Starting compiler/backend/ag32
Apr 21 00:57:32 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 21 00:57:33 Starting compiler/parsing/proofs
Apr 21 01:03:08 Finished compiler/parsing/proofs                               5m35s 815MB
Apr 21 01:03:09 Starting compiler/inference/proofs
Apr 21 01:05:50 Finished compiler/inference/proofs                             2m41s 854MB
Apr 21 01:05:51 Starting compiler/backend/semantics
Apr 21 01:12:58 Finished compiler/backend/semantics                            7m06s   2GB
Apr 21 01:12:58 Starting compiler/backend/reg_alloc/proofs
Apr 21 01:15:38 Finished compiler/backend/reg_alloc/proofs                     2m39s   1GB
Apr 21 01:15:38 Starting compiler/backend/proofs
Apr 21 01:54:33 Finished compiler/backend/proofs                              38m54s   3GB
Apr 21 01:54:34 Starting compiler/encoders/x64/proofs
Apr 21 02:03:54 Finished compiler/encoders/x64/proofs                          9m20s   4GB
Apr 21 02:03:55 Starting compiler/encoders/arm6/proofs
Apr 21 02:16:16 Finished compiler/encoders/arm6/proofs                        12m20s   3GB
Apr 21 02:16:16 Starting compiler/encoders/arm8/proofs
Apr 21 02:21:57 Finished compiler/encoders/arm8/proofs                         5m39s   1GB
Apr 21 02:21:57 Starting compiler/encoders/mips/proofs
Apr 21 02:31:39 Finished compiler/encoders/mips/proofs                         9m42s   2GB
Apr 21 02:31:40 Starting compiler/encoders/riscv/proofs
Apr 21 02:40:11 Finished compiler/encoders/riscv/proofs                        8m31s   1GB
Apr 21 02:40:12 Starting compiler/encoders/ag32/proofs
Apr 21 02:42:38 Finished compiler/encoders/ag32/proofs                         2m26s 914MB
Apr 21 02:42:39 Starting compiler/backend/x64/proofs
Apr 21 02:42:56 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 21 02:42:56 Starting compiler/backend/arm6/proofs
Apr 21 02:43:16 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 21 02:43:16 Starting compiler/backend/arm8/proofs
Apr 21 02:43:32 Finished compiler/backend/arm8/proofs                            15s   1GB
Apr 21 02:43:32 Starting compiler/backend/mips/proofs
Apr 21 02:43:50 Finished compiler/backend/mips/proofs                            17s   1GB
Apr 21 02:43:51 Starting compiler/backend/riscv/proofs
Apr 21 02:44:08 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 21 02:44:08 Starting compiler/backend/ag32/proofs
Apr 21 02:53:21 Finished compiler/backend/ag32/proofs                          9m12s   2GB
Apr 21 02:53:21 Starting compiler/proofs
Apr 21 02:54:53 Finished compiler/proofs                                       1m30s   3GB
Apr 21 02:54:53 Starting candle/set-theory
Apr 21 02:55:19 Finished candle/set-theory                                       25s 812MB
Apr 21 02:55:19 Starting candle/syntax-lib
Apr 21 02:55:29 Finished candle/syntax-lib                                        9s 428MB
Apr 21 02:55:30 Starting candle/standard/syntax
Apr 21 02:57:13 Finished candle/standard/syntax                                1m42s   1GB
Apr 21 02:57:13 Starting candle/standard/semantics
Apr 21 02:58:48 Finished candle/standard/semantics                             1m34s   1GB
Apr 21 02:58:48 Starting candle/standard/monadic
Apr 21 03:00:22 Finished candle/standard/monadic                               1m33s   1GB
Apr 21 03:00:22 Starting candle/standard/ml_kernel
Apr 21 03:04:25 Finished candle/standard/ml_kernel                             4m01s   3GB
Apr 21 03:04:25 Starting candle/standard/opentheory
Apr 21 03:13:15 Finished candle/standard/opentheory                            8m49s   3GB
Apr 21 03:13:15 Starting candle/standard/opentheory/compilation
Apr 21 03:43:39 Finished candle/standard/opentheory/compilation               30m22s  13GB
Apr 21 03:43:39 Starting candle/standard/opentheory/compilation/proofs
Apr 21 03:44:14 Finished candle/standard/opentheory/compilation/proofs           34s   3GB
Apr 21 03:44:14 Starting characteristic/examples
Apr 21 03:45:39 Finished characteristic/examples                               1m24s   2GB
Apr 21 03:45:40 Starting tutorial/solutions
Apr 21 03:59:02 Finished tutorial/solutions                                   13m21s   6GB
Apr 21 03:59:03 Starting translator/monadic/examples
Apr 21 04:01:33 Finished translator/monadic/examples                           2m29s   1GB
Apr 21 04:01:33 Starting examples
Apr 21 04:10:26 Finished examples                                              8m52s   3GB
Apr 21 04:10:27 Starting examples/compilation/x64
Apr 21 06:05:08 Finished examples/compilation/x64                           1h54m40s  13GB
Apr 21 06:05:09 Starting examples/compilation/x64/proofs
Apr 21 06:06:35 Finished examples/compilation/x64/proofs                       1m25s   2GB
Apr 21 06:06:35 Starting examples/compilation/ag32
Apr 21 06:35:11 Finished examples/compilation/ag32                            28m34s   6GB
Apr 21 06:35:11 Starting examples/compilation/ag32/proofs
Apr 21 06:35:50 Finished examples/compilation/ag32/proofs                        38s   3GB
Apr 21 06:35:50 Starting translator/okasaki-examples
Apr 21 06:39:56 Finished translator/okasaki-examples                           4m05s   2GB
Apr 21 06:39:57 Starting translator/other-examples
Apr 21 06:40:38 Finished translator/other-examples                               40s   1GB
Apr 21 06:40:38 Starting compiler/parsing/tests
Apr 21 06:41:04 Finished compiler/parsing/tests                                  24s 552MB
Apr 21 06:41:04 Starting compiler/inference/tests
Apr 21 06:45:10 Finished compiler/inference/tests                              4m05s   5GB
Apr 21 06:45:10 Starting compiler/bootstrap/translation
Apr 21 13:26:49 Finished compiler/bootstrap/translation                     6h41m38s  44GB
Apr 21 13:26:49 Starting unverified/sexpr-bootstrap/x64/64
Apr 21 13:34:24 Finished unverified/sexpr-bootstrap/x64/64                     7m34s   7GB
Apr 21 13:34:25 Starting unverified/sexpr-bootstrap/x64/32
Apr 21 13:39:02 Finished unverified/sexpr-bootstrap/x64/32                     4m36s  11GB
Apr 21 13:39:02 Starting compiler/benchmarks
Apr 21 14:17:11 Finished compiler/benchmarks                                  38m08s   1GB
Apr 21 14:17:12 Starting compiler/bootstrap/compilation/x64/64
Apr 22 00:50:20 Finished compiler/bootstrap/compilation/x64/64             10h33m07s  63GB
Apr 22 00:50:21 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 22 00:53:16 Finished compiler/bootstrap/compilation/x64/64/proofs          2m55s  11GB
Apr 22 00:53:17 Starting compiler/bootstrap/compilation/x64/32
Apr 22 10:19:26 Finished compiler/bootstrap/compilation/x64/32              9h26m08s  64GB
Apr 22 10:19:26 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 22 10:22:42 Finished compiler/bootstrap/compilation/x64/32/proofs          3m15s   6GB
Apr 22 10:22:42 Starting compiler/bootstrap/compilation/ag32/32
Apr 22 20:09:41 Finished compiler/bootstrap/compilation/ag32/32             9h46m58s  64GB
Apr 22 20:09:41 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 22 20:33:01 Finished compiler/bootstrap/compilation/ag32/32/proofs        23m19s  14GB
Apr 22 20:33:01 SUCCESS