Job 1538

CakeML:e186cc1984bac5cce7c150b458fe1604eece7703
  Fix cost examples [May 21 07:35:10]
HOL:3309c51ff0fc07e1ac1b254b4206400f551c96bd
  Polish bnfAlgebra, including moving some results to core theories [May 30 11:35:25]
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 31 20:26:01 Claimed job
May 31 20:26:03 Building HOL
May 31 20:40:28 Starting developers
May 31 20:40:30 Finished developers                                               2s 106MB
May 31 20:40:31 Starting developers/bin
May 31 20:40:37 Finished developers/bin                                           6s   1GB
May 31 20:40:37 Starting semantics/ffi
May 31 20:40:47 Finished semantics/ffi                                           10s 265MB
May 31 20:40:48 Starting semantics
May 31 20:42:22 Finished semantics                                             1m34s   1GB
May 31 20:42:23 Starting semantics/proofs
May 31 20:45:55 Finished semantics/proofs                                      3m31s   2GB
May 31 20:45:55 Starting semantics/alt_semantics
May 31 20:46:04 Finished semantics/alt_semantics                                  8s 424MB
May 31 20:46:04 Starting semantics/alt_semantics/proofs
May 31 20:48:17 Finished semantics/alt_semantics/proofs                        2m13s   1GB
May 31 20:48:17 Starting basis/pure
May 31 20:50:59 Finished basis/pure                                            2m41s   1GB
May 31 20:50:59 Starting translator
May 31 20:54:18 Finished translator                                            3m18s   2GB
May 31 20:54:18 Starting compiler/parsing
May 31 20:55:27 Finished compiler/parsing                                      1m08s   5GB
May 31 20:55:27 Starting characteristic
May 31 21:01:07 Finished characteristic                                        5m39s   3GB
May 31 21:01:07 Starting translator/monadic
May 31 21:02:53 Finished translator/monadic                                    1m46s   2GB
May 31 21:02:53 Starting basis
May 31 21:47:02 Finished basis                                                44m08s  24GB
May 31 21:47:02 Starting compiler/inference
May 31 21:48:15 Finished compiler/inference                                    1m12s   2GB
May 31 21:48:15 Starting compiler/backend/reg_alloc
May 31 21:49:23 Finished compiler/backend/reg_alloc                            1m07s   1GB
May 31 21:49:23 Starting compiler/backend/gc
May 31 21:53:04 Finished compiler/backend/gc                                   3m40s   3GB
May 31 21:53:04 Starting compiler/backend
May 31 21:58:13 Finished compiler/backend                                      5m08s   5GB
May 31 21:58:13 Starting compiler/encoders/asm
May 31 21:58:36 Finished compiler/encoders/asm                                   22s   1GB
May 31 21:58:36 Starting compiler/encoders/x64
May 31 21:59:40 Finished compiler/encoders/x64                                 1m03s   1GB
May 31 21:59:40 Starting compiler/encoders/arm7
May 31 22:01:44 Finished compiler/encoders/arm7                                2m03s   1GB
May 31 22:01:44 Starting compiler/encoders/arm8
May 31 22:02:24 Finished compiler/encoders/arm8                                  39s   1GB
May 31 22:02:24 Starting compiler/encoders/mips
May 31 22:03:51 Finished compiler/encoders/mips                                1m26s   1GB
May 31 22:03:51 Starting compiler/encoders/riscv
May 31 22:05:31 Finished compiler/encoders/riscv                               1m39s   1GB
May 31 22:05:31 Starting compiler/encoders/ag32
May 31 22:05:50 Finished compiler/encoders/ag32                                  18s 981MB
May 31 22:05:50 Starting compiler/backend/x64
May 31 22:06:08 Finished compiler/backend/x64                                    18s   1GB
May 31 22:06:09 Starting compiler/backend/arm7
May 31 22:06:29 Finished compiler/backend/arm7                                   19s   1GB
May 31 22:06:29 Starting compiler/backend/arm8
May 31 22:06:49 Finished compiler/backend/arm8                                   19s   1GB
May 31 22:06:49 Starting compiler/backend/mips
May 31 22:07:10 Finished compiler/backend/mips                                   21s   1GB
May 31 22:07:11 Starting compiler/backend/riscv
May 31 22:07:32 Finished compiler/backend/riscv                                  20s   1GB
May 31 22:07:32 Starting compiler/backend/ag32
May 31 22:08:41 Finished compiler/backend/ag32                                 1m09s   2GB
May 31 22:08:42 Starting compiler/parsing/proofs
May 31 22:14:23 Finished compiler/parsing/proofs                               5m41s   2GB
May 31 22:14:23 Starting compiler/inference/proofs
May 31 22:16:55 Finished compiler/inference/proofs                             2m31s   2GB
May 31 22:16:55 Starting compiler/backend/semantics
May 31 22:43:58 Finished compiler/backend/semantics                           27m02s   4GB
May 31 22:43:58 Starting compiler/backend/reg_alloc/proofs
May 31 22:47:16 Finished compiler/backend/reg_alloc/proofs                     3m18s   1GB
May 31 22:47:17 Starting compiler/backend/proofs
May 31 23:41:04 Finished compiler/backend/proofs                              53m46s  15GB
May 31 23:41:04 Starting compiler/encoders/x64/proofs
May 31 23:50:22 Finished compiler/encoders/x64/proofs                          9m18s   7GB
May 31 23:50:23 Starting compiler/encoders/arm7/proofs
Jun 01 00:03:14 Finished compiler/encoders/arm7/proofs                        12m50s   7GB
Jun 01 00:03:14 Starting compiler/encoders/arm8/proofs
Jun 01 00:09:59 Finished compiler/encoders/arm8/proofs                         6m44s   3GB
Jun 01 00:09:59 Starting compiler/encoders/mips/proofs
Jun 01 00:19:55 Finished compiler/encoders/mips/proofs                         9m55s   3GB
Jun 01 00:19:55 Starting compiler/encoders/riscv/proofs
Jun 01 00:28:13 Finished compiler/encoders/riscv/proofs                        8m17s   3GB
Jun 01 00:28:13 Starting compiler/encoders/ag32/proofs
Jun 01 00:30:34 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Jun 01 00:30:34 Starting compiler/backend/x64/proofs
Jun 01 00:30:56 Finished compiler/backend/x64/proofs                             21s   2GB
Jun 01 00:30:57 Starting compiler/backend/arm7/proofs
Jun 01 00:31:20 Finished compiler/backend/arm7/proofs                            23s   1GB
Jun 01 00:31:21 Starting compiler/backend/arm8/proofs
Jun 01 00:31:44 Finished compiler/backend/arm8/proofs                            22s   2GB
Jun 01 00:31:44 Starting compiler/backend/mips/proofs
Jun 01 00:32:06 Finished compiler/backend/mips/proofs                            22s   1GB
Jun 01 00:32:06 Starting compiler/backend/riscv/proofs
Jun 01 00:32:30 Finished compiler/backend/riscv/proofs                           23s   2GB
Jun 01 00:32:30 Starting compiler/backend/ag32/proofs
Jun 01 00:44:31 Finished compiler/backend/ag32/proofs                         12m00s   5GB
Jun 01 00:44:31 Starting compiler/proofs
Jun 01 00:46:31 Finished compiler/proofs                                       1m59s   6GB
Jun 01 00:46:31 Starting candle/set-theory
Jun 01 00:47:02 Finished candle/set-theory                                       30s   1GB
Jun 01 00:47:02 Starting candle/syntax-lib
Jun 01 00:47:13 Finished candle/syntax-lib                                       11s 815MB
Jun 01 00:47:13 Starting candle/standard/syntax
Jun 01 00:49:05 Finished candle/standard/syntax                                1m51s   1GB
Jun 01 00:49:05 Starting candle/standard/semantics
Jun 01 00:50:53 Finished candle/standard/semantics                             1m47s   2GB
Jun 01 00:50:53 Starting candle/standard/monadic
Jun 01 00:52:37 Finished candle/standard/monadic                               1m43s   1GB
Jun 01 00:52:37 Starting candle/standard/ml_kernel
Jun 01 00:58:08 Finished candle/standard/ml_kernel                             5m31s   5GB
Jun 01 00:58:09 Starting candle/overloading/syntax
Jun 01 01:01:21 Finished candle/overloading/syntax                             3m12s   2GB
Jun 01 01:01:21 Starting candle/overloading/semantics
Jun 01 01:13:22 Finished candle/overloading/semantics                         12m00s   8GB
Jun 01 01:13:22 Starting characteristic/examples
Jun 01 01:14:44 Finished characteristic/examples                               1m21s   4GB
Jun 01 01:14:44 Starting tutorial/solutions
Jun 01 01:30:16 Finished tutorial/solutions                                   15m31s  13GB
Jun 01 01:30:16 Starting translator/monadic/examples
Jun 01 01:33:44 Finished translator/monadic/examples                           3m27s   4GB
Jun 01 01:33:44 Starting examples
Jun 01 01:42:32 Finished examples                                              8m47s   6GB
Jun 01 01:42:33 Starting examples/compilation/x64
Jun 01 04:04:59 Finished examples/compilation/x64                           2h22m25s  20GB
Jun 01 04:05:01 Starting examples/compilation/x64/proofs
Jun 01 04:07:03 Finished examples/compilation/x64/proofs                       2m01s   3GB
Jun 01 04:07:03 Starting examples/compilation/ag32
Jun 01 04:41:06 Finished examples/compilation/ag32                            34m03s  15GB
Jun 01 04:41:06 Starting examples/compilation/ag32/proofs
Jun 01 04:42:00 Finished examples/compilation/ag32/proofs                        53s   5GB
Jun 01 04:42:00 Starting examples/cost
Jun 01 05:37:16 Finished examples/cost                                        55m15s  14GB
Jun 01 05:37:16 Starting examples/lpr_checker
Jun 01 05:41:10 Finished examples/lpr_checker                                  3m54s   3GB
Jun 01 05:41:10 Starting examples/lpr_checker/compilation
Jun 01 05:59:34 Finished examples/lpr_checker/compilation                     18m23s  16GB
Jun 01 05:59:35 Starting examples/lpr_checker/compilation/proofs
Jun 01 06:00:20 Finished examples/lpr_checker/compilation/proofs                 45s   4GB
Jun 01 06:00:20 Starting examples/lpr_checker/array
Jun 01 06:14:11 Finished examples/lpr_checker/array                           13m51s   5GB
Jun 01 06:14:12 Starting examples/lpr_checker/array/compilation
Jun 01 06:34:26 Finished examples/lpr_checker/array/compilation               20m14s  17GB
Jun 01 06:34:26 Starting examples/lpr_checker/array/compilation/proofs
Jun 01 06:35:18 Finished examples/lpr_checker/array/compilation/proofs           51s   5GB
Jun 01 06:35:18 Starting examples/opentheory
Jun 01 06:44:50 Finished examples/opentheory                                   9m30s   6GB
Jun 01 06:44:51 Starting examples/opentheory
Jun 01 06:44:51 Finished examples/opentheory                                      0s  98MB
Jun 01 06:44:52 Starting examples/opentheory/compilation
Jun 01 07:16:17 Finished examples/opentheory/compilation                      31m24s  19GB
Jun 01 07:16:17 Starting examples/opentheory/compilation/proofs
Jun 01 07:17:02 Finished examples/opentheory/compilation/proofs                  44s   4GB
Jun 01 07:17:02 Starting examples/opentheory/compilation/ag32
Jun 01 07:50:10 Finished examples/opentheory/compilation/ag32                 33m07s  21GB
Jun 01 07:50:10 Starting examples/opentheory/compilation/ag32/proofs
Jun 01 07:51:48 Finished examples/opentheory/compilation/ag32/proofs           1m37s   9GB
Jun 01 07:51:48 Starting translator/okasaki-examples
Jun 01 07:56:13 Finished translator/okasaki-examples                           4m24s   3GB
Jun 01 07:56:13 Starting translator/other-examples
Jun 01 07:58:18 Finished translator/other-examples                             2m05s   2GB
Jun 01 07:58:18 Starting compiler/parsing/tests
Jun 01 07:58:43 Finished compiler/parsing/tests                                  24s 648MB
Jun 01 07:58:43 Starting compiler/inference/tests
Jun 01 08:06:06 Finished compiler/inference/tests                              7m22s   7GB
Jun 01 08:06:06 Starting compiler/bootstrap/translation
Jun 01 10:31:45 Finished compiler/bootstrap/translation                     2h25m37s  48GB
Jun 01 10:31:45 Starting unverified/sexpr-bootstrap/x64/64
Jun 01 10:44:09 Finished unverified/sexpr-bootstrap/x64/64                    12m19s   8GB
Jun 01 10:44:09 Starting unverified/sexpr-bootstrap/x64/32
Jun 01 10:54:43 Finished unverified/sexpr-bootstrap/x64/32                    10m29s   8GB
Jun 01 10:54:43 Starting compiler/benchmarks
Jun 01 11:32:58 Finished compiler/benchmarks                                  38m14s   2GB
Jun 01 11:32:58 Starting compiler/bootstrap/compilation/x64/64
Jun 02 04:15:08 Finished compiler/bootstrap/compilation/x64/64             16h42m05s  64GB
Jun 02 04:15:09 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 02 04:17:30 Finished compiler/bootstrap/compilation/x64/64/proofs          2m20s  20GB
Jun 02 04:17:30 Starting compiler/bootstrap/compilation/x64/32
Jun 02 20:06:26 Finished compiler/bootstrap/compilation/x64/32             15h48m52s  64GB
Jun 02 20:06:26 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 02 20:08:33 Finished compiler/bootstrap/compilation/x64/32/proofs          2m06s  14GB
Jun 02 20:08:34 Starting compiler/bootstrap/compilation/ag32/32
Jun 03 11:45:43 Finished compiler/bootstrap/compilation/ag32/32            15h37m08s  64GB
Jun 03 11:45:43 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 03 11:55:10 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m26s  56GB
Jun 03 11:55:10 SUCCESS