Job 2121

CakeML:856f1d46cc19b4ced4723300b696246381574520
  Merge pull request #948 from CakeML/lex-decimal-chars [May 03 11:46:15]
HOL:f2908167506081d706dc1ac5ae630620ee2aae91
  Prove that sum of a graph's degrees is twice its number of edges [May 02 12:40:35]
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

May 03 12:03:25 Claimed job
May 03 12:03:31 Building HOL
May 03 12:16:00 Starting developers
May 03 12:16:05 Finished developers                                               5s  99MB
May 03 12:16:05 Starting developers/bin
May 03 12:16:12 Finished developers/bin                                           6s   1GB
May 03 12:16:12 Starting compiler/proofs
May 05 22:58:35 Resuming compiler/proofs
May 05 23:01:25 Finished compiler/proofs                                       2m50s   5GB
May 05 23:01:25 Starting compiler/bootstrap/translation
May 06 06:59:52 Finished compiler/bootstrap/translation                     7h58m26s  45GB
May 06 06:59:52 Starting semantics/ffi
May 06 06:59:59 Finished semantics/ffi                                            6s 221MB
May 06 06:59:59 Starting semantics
May 06 07:00:00 Finished semantics                                                1s  22MB
May 06 07:00:00 Starting semantics/proofs
May 06 07:00:35 Finished semantics/proofs                                        34s   1GB
May 06 07:00:35 Starting semantics/alt_semantics
May 06 07:01:07 Finished semantics/alt_semantics                                 31s 883MB
May 06 07:01:07 Starting semantics/alt_semantics/proofs
May 06 07:13:03 Finished semantics/alt_semantics/proofs                       11m55s   1GB
May 06 07:13:03 Starting basis/pure
May 06 07:13:04 Finished basis/pure                                               1s  20MB
May 06 07:13:05 Starting translator
May 06 07:14:53 Finished translator                                            1m48s   2GB
May 06 07:14:53 Starting compiler/parsing
May 06 07:14:55 Finished compiler/parsing                                         1s  19MB
May 06 07:14:55 Starting characteristic
May 06 07:14:57 Finished characteristic                                           1s  23MB
May 06 07:14:57 Starting translator/monadic
May 06 07:14:59 Finished translator/monadic                                       1s  21MB
May 06 07:14:59 Starting basis
May 06 07:18:56 Finished basis                                                 3m56s   2GB
May 06 07:18:56 Starting compiler/inference
May 06 07:18:58 Finished compiler/inference                                       1s  17MB
May 06 07:18:58 Starting compiler/backend/reg_alloc
May 06 07:19:00 Finished compiler/backend/reg_alloc                               1s  23MB
May 06 07:19:00 Starting compiler/backend/gc
May 06 07:19:02 Finished compiler/backend/gc                                      2s  25MB
May 06 07:19:02 Starting compiler/backend
May 06 07:19:14 Finished compiler/backend                                        12s 846MB
May 06 07:19:15 Starting compiler/encoders/asm
May 06 07:19:16 Finished compiler/encoders/asm                                    1s  25MB
May 06 07:19:16 Starting compiler/encoders/x64
May 06 07:19:18 Finished compiler/encoders/x64                                    1s  24MB
May 06 07:19:18 Starting compiler/encoders/arm7
May 06 07:19:20 Finished compiler/encoders/arm7                                   1s  26MB
May 06 07:19:20 Starting compiler/encoders/arm8
May 06 07:19:22 Finished compiler/encoders/arm8                                   1s  26MB
May 06 07:19:22 Starting compiler/encoders/arm8_asl
May 07 20:05:30 Resuming compiler/encoders/arm8_asl
May 07 22:27:56 Finished compiler/encoders/arm8_asl                         2h22m24s  26GB
May 07 22:27:58 Starting compiler/encoders/mips
May 07 22:28:00 Finished compiler/encoders/mips                                   1s  22MB
May 07 22:28:00 Starting compiler/encoders/riscv
May 07 22:28:02 Finished compiler/encoders/riscv                                  1s  24MB
May 07 22:28:02 Starting compiler/encoders/ag32
May 07 22:28:04 Finished compiler/encoders/ag32                                   1s  25MB
May 07 22:28:04 Starting compiler/backend/x64
May 07 22:28:06 Finished compiler/backend/x64                                     2s  23MB
May 07 22:28:06 Starting compiler/backend/arm7
May 07 22:28:09 Finished compiler/backend/arm7                                    2s  24MB
May 07 22:28:09 Starting compiler/backend/arm8
May 07 22:28:11 Finished compiler/backend/arm8                                    2s  26MB
May 07 22:28:11 Starting compiler/backend/mips
May 07 22:28:13 Finished compiler/backend/mips                                    2s  31MB
May 07 22:28:13 Starting compiler/backend/riscv
May 07 22:28:16 Finished compiler/backend/riscv                                   2s  23MB
May 07 22:28:16 Starting compiler/backend/ag32
May 07 22:29:43 Finished compiler/backend/ag32                                 1m27s   1GB
May 07 22:29:43 Starting compiler/parsing/proofs
May 07 22:29:45 Finished compiler/parsing/proofs                                  1s  17MB
May 07 22:29:45 Starting compiler/inference/proofs
May 07 22:29:47 Finished compiler/inference/proofs                                1s  20MB
May 07 22:29:47 Starting compiler/backend/semantics
May 07 22:30:58 Finished compiler/backend/semantics                            1m10s   1GB
May 07 22:30:58 Starting compiler/backend/reg_alloc/proofs
May 07 22:31:00 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
May 07 22:31:00 Starting compiler/backend/proofs
May 07 22:31:58 Finished compiler/backend/proofs                                 58s   2GB
May 07 22:31:58 Starting compiler/backend/serialiser
May 07 22:32:01 Finished compiler/backend/serialiser                              2s  33MB
May 07 22:32:01 Starting compiler/encoders/x64/proofs
May 07 22:41:51 Finished compiler/encoders/x64/proofs                          9m49s   6GB
May 07 22:41:51 Starting compiler/encoders/arm7/proofs
May 07 22:55:40 Finished compiler/encoders/arm7/proofs                        13m48s   3GB
May 07 22:55:41 Starting compiler/encoders/arm8/proofs
May 07 23:02:33 Finished compiler/encoders/arm8/proofs                         6m52s   1GB
May 07 23:02:34 Starting compiler/encoders/arm8_asl/proofs
May 07 23:54:50 Finished compiler/encoders/arm8_asl/proofs                    52m13s  10GB
May 07 23:54:52 Starting compiler/encoders/mips/proofs
May 08 00:05:28 Finished compiler/encoders/mips/proofs                        10m35s   3GB
May 08 00:05:28 Starting compiler/encoders/riscv/proofs
May 08 00:14:25 Finished compiler/encoders/riscv/proofs                        8m56s   1GB
May 08 00:14:25 Starting compiler/encoders/ag32/proofs
May 08 00:17:01 Finished compiler/encoders/ag32/proofs                         2m36s 962MB
May 08 00:17:01 Starting compiler/backend/x64/proofs
May 08 00:17:32 Finished compiler/backend/x64/proofs                             30s   2GB
May 08 00:17:32 Starting compiler/backend/arm7/proofs
May 08 00:18:05 Finished compiler/backend/arm7/proofs                            32s   2GB
May 08 00:18:05 Starting compiler/backend/arm8/proofs
May 08 00:18:35 Finished compiler/backend/arm8/proofs                            30s   1GB
May 08 00:18:35 Starting compiler/backend/arm8_asl
May 08 00:18:59 Finished compiler/backend/arm8_asl                               24s   1GB
May 08 00:18:59 Starting compiler/backend/mips/proofs
May 08 00:19:31 Finished compiler/backend/mips/proofs                            31s   2GB
May 08 00:19:31 Starting compiler/backend/riscv/proofs
May 08 00:20:05 Finished compiler/backend/riscv/proofs                           33s   2GB
May 08 00:20:05 Starting compiler/backend/ag32/proofs
May 08 00:34:04 Finished compiler/backend/ag32/proofs                         13m59s   2GB
May 08 00:34:04 Starting candle/set-theory
May 08 00:34:43 Finished candle/set-theory                                       38s   1GB
May 08 00:34:43 Starting candle/syntax-lib
May 08 00:34:45 Finished candle/syntax-lib                                        1s  20MB
May 08 00:34:45 Starting candle/standard/syntax
May 08 00:34:55 Finished candle/standard/syntax                                  10s 830MB
May 08 00:34:56 Starting candle/standard/semantics
May 08 00:36:54 Finished candle/standard/semantics                             1m58s   1GB
May 08 00:36:54 Starting candle/standard/monadic
May 08 00:36:56 Finished candle/standard/monadic                                  1s  20MB
May 08 00:36:56 Starting candle/standard/ml_kernel
May 08 00:38:30 Finished candle/standard/ml_kernel                             1m33s   3GB
May 08 00:38:30 Starting candle/overloading/syntax
May 08 00:41:55 Finished candle/overloading/syntax                             3m25s   2GB
May 08 00:41:55 Starting candle/overloading/semantics
May 08 00:54:17 Finished candle/overloading/semantics                         12m21s   2GB
May 08 00:54:17 Starting candle/overloading/monadic
May 08 00:56:59 Finished candle/overloading/monadic                            2m39s   1GB
May 08 00:56:59 Starting candle/overloading/ml_kernel
May 08 01:04:45 Finished candle/overloading/ml_kernel                          7m45s   3GB
May 08 01:04:45 Starting candle/overloading/ml_checker
May 08 01:07:18 Finished candle/overloading/ml_checker                         2m32s   3GB
May 08 01:07:18 Starting candle/prover
May 08 01:17:14 Finished candle/prover                                         9m55s   2GB
May 08 01:17:14 Starting pancake
May 08 01:17:58 Finished pancake                                                 43s 929MB
May 08 01:17:58 Starting pancake/ffi
May 08 01:17:59 Finished pancake/ffi                                              0s  13MB
May 08 01:17:59 Starting pancake/semantics
May 08 01:20:23 Finished pancake/semantics                                     2m23s   1GB
May 08 01:20:23 Starting pancake/proofs
May 08 01:24:37 Finished pancake/proofs                                        4m13s   1GB
May 08 01:24:37 Starting characteristic/examples
May 08 01:26:10 Finished characteristic/examples                               1m32s   2GB
May 08 01:26:10 Starting tutorial/solutions
May 08 01:41:49 Finished tutorial/solutions                                   15m38s   8GB
May 08 01:41:49 Starting translator/monadic/examples
May 08 01:45:50 Finished translator/monadic/examples                           4m00s   3GB
May 08 01:45:50 Starting examples
May 09 20:36:11 Resuming examples
May 09 20:37:46 Finished examples                                              1m35s   1GB
May 09 20:37:46 Starting examples/compilation/x64
May 09 22:38:33 Finished examples/compilation/x64                           2h00m46s  17GB
May 09 22:38:33 Starting examples/compilation/x64/proofs
May 09 22:41:08 Finished examples/compilation/x64/proofs                       2m34s   4GB
May 09 22:41:08 Starting examples/compilation/ag32
May 09 23:11:17 Finished examples/compilation/ag32                            30m08s   7GB
May 09 23:11:17 Starting examples/compilation/ag32/proofs
May 09 23:12:20 Finished examples/compilation/ag32/proofs                      1m02s   5GB
May 09 23:12:20 Starting examples/compilation/to_word
May 09 23:15:36 Finished examples/compilation/to_word                          3m16s   6GB
May 09 23:15:36 Starting examples/lpr_checker
May 09 23:16:42 Finished examples/lpr_checker                                  1m05s   1GB
May 09 23:16:42 Starting examples/lpr_checker/array
May 09 23:53:41 Finished examples/lpr_checker/array                           36m56s   6GB
May 09 23:53:43 Starting examples/lpr_checker/array/compilation
May 10 00:34:06 Finished examples/lpr_checker/array/compilation               40m22s  28GB
May 10 00:34:06 Starting examples/lpr_checker/array/compilation/proofs
May 10 00:35:36 Finished examples/lpr_checker/array/compilation/proofs         1m29s   5GB
May 10 00:35:36 Starting examples/opentheory
May 10 00:46:39 Finished examples/opentheory                                  11m02s   4GB
May 10 00:46:39 Starting examples/opentheory
May 10 00:46:41 Finished examples/opentheory                                      1s  27MB
May 10 00:46:41 Starting examples/opentheory/compilation
May 10 01:23:35 Finished examples/opentheory/compilation                      36m52s  30GB
May 10 01:23:35 Starting examples/opentheory/compilation/proofs
May 10 01:24:33 Finished examples/opentheory/compilation/proofs                  57s   4GB
May 10 01:24:33 Starting examples/opentheory/compilation/ag32
May 10 01:57:43 Finished examples/opentheory/compilation/ag32                 33m10s  29GB
May 10 01:57:43 Starting examples/opentheory/compilation/ag32/proofs
May 10 01:59:34 Finished examples/opentheory/compilation/ag32/proofs           1m50s   5GB
May 10 01:59:34 Starting examples/sat_encodings
May 10 02:01:35 Finished examples/sat_encodings                                2m00s 861MB
May 10 02:01:35 Starting examples/sat_encodings/case_studies
May 10 02:03:23 Finished examples/sat_encodings/case_studies                   1m48s   1GB
May 10 02:03:23 Starting examples/sat_encodings/translation
May 10 02:09:34 Finished examples/sat_encodings/translation                    6m11s   3GB
May 10 02:09:35 Starting examples/sat_encodings/translation/compilation
May 10 02:55:05 Finished examples/sat_encodings/translation/compilation       45m28s  19GB
May 10 02:55:05 Starting examples/deflate
May 10 02:56:07 Finished examples/deflate                                      1m01s 870MB
May 10 02:56:07 Starting examples/deflate/translation
May 10 02:57:50 Finished examples/deflate/translation                          1m42s   3GB
May 10 02:57:50 Starting examples/deflate/translation/compilation
May 10 03:18:11 Finished examples/deflate/translation/compilation             20m20s  11GB
May 10 03:18:11 Starting translator/okasaki-examples
May 10 03:23:25 Finished translator/okasaki-examples                           5m14s   2GB
May 10 03:23:25 Starting translator/other-examples
May 10 03:26:07 Finished translator/other-examples                             2m41s   1GB
May 10 03:26:07 Starting compiler/parsing/tests
May 10 03:26:39 Finished compiler/parsing/tests                                  32s 765MB
May 10 03:26:39 Starting compiler/inference/tests
May 10 03:35:07 Finished compiler/inference/tests                              8m27s   3GB
May 10 03:35:07 Starting compiler/printing/test
May 10 03:39:01 Finished compiler/printing/test                                3m53s   3GB
May 10 03:39:01 Starting icing/flover
May 10 04:22:16 Finished icing/flover                                         43m13s   2GB
May 10 04:22:16 Starting icing/
May 10 05:18:14 Finished icing/                                               55m57s   8GB
May 10 05:18:14 Starting icing/examples
May 10 05:19:46 Finished icing/examples                                        1m32s   4GB
May 10 05:19:46 Starting compiler/repl
May 10 05:28:32 Finished compiler/repl                                         8m43s   6GB
May 10 05:28:32 Starting unverified/sexpr-bootstrap/x64/64
May 10 05:41:52 Finished unverified/sexpr-bootstrap/x64/64                    13m17s  17GB
May 10 05:41:52 Starting unverified/sexpr-bootstrap/x64/32
May 10 05:52:43 Finished unverified/sexpr-bootstrap/x64/32                    10m49s  14GB
May 10 05:52:43 Starting compiler/benchmarks
May 10 06:08:08 Finished compiler/benchmarks                                  15m24s   2GB
May 10 06:08:08 Starting compiler/bootstrap/compilation/x64/64
May 10 17:51:06 Finished compiler/bootstrap/compilation/x64/64             11h42m56s  64GB
May 10 17:51:06 Starting compiler/bootstrap/compilation/x64/64/proofs
May 10 18:11:34 Finished compiler/bootstrap/compilation/x64/64/proofs         20m28s  29GB
May 10 18:11:34 Starting compiler/bootstrap/compilation/x64/32
May 11 00:48:11 Finished compiler/bootstrap/compilation/x64/32              6h36m30s  64GB
May 11 00:48:12 Starting compiler/bootstrap/compilation/x64/32/proofs
May 11 00:51:03 Finished compiler/bootstrap/compilation/x64/32/proofs          2m51s  15GB
May 11 00:51:03 Starting compiler/bootstrap/compilation/ag32/32
May 11 07:49:18 Finished compiler/bootstrap/compilation/ag32/32             6h58m13s  64GB
May 11 07:49:18 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 11 07:56:04 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m45s  23GB
May 11 07:56:04 SUCCESS