Job 1535

CakeML:e186cc1984bac5cce7c150b458fe1604eece7703
  Fix cost examples [May 21 07:35:10]
HOL:fe4634b86ea93f927bb796c73b7f77e15362962e
  Universally quantify statements [May 17 23:32:35]
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 21 07:35:22 Claimed job
May 21 07:35:28 Reusing HOL
May 21 07:35:33 Starting developers
May 21 07:35:33 Finished developers                                               0s  35MB
May 21 07:35:34 Starting developers/bin
May 21 07:35:40 Finished developers/bin                                           5s   1GB
May 21 07:35:40 Starting semantics/ffi
May 21 07:35:50 Finished semantics/ffi                                           10s 291MB
May 21 07:35:51 Starting semantics
May 21 07:37:17 Finished semantics                                             1m26s   1GB
May 21 07:37:17 Starting semantics/proofs
May 21 07:40:51 Finished semantics/proofs                                      3m33s   2GB
May 21 07:40:51 Starting semantics/alt_semantics
May 21 07:41:00 Finished semantics/alt_semantics                                  8s 392MB
May 21 07:41:00 Starting semantics/alt_semantics/proofs
May 21 07:43:13 Finished semantics/alt_semantics/proofs                        2m12s   1GB
May 21 07:43:13 Starting basis/pure
May 21 07:44:08 Finished basis/pure                                              54s   1GB
May 21 07:44:08 Starting translator
May 21 07:47:25 Finished translator                                            3m16s   2GB
May 21 07:47:25 Starting compiler/parsing
May 21 07:48:33 Finished compiler/parsing                                      1m07s   2GB
May 21 07:48:34 Starting characteristic
May 21 07:54:22 Finished characteristic                                        5m48s   4GB
May 21 07:54:22 Starting translator/monadic
May 21 07:56:11 Finished translator/monadic                                    1m48s   3GB
May 21 07:56:11 Starting basis
May 21 08:40:02 Finished basis                                                43m50s  18GB
May 21 08:40:02 Starting compiler/inference
May 21 08:41:11 Finished compiler/inference                                    1m08s   2GB
May 21 08:41:11 Starting compiler/backend/reg_alloc
May 21 08:42:19 Finished compiler/backend/reg_alloc                            1m07s   1GB
May 21 08:42:19 Starting compiler/backend/gc
May 21 08:45:45 Finished compiler/backend/gc                                   3m26s   3GB
May 21 08:45:46 Starting compiler/backend
May 21 08:50:52 Finished compiler/backend                                      5m05s   5GB
May 21 08:50:52 Starting compiler/encoders/asm
May 21 08:51:15 Finished compiler/encoders/asm                                   23s   1GB
May 21 08:51:16 Starting compiler/encoders/x64
May 21 08:51:43 Finished compiler/encoders/x64                                   27s   1GB
May 21 08:51:43 Starting compiler/encoders/arm7
May 21 08:52:34 Finished compiler/encoders/arm7                                  51s   1GB
May 21 08:52:35 Starting compiler/encoders/arm8
May 21 08:52:49 Finished compiler/encoders/arm8                                  13s   1GB
May 21 08:52:49 Starting compiler/encoders/mips
May 21 08:53:07 Finished compiler/encoders/mips                                  17s   1GB
May 21 08:53:07 Starting compiler/encoders/riscv
May 21 08:53:24 Finished compiler/encoders/riscv                                 16s   1GB
May 21 08:53:24 Starting compiler/encoders/ag32
May 21 08:53:42 Finished compiler/encoders/ag32                                  18s 948MB
May 21 08:53:43 Starting compiler/backend/x64
May 21 08:54:03 Finished compiler/backend/x64                                    20s   1GB
May 21 08:54:03 Starting compiler/backend/arm7
May 21 08:54:25 Finished compiler/backend/arm7                                   21s   1GB
May 21 08:54:25 Starting compiler/backend/arm8
May 21 08:54:46 Finished compiler/backend/arm8                                   20s   1GB
May 21 08:54:46 Starting compiler/backend/mips
May 21 08:55:07 Finished compiler/backend/mips                                   20s   1GB
May 21 08:55:07 Starting compiler/backend/riscv
May 21 08:55:28 Finished compiler/backend/riscv                                  21s   1GB
May 21 08:55:28 Starting compiler/backend/ag32
May 21 08:56:36 Finished compiler/backend/ag32                                 1m07s   2GB
May 21 08:56:36 Starting compiler/parsing/proofs
May 21 09:02:31 Finished compiler/parsing/proofs                               5m54s   2GB
May 21 09:02:31 Starting compiler/inference/proofs
May 21 09:05:05 Finished compiler/inference/proofs                             2m34s   2GB
May 21 09:05:05 Starting compiler/backend/semantics
May 21 09:32:32 Finished compiler/backend/semantics                           27m27s   5GB
May 21 09:32:33 Starting compiler/backend/reg_alloc/proofs
May 21 09:35:51 Finished compiler/backend/reg_alloc/proofs                     3m17s   1GB
May 21 09:35:51 Starting compiler/backend/proofs
May 21 10:29:54 Finished compiler/backend/proofs                              54m02s  24GB
May 21 10:29:54 Starting compiler/encoders/x64/proofs
May 21 10:39:22 Finished compiler/encoders/x64/proofs                          9m28s   6GB
May 21 10:39:23 Starting compiler/encoders/arm7/proofs
May 21 10:52:08 Finished compiler/encoders/arm7/proofs                        12m44s   7GB
May 21 10:52:08 Starting compiler/encoders/arm8/proofs
May 21 10:58:46 Finished compiler/encoders/arm8/proofs                         6m37s   3GB
May 21 10:58:46 Starting compiler/encoders/mips/proofs
May 21 11:08:39 Finished compiler/encoders/mips/proofs                         9m52s   6GB
May 21 11:08:39 Starting compiler/encoders/riscv/proofs
May 21 11:16:55 Finished compiler/encoders/riscv/proofs                        8m16s   3GB
May 21 11:16:55 Starting compiler/encoders/ag32/proofs
May 21 11:19:15 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
May 21 11:19:15 Starting compiler/backend/x64/proofs
May 21 11:19:37 Finished compiler/backend/x64/proofs                             21s   1GB
May 21 11:19:37 Starting compiler/backend/arm7/proofs
May 21 11:20:00 Finished compiler/backend/arm7/proofs                            23s   1GB
May 21 11:20:00 Starting compiler/backend/arm8/proofs
May 21 11:20:22 Finished compiler/backend/arm8/proofs                            21s   1GB
May 21 11:20:23 Starting compiler/backend/mips/proofs
May 21 11:20:45 Finished compiler/backend/mips/proofs                            22s   1GB
May 21 11:20:45 Starting compiler/backend/riscv/proofs
May 21 11:21:09 Finished compiler/backend/riscv/proofs                           23s   2GB
May 21 11:21:09 Starting compiler/backend/ag32/proofs
May 21 11:33:17 Finished compiler/backend/ag32/proofs                         12m07s   4GB
May 21 11:33:17 Starting compiler/proofs
May 21 11:35:17 Finished compiler/proofs                                       2m00s   6GB
May 21 11:35:18 Starting candle/set-theory
May 21 11:35:48 Finished candle/set-theory                                       29s   1GB
May 21 11:35:48 Starting candle/syntax-lib
May 21 11:36:00 Finished candle/syntax-lib                                       11s 818MB
May 21 11:36:00 Starting candle/standard/syntax
May 21 11:37:52 Finished candle/standard/syntax                                1m51s   1GB
May 21 11:37:52 Starting candle/standard/semantics
May 21 11:39:39 Finished candle/standard/semantics                             1m46s   2GB
May 21 11:39:39 Starting candle/standard/monadic
May 21 11:41:23 Finished candle/standard/monadic                               1m43s   2GB
May 21 11:41:23 Starting candle/standard/ml_kernel
May 21 11:46:53 Finished candle/standard/ml_kernel                             5m30s   6GB
May 21 11:46:54 Starting candle/overloading/syntax
May 21 11:50:02 Finished candle/overloading/syntax                             3m07s   1GB
May 21 11:50:02 Starting candle/overloading/semantics
May 21 12:02:06 Finished candle/overloading/semantics                         12m04s   8GB
May 21 12:02:06 Starting characteristic/examples
May 21 12:03:26 Finished characteristic/examples                               1m19s   4GB
May 21 12:03:27 Starting tutorial/solutions
May 21 12:18:38 Finished tutorial/solutions                                   15m10s  12GB
May 21 12:18:38 Starting translator/monadic/examples
May 21 12:22:05 Finished translator/monadic/examples                           3m26s   3GB
May 21 12:22:05 Starting examples
May 21 12:30:58 Finished examples                                              8m52s   6GB
May 21 12:30:58 Starting examples/compilation/x64
May 21 14:51:46 Finished examples/compilation/x64                           2h20m47s  24GB
May 21 14:51:47 Starting examples/compilation/x64/proofs
May 21 14:53:48 Finished examples/compilation/x64/proofs                       2m01s   3GB
May 21 14:53:48 Starting examples/compilation/ag32
May 21 15:27:50 Finished examples/compilation/ag32                            34m01s  11GB
May 21 15:27:50 Starting examples/compilation/ag32/proofs
May 21 15:28:45 Finished examples/compilation/ag32/proofs                        54s   5GB
May 21 15:28:45 Starting examples/cost
May 21 16:24:46 Finished examples/cost                                        56m00s  13GB
May 21 16:24:46 Starting examples/lpr_checker
May 21 16:28:40 Finished examples/lpr_checker                                  3m54s   3GB
May 21 16:28:41 Starting examples/lpr_checker/compilation
May 21 16:47:23 Finished examples/lpr_checker/compilation                     18m42s  15GB
May 21 16:47:23 Starting examples/lpr_checker/compilation/proofs
May 21 16:48:09 Finished examples/lpr_checker/compilation/proofs                 46s   4GB
May 21 16:48:10 Starting examples/lpr_checker/array
May 21 17:01:57 Finished examples/lpr_checker/array                           13m47s   6GB
May 21 17:01:58 Starting examples/lpr_checker/array/compilation
May 21 17:21:56 Finished examples/lpr_checker/array/compilation               19m58s  13GB
May 21 17:21:56 Starting examples/lpr_checker/array/compilation/proofs
May 21 17:22:46 Finished examples/lpr_checker/array/compilation/proofs           49s   5GB
May 21 17:22:46 Starting examples/opentheory
May 21 17:32:08 Finished examples/opentheory                                   9m21s   3GB
May 21 17:32:09 Starting examples/opentheory
May 21 17:32:09 Finished examples/opentheory                                      0s 100MB
May 21 17:32:09 Starting examples/opentheory/compilation
May 21 18:02:17 Finished examples/opentheory/compilation                      30m07s  27GB
May 21 18:02:17 Starting examples/opentheory/compilation/proofs
May 21 18:03:03 Finished examples/opentheory/compilation/proofs                  45s   4GB
May 21 18:03:03 Starting examples/opentheory/compilation/ag32
May 21 18:35:35 Finished examples/opentheory/compilation/ag32                 32m31s  29GB
May 21 18:35:35 Starting examples/opentheory/compilation/ag32/proofs
May 21 18:37:11 Finished examples/opentheory/compilation/ag32/proofs           1m35s   9GB
May 21 18:37:11 Starting translator/okasaki-examples
May 21 18:41:34 Finished translator/okasaki-examples                           4m22s   3GB
May 21 18:41:34 Starting translator/other-examples
May 21 18:43:36 Finished translator/other-examples                             2m01s   2GB
May 21 18:43:36 Starting compiler/parsing/tests
May 21 18:44:01 Finished compiler/parsing/tests                                  24s 723MB
May 21 18:44:01 Starting compiler/inference/tests
May 21 18:51:17 Finished compiler/inference/tests                              7m15s   5GB
May 21 18:51:17 Starting compiler/bootstrap/translation
May 21 21:22:44 Finished compiler/bootstrap/translation                     2h31m26s  44GB
May 21 21:22:44 Starting unverified/sexpr-bootstrap/x64/64
May 21 21:35:08 Finished unverified/sexpr-bootstrap/x64/64                    12m17s   8GB
May 21 21:35:08 Starting unverified/sexpr-bootstrap/x64/32
May 21 21:45:41 Finished unverified/sexpr-bootstrap/x64/32                    10m27s   8GB
May 21 21:45:41 Starting compiler/benchmarks
May 21 22:23:29 Finished compiler/benchmarks                                  37m47s   2GB
May 21 22:23:29 Starting compiler/bootstrap/compilation/x64/64
May 22 15:57:11 Finished compiler/bootstrap/compilation/x64/64             17h33m38s  64GB
May 22 15:57:12 Starting compiler/bootstrap/compilation/x64/64/proofs
May 22 15:59:26 Finished compiler/bootstrap/compilation/x64/64/proofs          2m14s  15GB
May 22 15:59:27 Starting compiler/bootstrap/compilation/x64/32
May 23 07:16:33 Finished compiler/bootstrap/compilation/x64/32             15h17m02s  63GB
May 23 07:16:33 Starting compiler/bootstrap/compilation/x64/32/proofs
May 23 07:18:39 Finished compiler/bootstrap/compilation/x64/32/proofs          2m05s  18GB
May 23 07:18:39 Starting compiler/bootstrap/compilation/ag32/32
May 23 22:47:07 Finished compiler/bootstrap/compilation/ag32/32            15h28m28s  64GB
May 23 22:47:08 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 23 22:56:49 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m40s  57GB
May 23 22:56:49 SUCCESS