Job 2292

CakeML:b76383b2a589101f171319130980075afdc90158
  Fix data_to_word_assignProof given integer$Num rewrites changes [Jan 30 06:21:36]
HOL:e1d4cc75edea2fa5a722e5775ffe85178b976b38
  Add a paragraph on Keccak to next-release [Feb 01 22:32:30]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Feb 02 16:49:26 Claimed job
Feb 02 16:49:33 Building HOL
Feb 02 17:03:27 Starting developers
Feb 02 17:03:32 Finished developers                                               5s 118MB
Feb 02 17:03:33 Starting developers/bin
Feb 02 17:03:39 Finished developers/bin                                           6s   1GB
Feb 02 17:03:39 Starting compiler/proofs
Feb 05 09:16:30 Resuming compiler/proofs
Feb 05 10:38:49 Finished compiler/proofs                                    1h22m19s  16GB
Feb 05 10:38:50 Starting compiler/bootstrap/translation
Feb 05 18:50:15 Finished compiler/bootstrap/translation                     8h11m25s  37GB
Feb 05 18:50:15 Starting semantics/ffi
Feb 05 18:50:21 Finished semantics/ffi                                            5s 218MB
Feb 05 18:50:21 Starting semantics
Feb 05 18:50:23 Finished semantics                                                1s  20MB
Feb 05 18:50:23 Starting semantics/proofs
Feb 05 18:50:56 Finished semantics/proofs                                        32s 729MB
Feb 05 18:50:56 Starting semantics/alt_semantics
Feb 05 18:51:28 Finished semantics/alt_semantics                                 32s 778MB
Feb 05 18:51:29 Starting semantics/alt_semantics/proofs
Feb 05 19:03:28 Finished semantics/alt_semantics/proofs                       11m59s   1GB
Feb 05 19:03:29 Starting basis/pure
Feb 05 19:03:30 Finished basis/pure                                               1s  19MB
Feb 05 19:03:30 Starting translator
Feb 05 19:05:22 Finished translator                                            1m51s   2GB
Feb 05 19:05:22 Starting compiler/parsing
Feb 05 19:05:23 Finished compiler/parsing                                         1s  17MB
Feb 05 19:05:23 Starting characteristic
Feb 05 19:05:25 Finished characteristic                                           1s  23MB
Feb 05 19:05:26 Starting translator/monadic
Feb 05 19:05:27 Finished translator/monadic                                       1s  27MB
Feb 05 19:05:28 Starting basis
Feb 05 19:09:14 Finished basis                                                 3m46s   2GB
Feb 05 19:09:14 Starting compiler/inference
Feb 05 19:09:16 Finished compiler/inference                                       1s  22MB
Feb 05 19:09:16 Starting compiler/backend/reg_alloc
Feb 05 19:09:18 Finished compiler/backend/reg_alloc                               1s  19MB
Feb 05 19:09:18 Starting compiler/backend/gc
Feb 05 19:09:20 Finished compiler/backend/gc                                      2s  26MB
Feb 05 19:09:20 Starting compiler/backend
Feb 05 19:09:33 Finished compiler/backend                                        12s 791MB
Feb 05 19:09:33 Starting compiler/encoders/asm
Feb 05 19:09:35 Finished compiler/encoders/asm                                    1s  21MB
Feb 05 19:09:35 Starting compiler/encoders/x64
Feb 05 19:09:37 Finished compiler/encoders/x64                                    1s  24MB
Feb 05 19:09:37 Starting compiler/encoders/arm7
Feb 05 19:09:39 Finished compiler/encoders/arm7                                   1s  23MB
Feb 05 19:09:39 Starting compiler/encoders/arm8
Feb 05 19:09:41 Finished compiler/encoders/arm8                                   1s  27MB
Feb 05 19:09:41 Starting compiler/encoders/arm8_asl
Feb 05 21:34:42 Finished compiler/encoders/arm8_asl                         2h25m00s  39GB
Feb 05 21:34:42 Starting compiler/encoders/mips
Feb 05 21:34:44 Finished compiler/encoders/mips                                   1s  21MB
Feb 05 21:34:44 Starting compiler/encoders/riscv
Feb 05 21:34:46 Finished compiler/encoders/riscv                                  1s  21MB
Feb 05 21:34:46 Starting compiler/encoders/ag32
Feb 05 21:34:48 Finished compiler/encoders/ag32                                   1s  20MB
Feb 05 21:34:48 Starting compiler/backend/x64
Feb 05 21:34:50 Finished compiler/backend/x64                                     2s  25MB
Feb 05 21:34:50 Starting compiler/backend/arm7
Feb 05 21:34:52 Finished compiler/backend/arm7                                    2s  28MB
Feb 05 21:34:52 Starting compiler/backend/arm8
Feb 05 21:34:55 Finished compiler/backend/arm8                                    2s  29MB
Feb 05 21:34:55 Starting compiler/backend/mips
Feb 05 21:34:57 Finished compiler/backend/mips                                    2s  28MB
Feb 05 21:34:57 Starting compiler/backend/riscv
Feb 05 21:35:00 Finished compiler/backend/riscv                                   2s  21MB
Feb 05 21:35:00 Starting compiler/backend/ag32
Feb 05 21:36:25 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 05 21:36:25 Starting compiler/parsing/proofs
Feb 05 21:36:27 Finished compiler/parsing/proofs                                  1s  21MB
Feb 05 21:36:27 Starting compiler/inference/proofs
Feb 05 21:36:28 Finished compiler/inference/proofs                                1s  22MB
Feb 05 21:36:29 Starting compiler/backend/semantics
Feb 05 21:37:42 Finished compiler/backend/semantics                            1m13s   1GB
Feb 05 21:37:42 Starting compiler/backend/reg_alloc/proofs
Feb 05 21:37:44 Finished compiler/backend/reg_alloc/proofs                        1s  28MB
Feb 05 21:37:44 Starting compiler/backend/proofs
Feb 05 21:38:42 Finished compiler/backend/proofs                                 57s   2GB
Feb 05 21:38:42 Starting compiler/backend/serialiser
Feb 05 21:38:45 Finished compiler/backend/serialiser                              2s  36MB
Feb 05 21:38:45 Starting compiler/encoders/x64/proofs
Feb 05 21:48:37 Finished compiler/encoders/x64/proofs                          9m51s   6GB
Feb 05 21:48:37 Starting compiler/encoders/arm7/proofs
Feb 05 22:02:35 Finished compiler/encoders/arm7/proofs                        13m58s   3GB
Feb 05 22:02:35 Starting compiler/encoders/arm8/proofs
Feb 05 22:09:31 Finished compiler/encoders/arm8/proofs                         6m56s   1GB
Feb 05 22:09:31 Starting compiler/encoders/arm8_asl/proofs
Feb 05 23:01:44 Finished compiler/encoders/arm8_asl/proofs                    52m12s   6GB
Feb 05 23:01:44 Starting compiler/encoders/mips/proofs
Feb 05 23:12:26 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Feb 05 23:12:26 Starting compiler/encoders/riscv/proofs
Feb 05 23:21:11 Finished compiler/encoders/riscv/proofs                        8m45s   2GB
Feb 05 23:21:12 Starting compiler/encoders/ag32/proofs
Feb 05 23:23:45 Finished compiler/encoders/ag32/proofs                         2m33s 950MB
Feb 05 23:23:45 Starting compiler/backend/x64/proofs
Feb 05 23:24:16 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 05 23:24:16 Starting compiler/backend/arm7/proofs
Feb 05 23:24:49 Finished compiler/backend/arm7/proofs                            33s   2GB
Feb 05 23:24:49 Starting compiler/backend/arm8/proofs
Feb 05 23:25:19 Finished compiler/backend/arm8/proofs                            29s   1GB
Feb 05 23:25:19 Starting compiler/backend/arm8_asl
Feb 05 23:25:46 Finished compiler/backend/arm8_asl                               26s   1GB
Feb 05 23:25:46 Starting compiler/backend/mips/proofs
Feb 05 23:26:19 Finished compiler/backend/mips/proofs                            32s   1GB
Feb 05 23:26:19 Starting compiler/backend/riscv/proofs
Feb 05 23:26:54 Finished compiler/backend/riscv/proofs                           35s   2GB
Feb 05 23:26:54 Starting compiler/backend/ag32/proofs
Feb 05 23:40:46 Finished compiler/backend/ag32/proofs                         13m51s   3GB
Feb 05 23:40:46 Starting candle/set-theory
Feb 05 23:41:25 Finished candle/set-theory                                       39s   1GB
Feb 05 23:41:25 Starting candle/syntax-lib
Feb 05 23:41:27 Finished candle/syntax-lib                                        1s  20MB
Feb 05 23:41:27 Starting candle/standard/syntax
Feb 05 23:41:38 Finished candle/standard/syntax                                  11s 793MB
Feb 05 23:41:38 Starting candle/standard/semantics
Feb 05 23:43:37 Finished candle/standard/semantics                             1m58s   1GB
Feb 05 23:43:37 Starting candle/standard/monadic
Feb 05 23:43:39 Finished candle/standard/monadic                                  1s  23MB
Feb 05 23:43:39 Starting candle/standard/ml_kernel
Feb 05 23:45:19 Finished candle/standard/ml_kernel                             1m39s   3GB
Feb 05 23:45:19 Starting candle/overloading/syntax
Feb 05 23:48:45 Finished candle/overloading/syntax                             3m25s   1GB
Feb 05 23:48:45 Starting candle/overloading/semantics
Feb 06 00:01:04 Finished candle/overloading/semantics                         12m19s   3GB
Feb 06 00:01:04 Starting candle/overloading/monadic
Feb 06 00:03:49 Finished candle/overloading/monadic                            2m44s   1GB
Feb 06 00:03:49 Starting candle/overloading/ml_kernel
Feb 06 00:11:47 Finished candle/overloading/ml_kernel                          7m57s   3GB
Feb 06 00:11:47 Starting candle/overloading/ml_checker
Feb 06 00:14:23 Finished candle/overloading/ml_checker                         2m35s   2GB
Feb 06 00:14:23 Starting candle/prover
Feb 06 00:24:30 Finished candle/prover                                        10m07s   4GB
Feb 06 00:24:31 Starting pancake
Feb 06 00:25:17 Finished pancake                                                 46s 871MB
Feb 06 00:25:17 Starting pancake/ffi
Feb 06 00:25:18 Finished pancake/ffi                                              0s  13MB
Feb 06 00:25:18 Starting pancake/semantics
Feb 06 00:27:46 Finished pancake/semantics                                     2m28s   1GB
Feb 06 00:27:46 Starting pancake/parser
Feb 06 00:28:10 Finished pancake/parser                                          23s   1GB
Feb 06 00:28:10 Starting pancake/proofs
Feb 06 01:01:51 Finished pancake/proofs                                       33m41s   4GB
Feb 06 01:01:51 Starting characteristic/examples
Feb 06 01:03:27 Finished characteristic/examples                               1m35s   2GB
Feb 06 01:03:27 Starting tutorial/solutions
Feb 06 01:19:30 Finished tutorial/solutions                                   16m02s   7GB
Feb 06 01:19:30 Starting translator/monadic/examples
Feb 06 01:23:38 Finished translator/monadic/examples                           4m07s   3GB
Feb 06 01:23:38 Starting examples
Feb 06 01:39:48 Finished examples                                             16m09s   4GB
Feb 06 01:39:48 Starting examples/compilation/x64
Feb 06 03:39:32 Finished examples/compilation/x64                           1h59m43s  17GB
Feb 06 03:39:32 Starting examples/compilation/x64/proofs
Feb 06 03:42:10 Finished examples/compilation/x64/proofs                       2m37s   4GB
Feb 06 03:42:10 Starting examples/compilation/ag32
Feb 06 04:12:40 Finished examples/compilation/ag32                            30m29s   6GB
Feb 06 04:12:40 Starting examples/compilation/ag32/proofs
Feb 06 04:13:44 Finished examples/compilation/ag32/proofs                      1m03s   4GB
Feb 06 04:13:44 Starting examples/compilation/to_word
Feb 06 04:17:07 Finished examples/compilation/to_word                          3m23s   6GB
Feb 06 04:17:07 Starting examples/lpr_checker
Feb 06 04:18:13 Finished examples/lpr_checker                                  1m05s   1GB
Feb 06 04:18:13 Starting examples/lpr_checker/array
Feb 06 04:49:14 Finished examples/lpr_checker/array                           31m00s   6GB
Feb 06 04:49:14 Starting examples/lpr_checker/array/compilation
Feb 06 05:41:59 Finished examples/lpr_checker/array/compilation               52m44s  25GB
Feb 06 05:41:59 Starting examples/lpr_checker/array/compilation/proofs
Feb 06 05:44:05 Finished examples/lpr_checker/array/compilation/proofs         2m06s   3GB
Feb 06 05:44:05 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 06 05:56:02 Finished examples/lpr_checker/array/compilation/proofsARM8    11m56s  21GB
Feb 06 05:56:02 Starting examples/pseudo_bool
Feb 06 05:57:55 Finished examples/pseudo_bool                                  1m53s   1GB
Feb 06 05:57:56 Starting examples/pseudo_bool/cnf_encoding
Feb 06 05:58:21 Finished examples/pseudo_bool/cnf_encoding                       25s 662MB
Feb 06 05:58:21 Starting examples/pseudo_bool/graph_encoding
Feb 06 05:59:04 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Feb 06 05:59:04 Starting examples/pseudo_bool/array
Feb 06 06:57:10 Finished examples/pseudo_bool/array                           58m05s   6GB
Feb 06 06:57:10 Starting examples/pseudo_bool/array/compilation
Feb 06 10:15:41 Finished examples/pseudo_bool/array/compilation             3h18m30s  32GB
Feb 06 10:15:41 Starting examples/pseudo_bool/array/compilation/proofs
Feb 06 10:18:37 Finished examples/pseudo_bool/array/compilation/proofs         2m56s   5GB
Feb 06 10:18:37 Starting examples/opentheory
Feb 06 10:29:28 Finished examples/opentheory                                  10m50s   6GB
Feb 06 10:29:28 Starting examples/opentheory
Feb 06 10:29:30 Finished examples/opentheory                                      1s  26MB
Feb 06 10:29:30 Starting examples/opentheory/compilation
Feb 06 11:06:55 Finished examples/opentheory/compilation                      37m25s  31GB
Feb 06 11:06:56 Starting examples/opentheory/compilation/proofs
Feb 06 11:07:59 Finished examples/opentheory/compilation/proofs                1m03s   4GB
Feb 06 11:07:59 Starting examples/opentheory/compilation/ag32
Feb 06 11:41:13 Finished examples/opentheory/compilation/ag32                 33m12s  26GB
Feb 06 11:41:13 Starting examples/opentheory/compilation/ag32/proofs
Feb 06 11:43:10 Finished examples/opentheory/compilation/ag32/proofs           1m57s   8GB
Feb 06 11:43:10 Starting examples/sat_encodings
Feb 06 11:45:14 Finished examples/sat_encodings                                2m03s   1GB
Feb 06 11:45:14 Starting examples/sat_encodings/case_studies
Feb 06 11:47:03 Finished examples/sat_encodings/case_studies                   1m48s   1GB
Feb 06 11:47:03 Starting examples/sat_encodings/translation
Feb 06 11:53:26 Finished examples/sat_encodings/translation                    6m22s   5GB
Feb 06 11:53:26 Starting examples/sat_encodings/translation/compilation
Feb 06 12:40:02 Finished examples/sat_encodings/translation/compilation       46m35s  22GB
Feb 06 12:40:02 Starting examples/deflate
Feb 06 12:41:02 Finished examples/deflate                                      1m00s 839MB
Feb 06 12:41:02 Starting examples/deflate/translation
Feb 06 12:42:57 Finished examples/deflate/translation                          1m54s   3GB
Feb 06 12:42:57 Starting examples/deflate/translation/compilation
Feb 06 13:03:05 Finished examples/deflate/translation/compilation             20m08s  14GB
Feb 06 13:03:05 Starting examples/vipr
Feb 06 13:07:11 Finished examples/vipr                                         4m05s   5GB
Feb 06 13:07:11 Starting examples/vipr/compilation
Feb 06 13:28:18 Finished examples/vipr/compilation                            21m06s  18GB
Feb 06 13:28:18 Starting translator/okasaki-examples
Feb 06 13:33:28 Finished translator/okasaki-examples                           5m09s   2GB
Feb 06 13:33:28 Starting translator/other-examples
Feb 06 13:37:03 Finished translator/other-examples                             3m35s   1GB
Feb 06 13:37:03 Starting compiler/parsing/tests
Feb 06 13:37:35 Finished compiler/parsing/tests                                  32s 938MB
Feb 06 13:37:35 Starting compiler/inference/tests
Feb 06 13:46:19 Finished compiler/inference/tests                              8m43s   4GB
Feb 06 13:46:19 Starting compiler/printing/test
Feb 06 13:50:12 Finished compiler/printing/test                                3m52s   3GB
Feb 06 13:50:12 Starting icing/flover
Feb 06 14:34:35 Finished icing/flover                                         44m22s   2GB
Feb 06 14:34:35 Starting icing/
Feb 06 15:29:22 Finished icing/                                               54m46s   7GB
Feb 06 15:29:22 Starting icing/examples
Feb 06 15:31:02 Finished icing/examples                                        1m40s   4GB
Feb 06 15:31:02 Starting compiler/repl
Feb 06 15:39:50 Finished compiler/repl                                         8m47s   5GB
Feb 06 15:39:50 Starting unverified/sexpr-bootstrap/x64/64
Feb 06 15:53:43 Finished unverified/sexpr-bootstrap/x64/64                    13m52s  15GB
Feb 06 15:53:43 Starting unverified/sexpr-bootstrap/x64/32
Feb 06 16:04:54 Finished unverified/sexpr-bootstrap/x64/32                    11m10s  12GB
Feb 06 16:04:55 Starting compiler/benchmarks
Feb 06 16:20:31 Finished compiler/benchmarks                                  15m36s   2GB
Feb 06 16:20:31 Starting compiler/bootstrap/compilation/x64/64
Feb 07 04:44:57 Finished compiler/bootstrap/compilation/x64/64             12h24m25s  63GB
Feb 07 04:44:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 07 05:05:55 Finished compiler/bootstrap/compilation/x64/64/proofs         20m56s  20GB
Feb 07 05:05:55 Starting compiler/bootstrap/compilation/x64/32
Feb 07 12:18:40 Finished compiler/bootstrap/compilation/x64/32              7h12m44s  63GB
Feb 07 12:18:40 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 07 12:21:55 Finished compiler/bootstrap/compilation/x64/32/proofs          3m15s  19GB
Feb 07 12:21:55 Starting compiler/bootstrap/compilation/ag32/32
Feb 07 19:52:07 Finished compiler/bootstrap/compilation/ag32/32             7h30m11s  64GB
Feb 07 19:52:07 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 07 19:59:09 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m01s  31GB
Feb 07 19:59:09 SUCCESS