Job 2122

CakeML:db4a478223a00be0062fd30dca61c6e532b19ca5
  Add new functions to List module in basis [May 05 11:22:17]
#950 (rev_list)
Merging into: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

May 11 07:56:06 Claimed job
May 11 07:56:11 Reusing HOL
May 11 07:56:51 Starting developers
May 11 07:56:56 Finished developers                                               5s  94MB
May 11 07:56:56 Starting developers/bin
May 11 07:57:02 Finished developers/bin                                           6s   1GB
May 11 07:57:02 Starting compiler/proofs
May 11 09:46:32 Finished compiler/proofs                                    1h49m28s  18GB
May 11 09:46:32 Starting compiler/bootstrap/translation
May 11 17:57:08 Finished compiler/bootstrap/translation                     8h10m34s  42GB
May 11 17:57:09 Starting semantics/ffi
May 11 17:57:14 Finished semantics/ffi                                            4s 425MB
May 11 17:57:14 Starting semantics
May 11 17:57:15 Finished semantics                                                1s  20MB
May 11 17:57:15 Starting semantics/proofs
May 11 17:57:50 Finished semantics/proofs                                        34s   1GB
May 11 17:57:50 Starting semantics/alt_semantics
May 11 17:58:22 Finished semantics/alt_semantics                                 31s 880MB
May 11 17:58:22 Starting semantics/alt_semantics/proofs
May 11 18:10:20 Finished semantics/alt_semantics/proofs                       11m57s   1GB
May 11 18:10:20 Starting basis/pure
May 11 18:10:22 Finished basis/pure                                               1s  19MB
May 11 18:10:22 Starting translator
May 11 18:12:10 Finished translator                                            1m48s   1GB
May 11 18:12:10 Starting compiler/parsing
May 11 18:12:12 Finished compiler/parsing                                         1s  18MB
May 11 18:12:12 Starting characteristic
May 11 18:12:14 Finished characteristic                                           1s  25MB
May 11 18:12:14 Starting translator/monadic
May 11 18:12:16 Finished translator/monadic                                       1s  22MB
May 11 18:12:16 Starting basis
May 11 18:16:26 Finished basis                                                 4m09s   3GB
May 11 18:16:26 Starting compiler/inference
May 11 18:16:28 Finished compiler/inference                                       1s  18MB
May 11 18:16:28 Starting compiler/backend/reg_alloc
May 11 18:16:30 Finished compiler/backend/reg_alloc                               1s  18MB
May 11 18:16:30 Starting compiler/backend/gc
May 11 18:16:32 Finished compiler/backend/gc                                      2s  25MB
May 11 18:16:32 Starting compiler/backend
May 11 18:16:45 Finished compiler/backend                                        12s 845MB
May 11 18:16:45 Starting compiler/encoders/asm
May 11 18:16:46 Finished compiler/encoders/asm                                    1s  22MB
May 11 18:16:47 Starting compiler/encoders/x64
May 11 18:16:48 Finished compiler/encoders/x64                                    1s  21MB
May 11 18:16:48 Starting compiler/encoders/arm7
May 11 18:16:50 Finished compiler/encoders/arm7                                   1s  25MB
May 11 18:16:50 Starting compiler/encoders/arm8
May 11 18:16:52 Finished compiler/encoders/arm8                                   1s  22MB
May 11 18:16:52 Starting compiler/encoders/arm8_asl
May 11 18:20:08 Finished compiler/encoders/arm8_asl                            3m15s   1GB
May 11 18:20:08 Starting compiler/encoders/mips
May 11 18:20:10 Finished compiler/encoders/mips                                   1s  20MB
May 11 18:20:10 Starting compiler/encoders/riscv
May 11 18:20:12 Finished compiler/encoders/riscv                                  1s  22MB
May 11 18:20:12 Starting compiler/encoders/ag32
May 11 18:20:14 Finished compiler/encoders/ag32                                   1s  22MB
May 11 18:20:14 Starting compiler/backend/x64
May 11 18:20:16 Finished compiler/backend/x64                                     2s  29MB
May 11 18:20:16 Starting compiler/backend/arm7
May 11 18:20:18 Finished compiler/backend/arm7                                    2s  22MB
May 11 18:20:18 Starting compiler/backend/arm8
May 11 18:20:21 Finished compiler/backend/arm8                                    2s  28MB
May 11 18:20:21 Starting compiler/backend/mips
May 11 18:20:23 Finished compiler/backend/mips                                    2s  21MB
May 11 18:20:23 Starting compiler/backend/riscv
May 11 18:20:25 Finished compiler/backend/riscv                                   2s  22MB
May 11 18:20:26 Starting compiler/backend/ag32
May 11 18:21:53 Finished compiler/backend/ag32                                 1m27s   1GB
May 11 18:21:53 Starting compiler/parsing/proofs
May 11 18:21:55 Finished compiler/parsing/proofs                                  1s  18MB
May 11 18:21:55 Starting compiler/inference/proofs
May 11 18:21:57 Finished compiler/inference/proofs                                1s  20MB
May 11 18:21:57 Starting compiler/backend/semantics
May 11 18:23:11 Finished compiler/backend/semantics                            1m13s   1GB
May 11 18:23:11 Starting compiler/backend/reg_alloc/proofs
May 11 18:23:13 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
May 11 18:23:13 Starting compiler/backend/proofs
May 11 18:24:11 Finished compiler/backend/proofs                                 58s   2GB
May 11 18:24:11 Starting compiler/backend/serialiser
May 11 18:24:14 Finished compiler/backend/serialiser                              2s  37MB
May 11 18:24:14 Starting compiler/encoders/x64/proofs
May 11 18:34:05 Finished compiler/encoders/x64/proofs                          9m50s   6GB
May 11 18:34:05 Starting compiler/encoders/arm7/proofs
May 11 18:47:50 Finished compiler/encoders/arm7/proofs                        13m44s   3GB
May 11 18:47:50 Starting compiler/encoders/arm8/proofs
May 11 18:54:49 Finished compiler/encoders/arm8/proofs                         6m59s   1GB
May 11 18:54:49 Starting compiler/encoders/arm8_asl/proofs
May 11 19:10:39 Finished compiler/encoders/arm8_asl/proofs                    15m49s   2GB
May 11 19:10:39 Starting compiler/encoders/mips/proofs
May 11 19:21:25 Finished compiler/encoders/mips/proofs                        10m45s   1GB
May 11 19:21:25 Starting compiler/encoders/riscv/proofs
May 11 19:30:34 Finished compiler/encoders/riscv/proofs                        9m08s   1GB
May 11 19:30:34 Starting compiler/encoders/ag32/proofs
May 11 19:33:09 Finished compiler/encoders/ag32/proofs                         2m35s   1GB
May 11 19:33:09 Starting compiler/backend/x64/proofs
May 11 19:33:38 Finished compiler/backend/x64/proofs                             29s   1GB
May 11 19:33:38 Starting compiler/backend/arm7/proofs
May 11 19:34:10 Finished compiler/backend/arm7/proofs                            31s   2GB
May 11 19:34:11 Starting compiler/backend/arm8/proofs
May 11 19:34:41 Finished compiler/backend/arm8/proofs                            30s   2GB
May 11 19:34:41 Starting compiler/backend/arm8_asl
May 11 19:35:03 Finished compiler/backend/arm8_asl                               22s   1GB
May 11 19:35:03 Starting compiler/backend/mips/proofs
May 11 19:35:35 Finished compiler/backend/mips/proofs                            31s   1GB
May 11 19:35:35 Starting compiler/backend/riscv/proofs
May 11 19:36:09 Finished compiler/backend/riscv/proofs                           33s   2GB
May 11 19:36:09 Starting compiler/backend/ag32/proofs
May 11 19:50:01 Finished compiler/backend/ag32/proofs                         13m51s   2GB
May 11 19:50:01 Starting candle/set-theory
May 11 19:50:39 Finished candle/set-theory                                       37s   1GB
May 11 19:50:39 Starting candle/syntax-lib
May 11 19:50:40 Finished candle/syntax-lib                                        1s  21MB
May 11 19:50:41 Starting candle/standard/syntax
May 11 19:50:52 Finished candle/standard/syntax                                  10s 822MB
May 11 19:50:52 Starting candle/standard/semantics
May 11 19:52:50 Finished candle/standard/semantics                             1m58s   1GB
May 11 19:52:50 Starting candle/standard/monadic
May 11 19:52:52 Finished candle/standard/monadic                                  1s  21MB
May 11 19:52:52 Starting candle/standard/ml_kernel
May 11 19:54:29 Finished candle/standard/ml_kernel                             1m36s   3GB
May 11 19:54:29 Starting candle/overloading/syntax
May 11 19:57:50 Finished candle/overloading/syntax                             3m21s   1GB
May 11 19:57:50 Starting candle/overloading/semantics
May 11 20:09:54 Finished candle/overloading/semantics                         12m03s   2GB
May 11 20:09:54 Starting candle/overloading/monadic
May 11 20:12:34 Finished candle/overloading/monadic                            2m38s   1GB
May 11 20:12:34 Starting candle/overloading/ml_kernel
May 11 20:20:31 Finished candle/overloading/ml_kernel                          7m56s   3GB
May 11 20:20:31 Starting candle/overloading/ml_checker
May 11 20:23:05 Finished candle/overloading/ml_checker                         2m33s   3GB
May 11 20:23:05 Starting candle/prover
May 11 20:32:55 Finished candle/prover                                         9m50s   2GB
May 11 20:32:55 Starting pancake
May 11 20:33:39 Finished pancake                                                 44s   1GB
May 11 20:33:39 Starting pancake/ffi
May 11 20:33:40 Finished pancake/ffi                                              0s  13MB
May 11 20:33:40 Starting pancake/semantics
May 11 20:36:12 Finished pancake/semantics                                     2m32s   1GB
May 11 20:36:13 Starting pancake/proofs
May 11 20:40:25 Finished pancake/proofs                                        4m12s   3GB
May 11 20:40:25 Starting characteristic/examples
May 11 20:41:56 Finished characteristic/examples                               1m30s   2GB
May 11 20:41:56 Starting tutorial/solutions
May 11 20:57:22 Finished tutorial/solutions                                   15m25s   6GB
May 11 20:57:22 Starting translator/monadic/examples
May 11 21:01:20 Finished translator/monadic/examples                           3m58s   3GB
May 11 21:01:20 Starting examples
May 11 21:18:01 Finished examples                                             16m39s   4GB
May 11 21:18:01 Starting examples/compilation/x64
May 11 23:17:09 Finished examples/compilation/x64                           1h59m05s  14GB
May 11 23:17:09 Starting examples/compilation/x64/proofs
May 11 23:19:40 Finished examples/compilation/x64/proofs                       2m30s   3GB
May 11 23:19:40 Starting examples/compilation/ag32
May 11 23:50:41 Finished examples/compilation/ag32                            31m00s   7GB
May 11 23:50:41 Starting examples/compilation/ag32/proofs
May 11 23:51:45 Finished examples/compilation/ag32/proofs                      1m04s   5GB
May 11 23:51:45 Starting examples/compilation/to_word
May 11 23:55:13 Finished examples/compilation/to_word                          3m27s   4GB
May 11 23:55:13 Starting examples/lpr_checker
May 11 23:56:18 Finished examples/lpr_checker                                  1m04s   1GB
May 11 23:56:18 Starting examples/lpr_checker/array
May 12 00:33:16 Finished examples/lpr_checker/array                           36m57s   8GB
May 12 00:33:16 Starting examples/lpr_checker/array/compilation
May 12 01:14:04 Finished examples/lpr_checker/array/compilation               40m48s  24GB
May 12 01:14:04 Starting examples/lpr_checker/array/compilation/proofs
May 12 01:15:36 Finished examples/lpr_checker/array/compilation/proofs         1m31s   7GB
May 12 01:15:36 Starting examples/opentheory
May 12 01:26:30 Finished examples/opentheory                                  10m53s   4GB
May 12 01:26:30 Starting examples/opentheory
May 12 01:26:32 Finished examples/opentheory                                      1s  28MB
May 12 01:26:32 Starting examples/opentheory/compilation
May 12 02:04:25 Finished examples/opentheory/compilation                      37m50s  26GB
May 12 02:04:25 Starting examples/opentheory/compilation/proofs
May 12 02:05:28 Finished examples/opentheory/compilation/proofs                1m02s   4GB
May 12 02:05:28 Starting examples/opentheory/compilation/ag32
May 12 02:38:38 Finished examples/opentheory/compilation/ag32                 33m09s  28GB
May 12 02:38:38 Starting examples/opentheory/compilation/ag32/proofs
May 12 02:40:36 Finished examples/opentheory/compilation/ag32/proofs           1m57s   8GB
May 12 02:40:36 Starting examples/sat_encodings
May 12 02:42:37 Finished examples/sat_encodings                                2m00s 859MB
May 12 02:42:37 Starting examples/sat_encodings/case_studies
May 12 02:44:27 Finished examples/sat_encodings/case_studies                   1m50s   1GB
May 12 02:44:28 Starting examples/sat_encodings/translation
May 12 02:50:46 Finished examples/sat_encodings/translation                    6m18s   4GB
May 12 02:50:46 Starting examples/sat_encodings/translation/compilation
May 12 03:36:35 Finished examples/sat_encodings/translation/compilation       45m46s  22GB
May 12 03:36:35 Starting examples/deflate
May 12 03:37:37 Finished examples/deflate                                      1m01s 993MB
May 12 03:37:37 Starting examples/deflate/translation
May 12 03:39:19 Finished examples/deflate/translation                          1m42s   3GB
May 12 03:39:19 Starting examples/deflate/translation/compilation
May 12 03:59:27 Finished examples/deflate/translation/compilation             20m07s  12GB
May 12 03:59:27 Starting translator/okasaki-examples
May 12 04:04:40 Finished translator/okasaki-examples                           5m12s   2GB
May 12 04:04:40 Starting translator/other-examples
May 12 04:05:36 Finished translator/other-examples                               55s   1GB
May 12 04:05:36 Starting compiler/parsing/tests
May 12 04:06:08 Finished compiler/parsing/tests                                  32s 739MB
May 12 04:06:08 Starting compiler/inference/tests
May 12 04:14:43 Finished compiler/inference/tests                              8m34s   3GB
May 12 04:14:43 Starting compiler/printing/test
May 12 04:18:33 Finished compiler/printing/test                                3m50s   3GB
May 12 04:18:33 Starting icing/flover
May 12 05:01:13 Finished icing/flover                                         42m37s   2GB
May 12 05:01:13 Starting icing/
May 12 05:57:22 Finished icing/                                               56m09s   7GB
May 12 05:57:22 Starting icing/examples
May 12 05:58:53 Finished icing/examples                                        1m29s   3GB
May 12 05:58:53 Starting compiler/repl
May 12 06:07:38 Finished compiler/repl                                         8m43s   5GB
May 12 06:07:38 Starting unverified/sexpr-bootstrap/x64/64
May 12 06:21:00 Finished unverified/sexpr-bootstrap/x64/64                    13m21s  16GB
May 12 06:21:00 Starting unverified/sexpr-bootstrap/x64/32
May 12 06:31:46 Finished unverified/sexpr-bootstrap/x64/32                    10m45s  14GB
May 12 06:31:46 Starting compiler/benchmarks
May 12 06:47:08 Finished compiler/benchmarks                                  15m21s   2GB
May 12 06:47:08 Starting compiler/bootstrap/compilation/x64/64
May 12 18:29:16 Finished compiler/bootstrap/compilation/x64/64             11h42m06s  64GB
May 12 18:29:16 Starting compiler/bootstrap/compilation/x64/64/proofs
May 12 18:49:47 Finished compiler/bootstrap/compilation/x64/64/proofs         20m30s  31GB
May 12 18:49:47 Starting compiler/bootstrap/compilation/x64/32
May 13 01:56:57 Finished compiler/bootstrap/compilation/x64/32              7h07m09s  58GB
May 13 01:56:57 Starting compiler/bootstrap/compilation/x64/32/proofs
May 13 01:59:57 Finished compiler/bootstrap/compilation/x64/32/proofs          2m59s  17GB
May 13 01:59:57 Starting compiler/bootstrap/compilation/ag32/32
May 13 09:37:00 Finished compiler/bootstrap/compilation/ag32/32             7h37m01s  64GB
May 13 09:37:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 13 09:43:44 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m43s  31GB
May 13 09:43:44 SUCCESS