Job 1536

CakeML:e186cc1984bac5cce7c150b458fe1604eece7703
  Fix cost examples [May 21 07:35:10]
HOL:dd71488a8337c0869382eafe18515017f1f40b0b
  Redefine REAL_SUM_IMAGE based on iterateTheory (now moved to src/real [May 23 23:04:04]
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 26 07:06:07 Claimed job
May 26 07:06:15 Building HOL
May 26 07:20:44 Starting developers
May 26 07:20:46 Finished developers                                               2s 122MB
May 26 07:20:46 Starting developers/bin
May 26 07:20:53 Finished developers/bin                                           6s   1GB
May 26 07:20:53 Starting semantics/ffi
May 26 07:21:03 Finished semantics/ffi                                           10s 268MB
May 26 07:21:04 Starting semantics
May 26 07:22:39 Finished semantics                                             1m35s   1GB
May 26 07:22:39 Starting semantics/proofs
May 26 07:26:15 Finished semantics/proofs                                      3m35s   1GB
May 26 07:26:16 Starting semantics/alt_semantics
May 26 07:26:24 Finished semantics/alt_semantics                                  8s 424MB
May 26 07:26:25 Starting semantics/alt_semantics/proofs
May 26 07:28:43 Finished semantics/alt_semantics/proofs                        2m18s   1GB
May 26 07:28:43 Starting basis/pure
May 26 07:31:27 Finished basis/pure                                            2m43s   1GB
May 26 07:31:28 Starting translator
May 26 07:35:17 Finished translator                                            3m49s   2GB
May 26 07:35:17 Starting compiler/parsing
May 26 07:36:45 Finished compiler/parsing                                      1m27s   4GB
May 26 07:36:45 Starting characteristic
May 26 07:43:01 Finished characteristic                                        6m15s   3GB
May 26 07:43:02 Starting translator/monadic
May 26 07:45:09 Finished translator/monadic                                    2m06s   2GB
May 26 07:45:09 Starting basis
May 26 08:34:24 Finished basis                                                49m15s  27GB
May 26 08:34:24 Starting compiler/inference
May 26 08:35:39 Finished compiler/inference                                    1m14s   2GB
May 26 08:35:39 Starting compiler/backend/reg_alloc
May 26 08:36:47 Finished compiler/backend/reg_alloc                            1m08s   2GB
May 26 08:36:47 Starting compiler/backend/gc
May 26 08:40:34 Finished compiler/backend/gc                                   3m46s   3GB
May 26 08:40:34 Starting compiler/backend
May 26 08:45:52 Finished compiler/backend                                      5m17s   5GB
May 26 08:45:53 Starting compiler/encoders/asm
May 26 08:46:16 Finished compiler/encoders/asm                                   23s   1GB
May 26 08:46:16 Starting compiler/encoders/x64
May 26 08:47:21 Finished compiler/encoders/x64                                 1m04s   1GB
May 26 08:47:22 Starting compiler/encoders/arm7
May 26 08:49:27 Finished compiler/encoders/arm7                                2m05s   1GB
May 26 08:49:27 Starting compiler/encoders/arm8
May 26 08:50:07 Finished compiler/encoders/arm8                                  39s   1GB
May 26 08:50:07 Starting compiler/encoders/mips
May 26 08:51:35 Finished compiler/encoders/mips                                1m27s   1GB
May 26 08:51:36 Starting compiler/encoders/riscv
May 26 08:53:18 Finished compiler/encoders/riscv                               1m42s   1GB
May 26 08:53:18 Starting compiler/encoders/ag32
May 26 08:53:38 Finished compiler/encoders/ag32                                  19s 939MB
May 26 08:53:38 Starting compiler/backend/x64
May 26 08:53:59 Finished compiler/backend/x64                                    20s   1GB
May 26 08:53:59 Starting compiler/backend/arm7
May 26 08:54:22 Finished compiler/backend/arm7                                   22s   1GB
May 26 08:54:22 Starting compiler/backend/arm8
May 26 08:54:43 Finished compiler/backend/arm8                                   20s   1GB
May 26 08:54:43 Starting compiler/backend/mips
May 26 08:55:05 Finished compiler/backend/mips                                   21s   1GB
May 26 08:55:05 Starting compiler/backend/riscv
May 26 08:55:27 Finished compiler/backend/riscv                                  21s   1GB
May 26 08:55:27 Starting compiler/backend/ag32
May 26 08:56:40 Finished compiler/backend/ag32                                 1m13s   1GB
May 26 08:56:41 Starting compiler/parsing/proofs
May 26 09:02:32 Finished compiler/parsing/proofs                               5m51s   2GB
May 26 09:02:32 Starting compiler/inference/proofs
May 26 09:05:11 Finished compiler/inference/proofs                             2m38s   2GB
May 26 09:05:11 Starting compiler/backend/semantics
May 26 09:33:04 Finished compiler/backend/semantics                           27m52s   6GB
May 26 09:33:04 Starting compiler/backend/reg_alloc/proofs
May 26 09:36:27 Finished compiler/backend/reg_alloc/proofs                     3m22s   1GB
May 26 09:36:28 Starting compiler/backend/proofs
May 26 10:31:49 Finished compiler/backend/proofs                              55m21s  29GB
May 26 10:31:50 Starting compiler/encoders/x64/proofs
May 26 10:41:08 Finished compiler/encoders/x64/proofs                          9m18s   5GB
May 26 10:41:08 Starting compiler/encoders/arm7/proofs
May 26 10:53:55 Finished compiler/encoders/arm7/proofs                        12m46s   8GB
May 26 10:53:55 Starting compiler/encoders/arm8/proofs
May 26 11:00:21 Finished compiler/encoders/arm8/proofs                         6m25s   4GB
May 26 11:00:22 Starting compiler/encoders/mips/proofs
May 26 11:10:14 Finished compiler/encoders/mips/proofs                         9m51s   7GB
May 26 11:10:14 Starting compiler/encoders/riscv/proofs
May 26 11:18:36 Finished compiler/encoders/riscv/proofs                        8m22s   3GB
May 26 11:18:36 Starting compiler/encoders/ag32/proofs
May 26 11:20:57 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
May 26 11:20:57 Starting compiler/backend/x64/proofs
May 26 11:21:20 Finished compiler/backend/x64/proofs                             22s   2GB
May 26 11:21:20 Starting compiler/backend/arm7/proofs
May 26 11:21:44 Finished compiler/backend/arm7/proofs                            23s   2GB
May 26 11:21:45 Starting compiler/backend/arm8/proofs
May 26 11:22:06 Finished compiler/backend/arm8/proofs                            21s   1GB
May 26 11:22:06 Starting compiler/backend/mips/proofs
May 26 11:22:29 Finished compiler/backend/mips/proofs                            22s   1GB
May 26 11:22:30 Starting compiler/backend/riscv/proofs
May 26 11:22:52 Finished compiler/backend/riscv/proofs                           22s   2GB
May 26 11:22:53 Starting compiler/backend/ag32/proofs
May 26 11:35:09 Finished compiler/backend/ag32/proofs                         12m15s   6GB
May 26 11:35:09 Starting compiler/proofs
May 26 11:37:09 Finished compiler/proofs                                       1m59s   6GB
May 26 11:37:09 Starting candle/set-theory
May 26 11:37:40 Finished candle/set-theory                                       30s   1GB
May 26 11:37:40 Starting candle/syntax-lib
May 26 11:37:51 Finished candle/syntax-lib                                       10s 810MB
May 26 11:37:51 Starting candle/standard/syntax
May 26 11:39:44 Finished candle/standard/syntax                                1m52s   1GB
May 26 11:39:44 Starting candle/standard/semantics
May 26 11:41:31 Finished candle/standard/semantics                             1m46s   2GB
May 26 11:41:31 Starting candle/standard/monadic
May 26 11:43:12 Finished candle/standard/monadic                               1m41s   1GB
May 26 11:43:12 Starting candle/standard/ml_kernel
May 26 11:48:41 Finished candle/standard/ml_kernel                             5m28s   6GB
May 26 11:48:41 Starting candle/overloading/syntax
May 26 11:51:53 Finished candle/overloading/syntax                             3m11s   1GB
May 26 11:51:53 Starting candle/overloading/semantics
May 26 12:03:58 Finished candle/overloading/semantics                         12m04s   8GB
May 26 12:03:59 Starting characteristic/examples
May 26 12:05:19 Finished characteristic/examples                               1m20s   4GB
May 26 12:05:19 Starting tutorial/solutions
May 26 12:20:09 Finished tutorial/solutions                                   14m49s  10GB
May 26 12:20:09 Starting translator/monadic/examples
May 26 12:23:37 Finished translator/monadic/examples                           3m28s   4GB
May 26 12:23:38 Starting examples
May 26 12:32:37 Finished examples                                              8m59s   6GB
May 26 12:32:37 Starting examples/compilation/x64
May 26 14:56:19 Finished examples/compilation/x64                           2h23m41s  30GB
May 26 14:56:19 Starting examples/compilation/x64/proofs
May 26 14:58:23 Finished examples/compilation/x64/proofs                       2m03s   3GB
May 26 14:58:23 Starting examples/compilation/ag32
May 26 15:32:44 Finished examples/compilation/ag32                            34m20s  12GB
May 26 15:32:44 Starting examples/compilation/ag32/proofs
May 26 15:33:37 Finished examples/compilation/ag32/proofs                        53s   4GB
May 26 15:33:38 Starting examples/cost
May 26 16:29:34 Finished examples/cost                                        55m55s  14GB
May 26 16:29:34 Starting examples/lpr_checker
May 26 16:33:27 Finished examples/lpr_checker                                  3m52s   3GB
May 26 16:33:27 Starting examples/lpr_checker/compilation
May 26 16:52:35 Finished examples/lpr_checker/compilation                     19m07s  11GB
May 26 16:52:35 Starting examples/lpr_checker/compilation/proofs
May 26 16:53:19 Finished examples/lpr_checker/compilation/proofs                 43s   4GB
May 26 16:53:19 Starting examples/lpr_checker/array
May 26 17:07:07 Finished examples/lpr_checker/array                           13m47s   5GB
May 26 17:07:07 Starting examples/lpr_checker/array/compilation
May 26 17:27:03 Finished examples/lpr_checker/array/compilation               19m55s  22GB
May 26 17:27:03 Starting examples/lpr_checker/array/compilation/proofs
May 26 17:27:54 Finished examples/lpr_checker/array/compilation/proofs           50s   5GB
May 26 17:27:54 Starting examples/opentheory
May 26 17:37:26 Finished examples/opentheory                                   9m32s   3GB
May 26 17:37:26 Starting examples/opentheory
May 26 17:37:27 Finished examples/opentheory                                      0s  99MB
May 26 17:37:27 Starting examples/opentheory/compilation
May 26 18:09:50 Finished examples/opentheory/compilation                      32m22s  24GB
May 26 18:09:50 Starting examples/opentheory/compilation/proofs
May 26 18:10:36 Finished examples/opentheory/compilation/proofs                  45s   3GB
May 26 18:10:36 Starting examples/opentheory/compilation/ag32
May 26 18:43:49 Finished examples/opentheory/compilation/ag32                 33m12s  28GB
May 26 18:43:49 Starting examples/opentheory/compilation/ag32/proofs
May 26 18:45:25 Finished examples/opentheory/compilation/ag32/proofs           1m35s   9GB
May 26 18:45:25 Starting translator/okasaki-examples
May 26 18:49:48 Finished translator/okasaki-examples                           4m22s   2GB
May 26 18:49:48 Starting translator/other-examples
May 26 18:51:53 Finished translator/other-examples                             2m04s   2GB
May 26 18:51:53 Starting compiler/parsing/tests
May 26 18:52:18 Finished compiler/parsing/tests                                  24s 679MB
May 26 18:52:18 Starting compiler/inference/tests
May 26 18:59:41 Finished compiler/inference/tests                              7m23s   6GB
May 26 18:59:41 Starting compiler/bootstrap/translation
May 26 21:25:47 Finished compiler/bootstrap/translation                     2h26m05s  48GB
May 26 21:25:47 Starting unverified/sexpr-bootstrap/x64/64
May 26 21:38:05 Finished unverified/sexpr-bootstrap/x64/64                    12m12s   8GB
May 26 21:38:05 Starting unverified/sexpr-bootstrap/x64/32
May 26 21:48:41 Finished unverified/sexpr-bootstrap/x64/32                    10m31s   8GB
May 26 21:48:42 Starting compiler/benchmarks
May 26 22:26:40 Finished compiler/benchmarks                                  37m56s   2GB
May 26 22:26:40 Starting compiler/bootstrap/compilation/x64/64
May 27 15:25:26 Finished compiler/bootstrap/compilation/x64/64             16h58m41s  64GB
May 27 15:25:26 Starting compiler/bootstrap/compilation/x64/64/proofs
May 27 15:27:51 Finished compiler/bootstrap/compilation/x64/64/proofs          2m24s  20GB
May 27 15:27:51 Starting compiler/bootstrap/compilation/x64/32
May 28 06:49:32 Finished compiler/bootstrap/compilation/x64/32             15h21m37s  64GB
May 28 06:49:33 Starting compiler/bootstrap/compilation/x64/32/proofs
May 28 06:51:48 Finished compiler/bootstrap/compilation/x64/32/proofs          2m15s  18GB
May 28 06:51:48 Starting compiler/bootstrap/compilation/ag32/32
May 31 15:13:42 Resuming compiler/bootstrap/compilation/ag32/32
May 31 15:13:44 Finished compiler/bootstrap/compilation/ag32/32                   1s 146MB
May 31 15:13:44 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 31 15:23:29 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m44s  57GB
May 31 15:23:29 SUCCESS