Job 2117

CakeML:b4b2e5dbd632063b2f838fadc54d14291ec0b530
  Merge pull request #946 from CakeML/count_allocations [Mar 23 09:59:25]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:stove 4.15.0-143-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

Mar 23 16:51:08 Claimed job
Mar 23 16:51:10 Reusing HOL
Mar 23 16:51:50 Starting developers
Mar 23 16:51:55 Finished developers                                               5s 120MB
Mar 23 16:51:56 Starting developers/bin
Mar 23 16:52:02 Finished developers/bin                                           6s   1GB
Mar 23 16:52:02 Starting compiler/proofs
Mar 23 19:04:00 Finished compiler/proofs                                    2h11m56s  19GB
Mar 23 19:04:00 Starting compiler/bootstrap/translation
Mar 24 03:44:37 Finished compiler/bootstrap/translation                     8h40m35s  40GB
Mar 24 03:44:37 Starting semantics/ffi
Mar 24 03:44:42 Finished semantics/ffi                                            4s 428MB
Mar 24 03:44:42 Starting semantics
Mar 24 03:44:44 Finished semantics                                                1s  22MB
Mar 24 03:44:44 Starting semantics/proofs
Mar 24 03:45:17 Finished semantics/proofs                                        33s   1GB
Mar 24 03:45:17 Starting semantics/alt_semantics
Mar 24 03:45:49 Finished semantics/alt_semantics                                 31s 851MB
Mar 24 03:45:49 Starting semantics/alt_semantics/proofs
Mar 24 03:57:36 Finished semantics/alt_semantics/proofs                       11m47s   2GB
Mar 24 03:57:36 Starting basis/pure
Mar 24 03:57:38 Finished basis/pure                                               1s  26MB
Mar 24 03:57:38 Starting translator
Mar 24 03:59:26 Finished translator                                            1m48s   1GB
Mar 24 03:59:26 Starting compiler/parsing
Mar 24 03:59:28 Finished compiler/parsing                                         1s  22MB
Mar 24 03:59:28 Starting characteristic
Mar 24 03:59:30 Finished characteristic                                           1s  26MB
Mar 24 03:59:30 Starting translator/monadic
Mar 24 03:59:32 Finished translator/monadic                                       1s  22MB
Mar 24 03:59:32 Starting basis
Mar 24 04:03:31 Finished basis                                                 3m58s   3GB
Mar 24 04:03:31 Starting compiler/inference
Mar 24 04:03:33 Finished compiler/inference                                       1s  22MB
Mar 24 04:03:33 Starting compiler/backend/reg_alloc
Mar 24 04:03:34 Finished compiler/backend/reg_alloc                               1s  17MB
Mar 24 04:03:35 Starting compiler/backend/gc
Mar 24 04:03:37 Finished compiler/backend/gc                                      2s  25MB
Mar 24 04:03:37 Starting compiler/backend
Mar 24 04:03:49 Finished compiler/backend                                        12s 759MB
Mar 24 04:03:49 Starting compiler/encoders/asm
Mar 24 04:03:51 Finished compiler/encoders/asm                                    1s  22MB
Mar 24 04:03:51 Starting compiler/encoders/x64
Mar 24 04:03:53 Finished compiler/encoders/x64                                    1s  23MB
Mar 24 04:03:53 Starting compiler/encoders/arm7
Mar 24 04:03:55 Finished compiler/encoders/arm7                                   1s  19MB
Mar 24 04:03:55 Starting compiler/encoders/arm8
Mar 24 04:03:57 Finished compiler/encoders/arm8                                   1s  19MB
Mar 24 04:03:57 Starting compiler/encoders/arm8_asl
Mar 24 04:07:12 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Mar 24 04:07:12 Starting compiler/encoders/mips
Mar 24 04:07:14 Finished compiler/encoders/mips                                   1s  23MB
Mar 24 04:07:14 Starting compiler/encoders/riscv
Mar 24 04:07:16 Finished compiler/encoders/riscv                                  1s  19MB
Mar 24 04:07:16 Starting compiler/encoders/ag32
Mar 24 04:07:18 Finished compiler/encoders/ag32                                   1s  22MB
Mar 24 04:07:18 Starting compiler/backend/x64
Mar 24 04:07:20 Finished compiler/backend/x64                                     2s  27MB
Mar 24 04:07:20 Starting compiler/backend/arm7
Mar 24 04:07:23 Finished compiler/backend/arm7                                    2s  28MB
Mar 24 04:07:23 Starting compiler/backend/arm8
Mar 24 04:07:25 Finished compiler/backend/arm8                                    2s  25MB
Mar 24 04:07:25 Starting compiler/backend/mips
Mar 24 04:07:27 Finished compiler/backend/mips                                    2s  27MB
Mar 24 04:07:27 Starting compiler/backend/riscv
Mar 24 04:07:30 Finished compiler/backend/riscv                                   2s  29MB
Mar 24 04:07:30 Starting compiler/backend/ag32
Mar 24 04:08:58 Finished compiler/backend/ag32                                 1m27s   1GB
Mar 24 04:08:58 Starting compiler/parsing/proofs
Mar 24 04:08:59 Finished compiler/parsing/proofs                                  1s  19MB
Mar 24 04:09:00 Starting compiler/inference/proofs
Mar 24 04:09:01 Finished compiler/inference/proofs                                1s  20MB
Mar 24 04:09:01 Starting compiler/backend/semantics
Mar 24 04:10:13 Finished compiler/backend/semantics                            1m11s   1GB
Mar 24 04:10:13 Starting compiler/backend/reg_alloc/proofs
Mar 24 04:10:15 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Mar 24 04:10:16 Starting compiler/backend/proofs
Mar 24 04:11:15 Finished compiler/backend/proofs                                 59s   3GB
Mar 24 04:11:15 Starting compiler/backend/serialiser
Mar 24 04:11:18 Finished compiler/backend/serialiser                              2s  35MB
Mar 24 04:11:18 Starting compiler/encoders/x64/proofs
Mar 24 04:21:08 Finished compiler/encoders/x64/proofs                          9m49s   7GB
Mar 24 04:21:08 Starting compiler/encoders/arm7/proofs
Mar 24 04:35:06 Finished compiler/encoders/arm7/proofs                        13m58s   3GB
Mar 24 04:35:07 Starting compiler/encoders/arm8/proofs
Mar 24 04:42:01 Finished compiler/encoders/arm8/proofs                         6m53s   1GB
Mar 24 04:42:01 Starting compiler/encoders/arm8_asl/proofs
Mar 24 04:57:57 Finished compiler/encoders/arm8_asl/proofs                    15m54s   1GB
Mar 24 04:57:57 Starting compiler/encoders/mips/proofs
Mar 24 05:08:41 Finished compiler/encoders/mips/proofs                        10m44s   2GB
Mar 24 05:08:41 Starting compiler/encoders/riscv/proofs
Mar 24 05:17:37 Finished compiler/encoders/riscv/proofs                        8m55s   2GB
Mar 24 05:17:37 Starting compiler/encoders/ag32/proofs
Mar 24 05:20:16 Finished compiler/encoders/ag32/proofs                         2m39s 926MB
Mar 24 05:20:16 Starting compiler/backend/x64/proofs
Mar 24 05:20:45 Finished compiler/backend/x64/proofs                             28s   1GB
Mar 24 05:20:45 Starting compiler/backend/arm7/proofs
Mar 24 05:21:18 Finished compiler/backend/arm7/proofs                            33s   2GB
Mar 24 05:21:18 Starting compiler/backend/arm8/proofs
Mar 24 05:21:49 Finished compiler/backend/arm8/proofs                            30s   2GB
Mar 24 05:21:49 Starting compiler/backend/arm8_asl
Mar 24 05:22:12 Finished compiler/backend/arm8_asl                               23s   1GB
Mar 24 05:22:13 Starting compiler/backend/mips/proofs
Mar 24 05:22:43 Finished compiler/backend/mips/proofs                            30s   1GB
Mar 24 05:22:43 Starting compiler/backend/riscv/proofs
Mar 24 05:23:17 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 24 05:23:17 Starting compiler/backend/ag32/proofs
Mar 24 05:37:24 Finished compiler/backend/ag32/proofs                         14m06s   3GB
Mar 24 05:37:24 Starting candle/set-theory
Mar 24 05:38:03 Finished candle/set-theory                                       38s   1GB
Mar 24 05:38:03 Starting candle/syntax-lib
Mar 24 05:38:05 Finished candle/syntax-lib                                        1s  27MB
Mar 24 05:38:05 Starting candle/standard/syntax
Mar 24 05:38:16 Finished candle/standard/syntax                                  10s 713MB
Mar 24 05:38:16 Starting candle/standard/semantics
Mar 24 05:40:14 Finished candle/standard/semantics                             1m57s   1GB
Mar 24 05:40:14 Starting candle/standard/monadic
Mar 24 05:40:16 Finished candle/standard/monadic                                  1s  21MB
Mar 24 05:40:16 Starting candle/standard/ml_kernel
Mar 24 05:41:52 Finished candle/standard/ml_kernel                             1m36s   3GB
Mar 24 05:41:52 Starting candle/overloading/syntax
Mar 24 05:45:13 Finished candle/overloading/syntax                             3m20s   1GB
Mar 24 05:45:13 Starting candle/overloading/semantics
Mar 24 05:57:22 Finished candle/overloading/semantics                         12m08s   3GB
Mar 24 05:57:22 Starting candle/overloading/monadic
Mar 24 06:00:02 Finished candle/overloading/monadic                            2m37s   1GB
Mar 24 06:00:03 Starting candle/overloading/ml_kernel
Mar 24 06:07:57 Finished candle/overloading/ml_kernel                          7m53s   3GB
Mar 24 06:07:57 Starting candle/overloading/ml_checker
Mar 24 06:10:27 Finished candle/overloading/ml_checker                         2m30s   4GB
Mar 24 06:10:27 Starting candle/prover
Mar 24 06:20:26 Finished candle/prover                                         9m59s   3GB
Mar 24 06:20:26 Starting pancake
Mar 24 06:21:11 Finished pancake                                                 44s 902MB
Mar 24 06:21:11 Starting pancake/ffi
Mar 24 06:21:11 Finished pancake/ffi                                              0s  13MB
Mar 24 06:21:11 Starting pancake/semantics
Mar 24 06:23:40 Finished pancake/semantics                                     2m28s   1GB
Mar 24 06:23:40 Starting pancake/proofs
Mar 24 06:27:49 Finished pancake/proofs                                        4m09s   2GB
Mar 24 06:27:50 Starting characteristic/examples
Mar 24 06:29:18 Finished characteristic/examples                               1m27s   3GB
Mar 24 06:29:18 Starting tutorial/solutions
Mar 24 06:44:45 Finished tutorial/solutions                                   15m27s   7GB
Mar 24 06:44:45 Starting translator/monadic/examples
Mar 24 06:48:51 Finished translator/monadic/examples                           4m06s   3GB
Mar 24 06:48:51 Starting examples
Mar 24 07:04:34 Finished examples                                             15m41s   4GB
Mar 24 07:04:34 Starting examples/compilation/x64
Mar 24 09:04:07 Finished examples/compilation/x64                           1h59m32s  16GB
Mar 24 09:04:08 Starting examples/compilation/x64/proofs
Mar 24 09:06:37 Finished examples/compilation/x64/proofs                       2m28s   4GB
Mar 24 09:06:37 Starting examples/compilation/ag32
Mar 24 09:37:15 Finished examples/compilation/ag32                            30m38s   7GB
Mar 24 09:37:15 Starting examples/compilation/ag32/proofs
Mar 24 09:38:20 Finished examples/compilation/ag32/proofs                      1m04s   5GB
Mar 24 09:38:20 Starting examples/compilation/to_word
Mar 24 09:41:48 Finished examples/compilation/to_word                          3m27s   5GB
Mar 24 09:41:48 Starting examples/lpr_checker
Mar 24 09:42:54 Finished examples/lpr_checker                                  1m06s   1GB
Mar 24 09:42:54 Starting examples/lpr_checker/array
Mar 24 10:19:44 Finished examples/lpr_checker/array                           36m48s   5GB
Mar 24 10:19:44 Starting examples/lpr_checker/array/compilation
Mar 24 10:59:52 Finished examples/lpr_checker/array/compilation               40m07s  31GB
Mar 24 10:59:52 Starting examples/lpr_checker/array/compilation/proofs
Mar 24 11:01:28 Finished examples/lpr_checker/array/compilation/proofs         1m35s   6GB
Mar 24 11:01:28 Starting examples/opentheory
Mar 24 11:12:32 Finished examples/opentheory                                  11m04s   4GB
Mar 24 11:12:32 Starting examples/opentheory
Mar 24 11:12:34 Finished examples/opentheory                                      1s  28MB
Mar 24 11:12:34 Starting examples/opentheory/compilation
Mar 24 11:49:26 Finished examples/opentheory/compilation                      36m49s  30GB
Mar 24 11:49:26 Starting examples/opentheory/compilation/proofs
Mar 24 11:50:31 Finished examples/opentheory/compilation/proofs                1m04s   4GB
Mar 24 11:50:31 Starting examples/opentheory/compilation/ag32
Mar 24 12:23:43 Finished examples/opentheory/compilation/ag32                 33m11s  29GB
Mar 24 12:23:43 Starting examples/opentheory/compilation/ag32/proofs
Mar 24 12:25:40 Finished examples/opentheory/compilation/ag32/proofs           1m57s   4GB
Mar 24 12:25:40 Starting examples/sat_encodings
Mar 24 12:27:42 Finished examples/sat_encodings                                2m01s 968MB
Mar 24 12:27:42 Starting examples/sat_encodings/case_studies
Mar 24 12:29:32 Finished examples/sat_encodings/case_studies                   1m49s   1GB
Mar 24 12:29:32 Starting examples/sat_encodings/translation
Mar 24 12:35:45 Finished examples/sat_encodings/translation                    6m12s   4GB
Mar 24 12:35:45 Starting examples/sat_encodings/translation/compilation
Mar 24 13:23:02 Finished examples/sat_encodings/translation/compilation       47m16s  22GB
Mar 24 13:23:03 Starting examples/deflate
Mar 24 13:24:02 Finished examples/deflate                                        58s 912MB
Mar 24 13:24:02 Starting examples/deflate/translation
Mar 24 13:25:43 Finished examples/deflate/translation                          1m41s   3GB
Mar 24 13:25:43 Starting examples/deflate/translation/compilation
Mar 24 13:46:06 Finished examples/deflate/translation/compilation             20m22s  11GB
Mar 24 13:46:06 Starting translator/okasaki-examples
Mar 24 13:51:16 Finished translator/okasaki-examples                           5m09s   2GB
Mar 24 13:51:16 Starting translator/other-examples
Mar 24 13:52:11 Finished translator/other-examples                               54s   1GB
Mar 24 13:52:11 Starting compiler/parsing/tests
Mar 24 13:52:43 Finished compiler/parsing/tests                                  31s 779MB
Mar 24 13:52:43 Starting compiler/inference/tests
Mar 24 14:01:06 Finished compiler/inference/tests                              8m23s   5GB
Mar 24 14:01:07 Starting compiler/printing/test
Mar 24 14:04:47 Finished compiler/printing/test                                3m40s   4GB
Mar 24 14:04:47 Starting icing/flover
Mar 24 14:47:30 Finished icing/flover                                         42m41s   2GB
Mar 24 14:47:31 Starting icing/
Mar 24 15:43:46 Finished icing/                                               56m15s   7GB
Mar 24 15:43:46 Starting icing/examples
Mar 24 15:45:20 Finished icing/examples                                        1m33s   6GB
Mar 24 15:45:20 Starting compiler/repl
Mar 24 15:53:59 Finished compiler/repl                                         8m37s   5GB
Mar 24 15:53:59 Starting unverified/sexpr-bootstrap/x64/64
Mar 24 16:07:15 Finished unverified/sexpr-bootstrap/x64/64                    13m12s  15GB
Mar 24 16:07:15 Starting unverified/sexpr-bootstrap/x64/32
Mar 24 16:18:12 Finished unverified/sexpr-bootstrap/x64/32                    10m52s  13GB
Mar 24 16:18:12 Starting compiler/benchmarks
Mar 24 16:33:37 Finished compiler/benchmarks                                  15m24s   2GB
Mar 24 16:33:37 Starting compiler/bootstrap/compilation/x64/64
Mar 25 04:32:24 Finished compiler/bootstrap/compilation/x64/64             11h58m44s  64GB
Mar 25 04:32:24 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 25 04:53:16 Finished compiler/bootstrap/compilation/x64/64/proofs         20m52s  43GB
Mar 25 04:53:16 Starting compiler/bootstrap/compilation/x64/32
Mar 25 11:58:13 Finished compiler/bootstrap/compilation/x64/32              7h04m54s  64GB
Mar 25 11:58:13 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 25 12:01:11 Finished compiler/bootstrap/compilation/x64/32/proofs          2m57s  17GB
Mar 25 12:01:11 Starting compiler/bootstrap/compilation/ag32/32
Mar 25 19:05:11 Finished compiler/bootstrap/compilation/ag32/32             7h03m59s  64GB
Mar 25 19:05:11 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 25 19:12:06 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m55s  44GB
Mar 25 19:12:07 SUCCESS