Job 2080

CakeML:395c80b348616fe6e0af7e6b5af491c3bb138f73
  Fix breakage caused by HOL-Theorem-Prover/HOL@29ebd7ceac5df [Jan 10 04:31:54]
HOL:fcd4fa574e5dc5df47c8e575bcb14fc4b299c9b3
  Add a couple of simple automatic rewrites for generic graphs [Jan 08 10:56:36]
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

Jan 10 04:33:36 Claimed job
Jan 10 04:33:38 Reusing HOL
Jan 10 04:34:20 Starting developers
Jan 10 04:34:25 Finished developers                                               5s 105MB
Jan 10 04:34:25 Starting developers/bin
Jan 10 04:34:31 Finished developers/bin                                           5s   1GB
Jan 10 04:34:31 Starting compiler/proofs
Jan 10 06:22:33 Finished compiler/proofs                                    1h48m00s  17GB
Jan 10 06:22:33 Starting compiler/bootstrap/translation
Jan 10 11:18:00 Finished compiler/bootstrap/translation                     4h55m25s  40GB
Jan 10 11:18:00 Starting semantics/ffi
Jan 10 11:18:05 Finished semantics/ffi                                            4s 416MB
Jan 10 11:18:05 Starting semantics
Jan 10 11:18:06 Finished semantics                                                1s  18MB
Jan 10 11:18:06 Starting semantics/proofs
Jan 10 11:18:40 Finished semantics/proofs                                        33s   1GB
Jan 10 11:18:40 Starting semantics/alt_semantics
Jan 10 11:19:11 Finished semantics/alt_semantics                                 30s 736MB
Jan 10 11:19:11 Starting semantics/alt_semantics/proofs
Jan 10 11:31:01 Finished semantics/alt_semantics/proofs                       11m50s   2GB
Jan 10 11:31:01 Starting basis/pure
Jan 10 11:31:03 Finished basis/pure                                               1s  18MB
Jan 10 11:31:03 Starting translator
Jan 10 11:32:53 Finished translator                                            1m49s   1GB
Jan 10 11:32:53 Starting compiler/parsing
Jan 10 11:32:54 Finished compiler/parsing                                         1s  20MB
Jan 10 11:32:54 Starting characteristic
Jan 10 11:32:56 Finished characteristic                                           1s  28MB
Jan 10 11:32:56 Starting translator/monadic
Jan 10 11:32:58 Finished translator/monadic                                       1s  21MB
Jan 10 11:32:58 Starting basis
Jan 10 11:36:26 Finished basis                                                 3m27s   3GB
Jan 10 11:36:26 Starting compiler/inference
Jan 10 11:36:28 Finished compiler/inference                                       1s  19MB
Jan 10 11:36:28 Starting compiler/backend/reg_alloc
Jan 10 11:36:30 Finished compiler/backend/reg_alloc                               1s  21MB
Jan 10 11:36:30 Starting compiler/backend/gc
Jan 10 11:36:32 Finished compiler/backend/gc                                      2s  26MB
Jan 10 11:36:32 Starting compiler/backend
Jan 10 11:36:45 Finished compiler/backend                                        12s 792MB
Jan 10 11:36:45 Starting compiler/encoders/asm
Jan 10 11:36:47 Finished compiler/encoders/asm                                    1s  23MB
Jan 10 11:36:47 Starting compiler/encoders/x64
Jan 10 11:36:48 Finished compiler/encoders/x64                                    1s  19MB
Jan 10 11:36:49 Starting compiler/encoders/arm7
Jan 10 11:36:50 Finished compiler/encoders/arm7                                   1s  25MB
Jan 10 11:36:50 Starting compiler/encoders/arm8
Jan 10 11:36:52 Finished compiler/encoders/arm8                                   1s  23MB
Jan 10 11:36:52 Starting compiler/encoders/arm8_asl
Jan 10 14:06:08 Finished compiler/encoders/arm8_asl                         2h29m14s  34GB
Jan 10 14:06:08 Starting compiler/encoders/mips
Jan 10 14:06:10 Finished compiler/encoders/mips                                   1s  21MB
Jan 10 14:06:10 Starting compiler/encoders/riscv
Jan 10 14:06:12 Finished compiler/encoders/riscv                                  1s  22MB
Jan 10 14:06:12 Starting compiler/encoders/ag32
Jan 10 14:06:13 Finished compiler/encoders/ag32                                   1s  19MB
Jan 10 14:06:14 Starting compiler/backend/x64
Jan 10 14:06:16 Finished compiler/backend/x64                                     2s  24MB
Jan 10 14:06:16 Starting compiler/backend/arm7
Jan 10 14:06:18 Finished compiler/backend/arm7                                    2s  28MB
Jan 10 14:06:18 Starting compiler/backend/arm8
Jan 10 14:06:20 Finished compiler/backend/arm8                                    2s  26MB
Jan 10 14:06:20 Starting compiler/backend/mips
Jan 10 14:06:23 Finished compiler/backend/mips                                    2s  27MB
Jan 10 14:06:23 Starting compiler/backend/riscv
Jan 10 14:06:25 Finished compiler/backend/riscv                                   2s  26MB
Jan 10 14:06:25 Starting compiler/backend/ag32
Jan 10 14:07:53 Finished compiler/backend/ag32                                 1m28s   1GB
Jan 10 14:07:54 Starting compiler/parsing/proofs
Jan 10 14:07:55 Finished compiler/parsing/proofs                                  1s  19MB
Jan 10 14:07:55 Starting compiler/inference/proofs
Jan 10 14:07:57 Finished compiler/inference/proofs                                1s  20MB
Jan 10 14:07:57 Starting compiler/backend/semantics
Jan 10 14:09:11 Finished compiler/backend/semantics                            1m13s   1GB
Jan 10 14:09:11 Starting compiler/backend/reg_alloc/proofs
Jan 10 14:09:13 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Jan 10 14:09:13 Starting compiler/backend/proofs
Jan 10 14:10:12 Finished compiler/backend/proofs                                 58s   3GB
Jan 10 14:10:12 Starting compiler/backend/serialiser
Jan 10 14:10:15 Finished compiler/backend/serialiser                              2s  29MB
Jan 10 14:10:15 Starting compiler/encoders/x64/proofs
Jan 10 14:20:09 Finished compiler/encoders/x64/proofs                          9m54s   5GB
Jan 10 14:20:09 Starting compiler/encoders/arm7/proofs
Jan 10 14:33:45 Finished compiler/encoders/arm7/proofs                        13m35s   5GB
Jan 10 14:33:45 Starting compiler/encoders/arm8/proofs
Jan 10 14:40:39 Finished compiler/encoders/arm8/proofs                         6m54s   1GB
Jan 10 14:40:39 Starting compiler/encoders/arm8_asl/proofs
Jan 10 15:32:46 Finished compiler/encoders/arm8_asl/proofs                    52m05s   5GB
Jan 10 15:32:46 Starting compiler/encoders/mips/proofs
Jan 10 15:43:33 Finished compiler/encoders/mips/proofs                        10m47s   2GB
Jan 10 15:43:33 Starting compiler/encoders/riscv/proofs
Jan 10 15:52:29 Finished compiler/encoders/riscv/proofs                        8m56s   2GB
Jan 10 15:52:30 Starting compiler/encoders/ag32/proofs
Jan 10 15:55:06 Finished compiler/encoders/ag32/proofs                         2m36s   1GB
Jan 10 15:55:06 Starting compiler/backend/x64/proofs
Jan 10 15:55:37 Finished compiler/backend/x64/proofs                             31s   2GB
Jan 10 15:55:37 Starting compiler/backend/arm7/proofs
Jan 10 15:56:11 Finished compiler/backend/arm7/proofs                            33s   2GB
Jan 10 15:56:11 Starting compiler/backend/arm8/proofs
Jan 10 15:56:40 Finished compiler/backend/arm8/proofs                            29s   1GB
Jan 10 15:56:40 Starting compiler/backend/arm8_asl
Jan 10 15:57:04 Finished compiler/backend/arm8_asl                               23s   1GB
Jan 10 15:57:04 Starting compiler/backend/mips/proofs
Jan 10 15:57:35 Finished compiler/backend/mips/proofs                            31s   2GB
Jan 10 15:57:35 Starting compiler/backend/riscv/proofs
Jan 10 15:58:09 Finished compiler/backend/riscv/proofs                           34s   2GB
Jan 10 15:58:09 Starting compiler/backend/ag32/proofs
Jan 10 16:11:43 Finished compiler/backend/ag32/proofs                         13m33s   3GB
Jan 10 16:11:43 Starting candle/set-theory
Jan 10 16:12:22 Finished candle/set-theory                                       38s   1GB
Jan 10 16:12:22 Starting candle/syntax-lib
Jan 10 16:12:23 Finished candle/syntax-lib                                        1s  19MB
Jan 10 16:12:24 Starting candle/standard/syntax
Jan 10 16:12:34 Finished candle/standard/syntax                                  10s 675MB
Jan 10 16:12:35 Starting candle/standard/semantics
Jan 10 16:14:33 Finished candle/standard/semantics                             1m58s   1GB
Jan 10 16:14:33 Starting candle/standard/monadic
Jan 10 16:14:35 Finished candle/standard/monadic                                  1s  22MB
Jan 10 16:14:35 Starting candle/standard/ml_kernel
Jan 10 16:16:09 Finished candle/standard/ml_kernel                             1m33s   4GB
Jan 10 16:16:09 Starting candle/overloading/syntax
Jan 10 16:19:28 Finished candle/overloading/syntax                             3m19s   1GB
Jan 10 16:19:28 Starting candle/overloading/semantics
Jan 10 16:31:35 Finished candle/overloading/semantics                         12m05s   2GB
Jan 10 16:31:35 Starting candle/overloading/monadic
Jan 10 16:34:14 Finished candle/overloading/monadic                            2m37s   1GB
Jan 10 16:34:14 Starting candle/overloading/ml_kernel
Jan 10 16:41:48 Finished candle/overloading/ml_kernel                          7m34s   4GB
Jan 10 16:41:48 Starting candle/overloading/ml_checker
Jan 10 16:44:22 Finished candle/overloading/ml_checker                         2m33s   3GB
Jan 10 16:44:22 Starting candle/prover
Jan 10 16:54:12 Finished candle/prover                                         9m49s   3GB
Jan 10 16:54:12 Starting pancake
Jan 10 16:57:37 Finished pancake                                               3m24s   5GB
Jan 10 16:57:38 Starting pancake/ffi
Jan 10 16:57:38 Finished pancake/ffi                                              0s  13MB
Jan 10 16:57:38 Starting pancake/semantics
Jan 10 17:00:08 Finished pancake/semantics                                     2m29s   1GB
Jan 10 17:00:08 Starting pancake/proofs
Jan 10 17:03:16 Finished pancake/proofs                                        3m07s   2GB
Jan 10 17:03:16 Starting characteristic/examples
Jan 10 17:04:42 Finished characteristic/examples                               1m26s   2GB
Jan 10 17:04:42 Starting tutorial/solutions
Jan 10 17:19:50 Finished tutorial/solutions                                   15m07s   9GB
Jan 10 17:19:50 Starting translator/monadic/examples
Jan 10 17:23:54 Finished translator/monadic/examples                           4m04s   2GB
Jan 10 17:23:54 Starting examples
Jan 10 17:34:28 Finished examples                                             10m30s   4GB
Jan 10 17:34:28 Starting examples/compilation/x64
Jan 10 19:34:41 Finished examples/compilation/x64                           2h00m10s  13GB
Jan 10 19:34:41 Starting examples/compilation/x64/proofs
Jan 10 19:37:12 Finished examples/compilation/x64/proofs                       2m31s   4GB
Jan 10 19:37:13 Starting examples/compilation/ag32
Jan 10 20:07:37 Finished examples/compilation/ag32                            30m24s   7GB
Jan 10 20:07:37 Starting examples/compilation/ag32/proofs
Jan 10 20:08:39 Finished examples/compilation/ag32/proofs                      1m01s   4GB
Jan 10 20:08:39 Starting examples/compilation/to_word
Jan 10 20:12:01 Finished examples/compilation/to_word                          3m21s   6GB
Jan 10 20:12:01 Starting examples/lpr_checker
Jan 10 20:13:05 Finished examples/lpr_checker                                  1m03s   1GB
Jan 10 20:13:05 Starting examples/lpr_checker/array
Jan 10 20:47:36 Finished examples/lpr_checker/array                           34m30s   6GB
Jan 10 20:47:36 Starting examples/lpr_checker/array/compilation
Jan 10 21:26:04 Finished examples/lpr_checker/array/compilation               38m27s  25GB
Jan 10 21:26:04 Starting examples/lpr_checker/array/compilation/proofs
Jan 10 21:27:35 Finished examples/lpr_checker/array/compilation/proofs         1m30s   7GB
Jan 10 21:27:35 Starting examples/opentheory
Jan 10 21:38:12 Finished examples/opentheory                                  10m36s   4GB
Jan 10 21:38:12 Starting examples/opentheory
Jan 10 21:38:14 Finished examples/opentheory                                      1s  27MB
Jan 10 21:38:14 Starting examples/opentheory/compilation
Jan 10 22:14:15 Finished examples/opentheory/compilation                      35m59s  29GB
Jan 10 22:14:15 Starting examples/opentheory/compilation/proofs
Jan 10 22:15:17 Finished examples/opentheory/compilation/proofs                1m02s   4GB
Jan 10 22:15:17 Starting examples/opentheory/compilation/ag32
Jan 10 22:47:38 Finished examples/opentheory/compilation/ag32                 32m20s  28GB
Jan 10 22:47:38 Starting examples/opentheory/compilation/ag32/proofs
Jan 10 22:49:32 Finished examples/opentheory/compilation/ag32/proofs           1m53s   7GB
Jan 10 22:49:32 Starting examples/sat_encodings
Jan 10 22:51:31 Finished examples/sat_encodings                                1m59s 824MB
Jan 10 22:51:31 Starting examples/sat_encodings/case_studies
Jan 10 22:53:20 Finished examples/sat_encodings/case_studies                   1m48s 977MB
Jan 10 22:53:20 Starting examples/sat_encodings/translation
Jan 10 22:59:16 Finished examples/sat_encodings/translation                    5m55s   4GB
Jan 10 22:59:16 Starting examples/sat_encodings/translation/compilation
Jan 10 23:44:45 Finished examples/sat_encodings/translation/compilation       45m28s  21GB
Jan 10 23:44:45 Starting examples/deflate
Jan 10 23:45:46 Finished examples/deflate                                      1m00s   1GB
Jan 10 23:45:46 Starting examples/deflate/translation
Jan 10 23:47:22 Finished examples/deflate/translation                          1m35s   2GB
Jan 10 23:47:22 Starting examples/deflate/translation/compilation
Jan 11 00:06:49 Finished examples/deflate/translation/compilation             19m27s  11GB
Jan 11 00:06:49 Starting translator/okasaki-examples
Jan 11 00:12:00 Finished translator/okasaki-examples                           5m10s   2GB
Jan 11 00:12:00 Starting translator/other-examples
Jan 11 00:14:40 Finished translator/other-examples                             2m39s   1GB
Jan 11 00:14:40 Starting compiler/parsing/tests
Jan 11 00:15:12 Finished compiler/parsing/tests                                  32s 755MB
Jan 11 00:15:13 Starting compiler/inference/tests
Jan 11 00:23:39 Finished compiler/inference/tests                              8m26s   5GB
Jan 11 00:23:39 Starting compiler/printing/test
Jan 11 00:27:08 Finished compiler/printing/test                                3m28s   3GB
Jan 11 00:27:08 Starting icing/flover
Jan 11 01:09:37 Finished icing/flover                                         42m27s   2GB
Jan 11 01:09:37 Starting icing/
Jan 11 02:09:50 Finished icing/                                             1h00m09s   9GB
Jan 11 02:09:50 Starting icing/examples
Jan 11 02:11:42 Finished icing/examples                                        1m52s   7GB
Jan 11 02:11:42 Starting compiler/repl
Jan 11 02:20:16 Finished compiler/repl                                         8m33s   4GB
Jan 11 02:20:16 Starting unverified/sexpr-bootstrap/x64/64
Jan 11 02:33:08 Finished unverified/sexpr-bootstrap/x64/64                    12m48s  14GB
Jan 11 02:33:08 Starting unverified/sexpr-bootstrap/x64/32
Jan 11 02:43:27 Finished unverified/sexpr-bootstrap/x64/32                    10m15s  13GB
Jan 11 02:43:27 Starting compiler/benchmarks
Jan 11 02:43:31 Finished compiler/benchmarks                                      4s  34MB
Jan 11 02:43:31 Starting compiler/bootstrap/compilation/x64/64
Jan 11 13:43:13 Finished compiler/bootstrap/compilation/x64/64             10h59m39s  64GB
Jan 11 13:43:13 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 11 14:03:34 Finished compiler/bootstrap/compilation/x64/64/proofs         20m21s  30GB
Jan 11 14:03:35 Starting compiler/bootstrap/compilation/x64/32
Jan 11 20:57:12 Finished compiler/bootstrap/compilation/x64/32              6h53m35s  46GB
Jan 11 20:57:12 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 11 21:00:04 Finished compiler/bootstrap/compilation/x64/32/proofs          2m51s  17GB
Jan 11 21:00:04 Starting compiler/bootstrap/compilation/ag32/32
Jan 12 03:41:38 Finished compiler/bootstrap/compilation/ag32/32             6h41m33s  64GB
Jan 12 03:41:38 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 12 03:47:45 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m06s  31GB
Jan 12 03:47:45 SUCCESS