Job 1055

CakeML:dc73bd8f21601e06bdc92eb303865a3992673970
  Merge pull request #694 from CakeML/remove-oom [Oct 13 07:36:28]
HOL:4f67f38e1314dcb1488b3925ddbbc4bbd80795bf
  Use new syntax for some theorems in examples/lambda/basics/term [Oct 14 00:51:09]
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

Oct 16 02:45:13 Claimed job
Oct 16 02:45:20 Building HOL
Oct 16 02:54:44 Starting developers
Oct 16 02:54:46 Finished developers                                               1s  75MB
Oct 16 02:54:46 Starting developers/bin
Oct 16 02:54:50 Finished developers/bin                                           3s 164MB
Oct 16 02:54:50 Starting semantics/ffi
Oct 16 02:55:25 Finished semantics/ffi                                           34s 330MB
Oct 16 02:55:25 Starting semantics
Oct 16 02:56:58 Finished semantics                                             1m33s   1GB
Oct 16 02:56:59 Starting semantics/proofs
Oct 16 02:59:58 Finished semantics/proofs                                      2m58s   1GB
Oct 16 02:59:58 Starting semantics/alt_semantics
Oct 16 03:00:04 Finished semantics/alt_semantics                                  6s 310MB
Oct 16 03:00:05 Starting semantics/alt_semantics/proofs
Oct 16 03:01:54 Finished semantics/alt_semantics/proofs                        1m49s   1GB
Oct 16 03:01:55 Starting basis/pure
Oct 16 03:05:48 Finished basis/pure                                            3m53s 922MB
Oct 16 03:05:48 Starting translator
Oct 16 03:07:37 Finished translator                                            1m48s   1GB
Oct 16 03:07:37 Starting compiler/parsing
Oct 16 03:08:37 Finished compiler/parsing                                        59s   1GB
Oct 16 03:08:37 Starting characteristic
Oct 16 03:13:52 Finished characteristic                                        5m14s   1GB
Oct 16 03:13:52 Starting translator/monadic
Oct 16 03:15:17 Finished translator/monadic                                    1m24s   1GB
Oct 16 03:15:17 Starting basis
Oct 16 03:35:21 Finished basis                                                20m02s   3GB
Oct 16 03:35:21 Starting compiler/inference
Oct 16 03:37:15 Finished compiler/inference                                    1m53s   1GB
Oct 16 03:37:15 Starting compiler/backend/reg_alloc
Oct 16 03:38:14 Finished compiler/backend/reg_alloc                              58s   1GB
Oct 16 03:38:14 Starting compiler/backend/gc
Oct 16 03:47:38 Finished compiler/backend/gc                                   9m23s   1GB
Oct 16 03:47:38 Starting compiler/backend
Oct 16 03:47:39 Finished compiler/backend                                         0s  45MB
Oct 16 03:47:39 Starting compiler/encoders/asm
Oct 16 03:47:40 Finished compiler/encoders/asm                                    0s  35MB
Oct 16 03:47:40 Starting compiler/encoders/x64
Oct 16 03:48:38 Finished compiler/encoders/x64                                   58s 806MB
Oct 16 03:48:39 Starting compiler/encoders/arm7
Oct 16 03:50:18 Finished compiler/encoders/arm7                                1m38s   1GB
Oct 16 03:50:18 Starting compiler/encoders/arm8
Oct 16 03:50:48 Finished compiler/encoders/arm8                                  30s 560MB
Oct 16 03:50:49 Starting compiler/encoders/mips
Oct 16 03:51:54 Finished compiler/encoders/mips                                1m05s 946MB
Oct 16 03:51:54 Starting compiler/encoders/riscv
Oct 16 03:53:14 Finished compiler/encoders/riscv                               1m19s 774MB
Oct 16 03:53:14 Starting compiler/encoders/ag32
Oct 16 03:53:30 Finished compiler/encoders/ag32                                  14s 804MB
Oct 16 03:53:30 Starting compiler/backend/x64
Oct 16 03:53:45 Finished compiler/backend/x64                                    15s 873MB
Oct 16 03:53:46 Starting compiler/backend/arm7
Oct 16 03:54:04 Finished compiler/backend/arm7                                   17s   1GB
Oct 16 03:54:04 Starting compiler/backend/arm8
Oct 16 03:54:21 Finished compiler/backend/arm8                                   16s   1GB
Oct 16 03:54:21 Starting compiler/backend/mips
Oct 16 03:54:38 Finished compiler/backend/mips                                   16s   1GB
Oct 16 03:54:38 Starting compiler/backend/riscv
Oct 16 03:54:55 Finished compiler/backend/riscv                                  16s   1GB
Oct 16 03:54:55 Starting compiler/backend/ag32
Oct 16 03:56:03 Finished compiler/backend/ag32                                 1m07s   1GB
Oct 16 03:56:03 Starting compiler/parsing/proofs
Oct 16 04:01:50 Finished compiler/parsing/proofs                               5m45s 795MB
Oct 16 04:01:50 Starting compiler/inference/proofs
Oct 16 04:04:33 Finished compiler/inference/proofs                             2m42s   1GB
Oct 16 04:04:33 Starting compiler/backend/semantics
Oct 16 04:10:47 Finished compiler/backend/semantics                            6m13s   1GB
Oct 16 04:10:47 Starting compiler/backend/reg_alloc/proofs
Oct 16 04:14:05 Finished compiler/backend/reg_alloc/proofs                     3m17s 811MB
Oct 16 04:14:05 Starting compiler/backend/proofs
Oct 16 04:55:29 Finished compiler/backend/proofs                              41m23s   4GB
Oct 16 04:55:29 Starting compiler/encoders/x64/proofs
Oct 16 05:05:53 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Oct 16 05:05:53 Starting compiler/encoders/arm7/proofs
Oct 16 05:19:39 Finished compiler/encoders/arm7/proofs                        13m46s   3GB
Oct 16 05:19:40 Starting compiler/encoders/arm8/proofs
Oct 16 05:26:14 Finished compiler/encoders/arm8/proofs                         6m34s   1GB
Oct 16 05:26:15 Starting compiler/encoders/mips/proofs
Oct 16 05:36:36 Finished compiler/encoders/mips/proofs                        10m21s   1GB
Oct 16 05:36:37 Starting compiler/encoders/riscv/proofs
Oct 16 05:45:16 Finished compiler/encoders/riscv/proofs                        8m39s   1GB
Oct 16 05:45:17 Starting compiler/encoders/ag32/proofs
Oct 16 05:47:46 Finished compiler/encoders/ag32/proofs                         2m29s 865MB
Oct 16 05:47:47 Starting compiler/backend/x64/proofs
Oct 16 05:48:03 Finished compiler/backend/x64/proofs                             16s 994MB
Oct 16 05:48:04 Starting compiler/backend/arm7/proofs
Oct 16 05:48:22 Finished compiler/backend/arm7/proofs                            17s   1GB
Oct 16 05:48:22 Starting compiler/backend/arm8/proofs
Oct 16 05:48:39 Finished compiler/backend/arm8/proofs                            16s   1GB
Oct 16 05:48:39 Starting compiler/backend/mips/proofs
Oct 16 05:48:58 Finished compiler/backend/mips/proofs                            17s   1GB
Oct 16 05:48:58 Starting compiler/backend/riscv/proofs
Oct 16 05:49:15 Finished compiler/backend/riscv/proofs                           17s   1GB
Oct 16 05:49:16 Starting compiler/backend/ag32/proofs
Oct 16 05:58:16 Finished compiler/backend/ag32/proofs                          8m59s   3GB
Oct 16 05:58:17 Starting compiler/proofs
Oct 16 05:59:55 Finished compiler/proofs                                       1m38s   2GB
Oct 16 05:59:55 Starting candle/set-theory
Oct 16 06:00:21 Finished candle/set-theory                                       25s 782MB
Oct 16 06:00:21 Starting candle/syntax-lib
Oct 16 06:00:31 Finished candle/syntax-lib                                        9s 581MB
Oct 16 06:00:31 Starting candle/standard/syntax
Oct 16 06:02:14 Finished candle/standard/syntax                                1m42s   1GB
Oct 16 06:02:15 Starting candle/standard/semantics
Oct 16 06:03:50 Finished candle/standard/semantics                             1m35s   1GB
Oct 16 06:03:50 Starting candle/standard/monadic
Oct 16 06:05:26 Finished candle/standard/monadic                               1m35s   1GB
Oct 16 06:05:26 Starting candle/standard/ml_kernel
Oct 16 06:09:25 Finished candle/standard/ml_kernel                             3m58s   3GB
Oct 16 06:09:25 Starting candle/standard/opentheory
Oct 16 06:18:15 Finished candle/standard/opentheory                            8m49s   3GB
Oct 16 06:18:15 Starting candle/standard/opentheory/compilation
Oct 16 06:49:01 Finished candle/standard/opentheory/compilation               30m45s  15GB
Oct 16 06:49:01 Starting candle/standard/opentheory/compilation/proofs
Oct 16 06:49:46 Finished candle/standard/opentheory/compilation/proofs           45s   2GB
Oct 16 06:49:46 Starting characteristic/examples
Oct 16 06:51:13 Finished characteristic/examples                               1m26s   2GB
Oct 16 06:51:13 Starting tutorial/solutions
Oct 16 07:04:42 Finished tutorial/solutions                                   13m28s   6GB
Oct 16 07:04:42 Starting translator/monadic/examples
Oct 16 07:07:43 Finished translator/monadic/examples                           3m00s   2GB
Oct 16 07:07:43 Starting examples
Oct 16 07:17:08 Finished examples                                              9m25s   4GB
Oct 16 07:17:09 Starting examples/compilation/x64
Oct 16 09:23:05 Finished examples/compilation/x64                           2h05m54s  13GB
Oct 16 09:23:05 Starting examples/compilation/x64/proofs
Oct 16 09:24:37 Finished examples/compilation/x64/proofs                       1m30s   2GB
Oct 16 09:24:37 Starting examples/compilation/ag32
Oct 16 09:53:41 Finished examples/compilation/ag32                            29m03s   5GB
Oct 16 09:53:41 Starting examples/compilation/ag32/proofs
Oct 16 09:54:37 Finished examples/compilation/ag32/proofs                        56s   3GB
Oct 16 09:54:38 Starting translator/okasaki-examples
Oct 16 09:58:49 Finished translator/okasaki-examples                           4m11s   1GB
Oct 16 09:58:50 Starting translator/other-examples
Oct 16 10:02:17 Finished translator/other-examples                             3m26s   1GB
Oct 16 10:02:17 Starting compiler/parsing/tests
Oct 16 10:02:42 Finished compiler/parsing/tests                                  24s 483MB
Oct 16 10:02:42 Starting compiler/inference/tests
Oct 16 10:07:06 Finished compiler/inference/tests                              4m23s   3GB
Oct 16 10:07:06 Starting compiler/bootstrap/translation
Oct 16 12:45:07 Finished compiler/bootstrap/translation                     2h38m00s  45GB
Oct 16 12:45:08 Starting unverified/sexpr-bootstrap/x64/64
Oct 16 12:59:22 Finished unverified/sexpr-bootstrap/x64/64                    14m13s   4GB
Oct 16 12:59:22 Starting unverified/sexpr-bootstrap/x64/32
Oct 16 13:08:58 Finished unverified/sexpr-bootstrap/x64/32                     9m33s   7GB
Oct 16 13:08:59 Starting compiler/benchmarks
Oct 16 13:46:46 Finished compiler/benchmarks                                  37m45s   2GB
Oct 16 13:46:46 Starting compiler/bootstrap/compilation/x64/64
Oct 17 03:48:58 Finished compiler/bootstrap/compilation/x64/64             14h02m10s  63GB
Oct 17 03:48:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 17 03:53:26 Finished compiler/bootstrap/compilation/x64/64/proofs          4m27s   6GB
Oct 17 03:53:27 Starting compiler/bootstrap/compilation/x64/32
Oct 17 15:42:50 Finished compiler/bootstrap/compilation/x64/32             11h49m22s  63GB
Oct 17 15:42:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 17 15:46:24 Finished compiler/bootstrap/compilation/x64/32/proofs          3m32s   5GB
Oct 17 15:46:24 Starting compiler/bootstrap/compilation/ag32/32
Oct 18 04:58:53 Finished compiler/bootstrap/compilation/ag32/32            13h12m27s  64GB
Oct 18 04:58:53 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 18 05:23:26 Finished compiler/bootstrap/compilation/ag32/32/proofs        24m32s  17GB
Oct 18 05:23:27 SUCCESS