Job 1518

CakeML:c39f0f7c5f4e94fa52bd30f8df07e7901b9f3dcc
  Merge pull request #826 from CakeML/double_from_string [May 02 20:39:10]
HOL:42c6babbdc8d94d05727b183c188c11aefdbcd80
  Revise name-carrying FOL system to have explicit "weakening" option [May 04 07:07:23]
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

May 06 07:34:06 Claimed job
May 06 07:34:13 Building HOL
May 06 07:49:01 Starting developers
May 06 07:49:02 Finished developers                                               0s  35MB
May 06 07:49:02 Starting developers/bin
May 06 07:49:08 Finished developers/bin                                           5s   1GB
May 06 07:49:08 Starting semantics/ffi
May 06 07:49:18 Finished semantics/ffi                                            9s 296MB
May 06 07:49:18 Starting semantics
May 06 07:50:51 Finished semantics                                             1m32s   1GB
May 06 07:50:51 Starting semantics/proofs
May 06 07:54:23 Finished semantics/proofs                                      3m30s   1GB
May 06 07:54:23 Starting semantics/alt_semantics
May 06 07:54:31 Finished semantics/alt_semantics                                  8s 433MB
May 06 07:54:31 Starting semantics/alt_semantics/proofs
May 06 07:56:43 Finished semantics/alt_semantics/proofs                        2m11s   1GB
May 06 07:56:43 Starting basis/pure
May 06 07:59:23 Finished basis/pure                                            2m40s   1GB
May 06 07:59:24 Starting translator
May 06 08:02:42 Finished translator                                            3m17s   2GB
May 06 08:02:42 Starting compiler/parsing
May 06 08:03:49 Finished compiler/parsing                                      1m07s   4GB
May 06 08:03:49 Starting characteristic
May 06 08:09:25 Finished characteristic                                        5m35s   3GB
May 06 08:09:25 Starting translator/monadic
May 06 08:11:12 Finished translator/monadic                                    1m46s   3GB
May 06 08:11:12 Starting basis
May 06 08:55:08 Finished basis                                                43m55s  29GB
May 06 08:55:08 Starting compiler/inference
May 06 08:56:21 Finished compiler/inference                                    1m12s   2GB
May 06 08:56:21 Starting compiler/backend/reg_alloc
May 06 08:57:27 Finished compiler/backend/reg_alloc                            1m06s   1GB
May 06 08:57:28 Starting compiler/backend/gc
May 06 09:01:04 Finished compiler/backend/gc                                   3m36s   4GB
May 06 09:01:04 Starting compiler/backend
May 06 09:06:09 Finished compiler/backend                                      5m04s   5GB
May 06 09:06:09 Starting compiler/encoders/asm
May 06 09:06:32 Finished compiler/encoders/asm                                   22s   1GB
May 06 09:06:32 Starting compiler/encoders/x64
May 06 09:07:34 Finished compiler/encoders/x64                                 1m02s   1GB
May 06 09:07:34 Starting compiler/encoders/arm7
May 06 09:09:37 Finished compiler/encoders/arm7                                2m02s   1GB
May 06 09:09:38 Starting compiler/encoders/arm8
May 06 09:10:17 Finished compiler/encoders/arm8                                  39s   1GB
May 06 09:10:17 Starting compiler/encoders/mips
May 06 09:11:44 Finished compiler/encoders/mips                                1m26s   1GB
May 06 09:11:45 Starting compiler/encoders/riscv
May 06 09:13:21 Finished compiler/encoders/riscv                               1m36s   1GB
May 06 09:13:21 Starting compiler/encoders/ag32
May 06 09:13:40 Finished compiler/encoders/ag32                                  18s 974MB
May 06 09:13:40 Starting compiler/backend/x64
May 06 09:14:00 Finished compiler/backend/x64                                    20s   1GB
May 06 09:14:01 Starting compiler/backend/arm7
May 06 09:14:22 Finished compiler/backend/arm7                                   20s   1GB
May 06 09:14:22 Starting compiler/backend/arm8
May 06 09:14:42 Finished compiler/backend/arm8                                   20s   1GB
May 06 09:14:42 Starting compiler/backend/mips
May 06 09:15:02 Finished compiler/backend/mips                                   19s   1GB
May 06 09:15:03 Starting compiler/backend/riscv
May 06 09:15:24 Finished compiler/backend/riscv                                  21s   1GB
May 06 09:15:24 Starting compiler/backend/ag32
May 06 09:16:34 Finished compiler/backend/ag32                                 1m09s   2GB
May 06 09:16:34 Starting compiler/parsing/proofs
May 06 09:22:25 Finished compiler/parsing/proofs                               5m50s   2GB
May 06 09:22:25 Starting compiler/inference/proofs
May 06 09:24:58 Finished compiler/inference/proofs                             2m32s   2GB
May 06 09:24:58 Starting compiler/backend/semantics
May 06 09:51:57 Finished compiler/backend/semantics                           26m59s   4GB
May 06 09:51:58 Starting compiler/backend/reg_alloc/proofs
May 06 09:55:17 Finished compiler/backend/reg_alloc/proofs                     3m19s   1GB
May 06 09:55:17 Starting compiler/backend/proofs
May 06 10:48:50 Finished compiler/backend/proofs                              53m32s  16GB
May 06 10:48:50 Starting compiler/encoders/x64/proofs
May 06 10:58:18 Finished compiler/encoders/x64/proofs                          9m27s   6GB
May 06 10:58:18 Starting compiler/encoders/arm7/proofs
May 06 11:11:00 Finished compiler/encoders/arm7/proofs                        12m41s   9GB
May 06 11:11:00 Starting compiler/encoders/arm8/proofs
May 06 11:17:38 Finished compiler/encoders/arm8/proofs                         6m37s   3GB
May 06 11:17:38 Starting compiler/encoders/mips/proofs
May 06 11:27:23 Finished compiler/encoders/mips/proofs                         9m44s   5GB
May 06 11:27:23 Starting compiler/encoders/riscv/proofs
May 06 11:35:42 Finished compiler/encoders/riscv/proofs                        8m18s   4GB
May 06 11:35:42 Starting compiler/encoders/ag32/proofs
May 06 11:38:02 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
May 06 11:38:02 Starting compiler/backend/x64/proofs
May 06 11:38:25 Finished compiler/backend/x64/proofs                             22s   2GB
May 06 11:38:25 Starting compiler/backend/arm7/proofs
May 06 11:38:48 Finished compiler/backend/arm7/proofs                            23s   1GB
May 06 11:38:48 Starting compiler/backend/arm8/proofs
May 06 11:39:10 Finished compiler/backend/arm8/proofs                            21s   1GB
May 06 11:39:10 Starting compiler/backend/mips/proofs
May 06 11:39:33 Finished compiler/backend/mips/proofs                            22s   1GB
May 06 11:39:33 Starting compiler/backend/riscv/proofs
May 06 11:39:56 Finished compiler/backend/riscv/proofs                           22s   2GB
May 06 11:39:56 Starting compiler/backend/ag32/proofs
May 06 11:52:01 Finished compiler/backend/ag32/proofs                         12m04s   5GB
May 06 11:52:01 Starting compiler/proofs
May 06 11:53:59 Finished compiler/proofs                                       1m57s   6GB
May 06 11:53:59 Starting candle/set-theory
May 06 11:54:28 Finished candle/set-theory                                       28s 928MB
May 06 11:54:28 Starting candle/syntax-lib
May 06 11:54:40 Finished candle/syntax-lib                                       11s 799MB
May 06 11:54:40 Starting candle/standard/syntax
May 06 11:56:33 Finished candle/standard/syntax                                1m52s   1GB
May 06 11:56:33 Starting candle/standard/semantics
May 06 11:58:21 Finished candle/standard/semantics                             1m46s   2GB
May 06 11:58:21 Starting candle/standard/monadic
May 06 12:00:03 Finished candle/standard/monadic                               1m41s   2GB
May 06 12:00:03 Starting candle/standard/ml_kernel
May 06 12:05:32 Finished candle/standard/ml_kernel                             5m28s   5GB
May 06 12:05:32 Starting candle/overloading/syntax
May 06 12:08:41 Finished candle/overloading/syntax                             3m09s   2GB
May 06 12:08:42 Starting candle/overloading/semantics
May 06 12:20:44 Finished candle/overloading/semantics                         12m02s   8GB
May 06 12:20:44 Starting characteristic/examples
May 06 12:22:04 Finished characteristic/examples                               1m19s   4GB
May 06 12:22:04 Starting tutorial/solutions
May 06 12:37:27 Finished tutorial/solutions                                   15m22s  11GB
May 06 12:37:27 Starting translator/monadic/examples
May 06 12:40:51 Finished translator/monadic/examples                           3m24s   4GB
May 06 12:40:51 Starting examples
May 06 12:49:48 Finished examples                                              8m56s   6GB
May 06 12:49:48 Starting examples/compilation/x64
May 06 15:13:35 Finished examples/compilation/x64                           2h23m46s  20GB
May 06 15:13:35 Starting examples/compilation/x64/proofs
May 06 15:15:36 Finished examples/compilation/x64/proofs                       2m00s   3GB
May 06 15:15:36 Starting examples/compilation/ag32
May 06 15:49:38 Finished examples/compilation/ag32                            34m01s  12GB
May 06 15:49:38 Starting examples/compilation/ag32/proofs
May 06 15:50:29 Finished examples/compilation/ag32/proofs                        50s   5GB
May 06 15:50:29 Starting examples/cost
May 06 16:46:08 Finished examples/cost                                        55m38s  13GB
May 06 16:46:08 Starting examples/lpr_checker
May 06 16:50:05 Finished examples/lpr_checker                                  3m56s   6GB
May 06 16:50:05 Starting examples/lpr_checker/compilation
May 06 17:08:47 Finished examples/lpr_checker/compilation                     18m41s  16GB
May 06 17:08:47 Starting examples/lpr_checker/compilation/proofs
May 06 17:09:33 Finished examples/lpr_checker/compilation/proofs                 45s   4GB
May 06 17:09:33 Starting examples/lpr_checker/array
May 06 17:23:20 Finished examples/lpr_checker/array                           13m46s   5GB
May 06 17:23:20 Starting examples/lpr_checker/array/compilation
May 06 17:43:29 Finished examples/lpr_checker/array/compilation               20m08s  20GB
May 06 17:43:29 Starting examples/lpr_checker/array/compilation/proofs
May 06 17:44:20 Finished examples/lpr_checker/array/compilation/proofs           51s   5GB
May 06 17:44:21 Starting examples/opentheory
May 06 17:53:58 Finished examples/opentheory                                   9m37s   5GB
May 06 17:53:58 Starting examples/opentheory
May 06 17:53:59 Finished examples/opentheory                                      0s 100MB
May 06 17:53:59 Starting examples/opentheory/compilation
May 06 18:25:58 Finished examples/opentheory/compilation                      31m58s  26GB
May 06 18:25:58 Starting examples/opentheory/compilation/proofs
May 06 18:26:44 Finished examples/opentheory/compilation/proofs                  46s   4GB
May 06 18:26:45 Starting examples/opentheory/compilation/ag32
May 06 18:58:41 Finished examples/opentheory/compilation/ag32                 31m56s  25GB
May 06 18:58:41 Starting examples/opentheory/compilation/ag32/proofs
May 06 19:00:18 Finished examples/opentheory/compilation/ag32/proofs           1m36s   9GB
May 06 19:00:18 Starting translator/okasaki-examples
May 06 19:04:43 Finished translator/okasaki-examples                           4m24s   3GB
May 06 19:04:43 Starting translator/other-examples
May 06 19:06:44 Finished translator/other-examples                             2m00s   2GB
May 06 19:06:44 Starting compiler/parsing/tests
May 06 19:07:09 Finished compiler/parsing/tests                                  24s 656MB
May 06 19:07:09 Starting compiler/inference/tests
May 06 19:14:37 Finished compiler/inference/tests                              7m27s   6GB
May 06 19:14:38 Starting compiler/bootstrap/translation
May 06 21:43:53 Finished compiler/bootstrap/translation                     2h29m14s  55GB
May 06 21:43:53 Starting unverified/sexpr-bootstrap/x64/64
May 06 21:56:09 Finished unverified/sexpr-bootstrap/x64/64                    12m11s   8GB
May 06 21:56:09 Starting unverified/sexpr-bootstrap/x64/32
May 06 22:06:40 Finished unverified/sexpr-bootstrap/x64/32                    10m27s   8GB
May 06 22:06:40 Starting compiler/benchmarks
May 06 22:44:31 Finished compiler/benchmarks                                  37m48s   2GB
May 06 22:44:33 Starting compiler/bootstrap/compilation/x64/64
May 07 16:39:44 Finished compiler/bootstrap/compilation/x64/64             17h55m07s  64GB
May 07 16:39:44 Starting compiler/bootstrap/compilation/x64/64/proofs
May 07 16:41:57 Finished compiler/bootstrap/compilation/x64/64/proofs          2m13s  16GB
May 07 16:41:57 Starting compiler/bootstrap/compilation/x64/32
May 08 09:39:48 Finished compiler/bootstrap/compilation/x64/32             16h57m46s  63GB
May 08 09:39:48 Starting compiler/bootstrap/compilation/x64/32/proofs
May 08 09:42:04 Finished compiler/bootstrap/compilation/x64/32/proofs          2m15s  14GB
May 08 09:42:04 Starting compiler/bootstrap/compilation/ag32/32
May 09 02:06:48 Finished compiler/bootstrap/compilation/ag32/32            16h24m43s  64GB
May 09 02:06:48 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 09 02:16:26 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m37s  56GB
May 09 02:16:26 SUCCESS