Job 2291

CakeML:b76383b2a589101f171319130980075afdc90158
  Fix data_to_word_assignProof given integer$Num rewrites changes [Jan 30 06:21:36]
HOL:02b18c783478fd195ee64f2aa9bddd1666105bbb
  Link new padics example into release notes and examples build [Jan 29 04:14:04]
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

Jan 30 06:26:02 Claimed job
Jan 30 06:26:06 Building HOL
Jan 30 06:39:53 Starting developers
Jan 30 06:39:58 Finished developers                                               5s 144MB
Jan 30 06:39:59 Starting developers/bin
Jan 30 06:40:05 Finished developers/bin                                           5s   1GB
Jan 30 06:40:05 Starting compiler/proofs
Jan 30 08:33:45 Finished compiler/proofs                                    1h53m40s  17GB
Jan 30 08:33:45 Starting compiler/bootstrap/translation
Jan 30 16:46:15 Finished compiler/bootstrap/translation                     8h12m29s  42GB
Jan 30 16:46:15 Starting semantics/ffi
Jan 30 16:46:20 Finished semantics/ffi                                            4s 376MB
Jan 30 16:46:20 Starting semantics
Jan 30 16:46:21 Finished semantics                                                1s  18MB
Jan 30 16:46:21 Starting semantics/proofs
Jan 30 16:46:54 Finished semantics/proofs                                        32s 750MB
Jan 30 16:46:54 Starting semantics/alt_semantics
Jan 30 16:47:26 Finished semantics/alt_semantics                                 32s 751MB
Jan 30 16:47:26 Starting semantics/alt_semantics/proofs
Jan 30 16:59:24 Finished semantics/alt_semantics/proofs                       11m58s   1GB
Jan 30 16:59:24 Starting basis/pure
Jan 30 16:59:26 Finished basis/pure                                               1s  24MB
Jan 30 16:59:26 Starting translator
Jan 30 17:01:13 Finished translator                                            1m47s   2GB
Jan 30 17:01:13 Starting compiler/parsing
Jan 30 17:01:15 Finished compiler/parsing                                         1s  17MB
Jan 30 17:01:15 Starting characteristic
Jan 30 17:01:17 Finished characteristic                                           1s  22MB
Jan 30 17:01:17 Starting translator/monadic
Jan 30 17:01:19 Finished translator/monadic                                       1s  21MB
Jan 30 17:01:19 Starting basis
Jan 30 17:05:04 Finished basis                                                 3m44s   3GB
Jan 30 17:05:04 Starting compiler/inference
Jan 30 17:05:06 Finished compiler/inference                                       1s  22MB
Jan 30 17:05:06 Starting compiler/backend/reg_alloc
Jan 30 17:05:08 Finished compiler/backend/reg_alloc                               1s  19MB
Jan 30 17:05:08 Starting compiler/backend/gc
Jan 30 17:05:10 Finished compiler/backend/gc                                      2s  23MB
Jan 30 17:05:10 Starting compiler/backend
Jan 30 17:05:23 Finished compiler/backend                                        12s 791MB
Jan 30 17:05:23 Starting compiler/encoders/asm
Jan 30 17:05:25 Finished compiler/encoders/asm                                    1s  20MB
Jan 30 17:05:25 Starting compiler/encoders/x64
Jan 30 17:05:27 Finished compiler/encoders/x64                                    1s  21MB
Jan 30 17:05:27 Starting compiler/encoders/arm7
Jan 30 17:05:29 Finished compiler/encoders/arm7                                   1s  24MB
Jan 30 17:05:29 Starting compiler/encoders/arm8
Jan 30 17:05:31 Finished compiler/encoders/arm8                                   1s  26MB
Jan 30 17:05:31 Starting compiler/encoders/arm8_asl
Jan 30 19:31:55 Finished compiler/encoders/arm8_asl                         2h26m24s  40GB
Jan 30 19:31:56 Starting compiler/encoders/mips
Jan 30 19:31:58 Finished compiler/encoders/mips                                   1s  18MB
Jan 30 19:31:58 Starting compiler/encoders/riscv
Jan 30 19:32:00 Finished compiler/encoders/riscv                                  1s  24MB
Jan 30 19:32:00 Starting compiler/encoders/ag32
Jan 30 19:32:02 Finished compiler/encoders/ag32                                   1s  27MB
Jan 30 19:32:02 Starting compiler/backend/x64
Jan 30 19:32:04 Finished compiler/backend/x64                                     2s  22MB
Jan 30 19:32:04 Starting compiler/backend/arm7
Jan 30 19:32:06 Finished compiler/backend/arm7                                    2s  24MB
Jan 30 19:32:07 Starting compiler/backend/arm8
Jan 30 19:32:09 Finished compiler/backend/arm8                                    2s  25MB
Jan 30 19:32:09 Starting compiler/backend/mips
Jan 30 19:32:11 Finished compiler/backend/mips                                    2s  26MB
Jan 30 19:32:11 Starting compiler/backend/riscv
Jan 30 19:32:14 Finished compiler/backend/riscv                                   2s  29MB
Jan 30 19:32:14 Starting compiler/backend/ag32
Jan 30 19:33:40 Finished compiler/backend/ag32                                 1m25s   1GB
Jan 30 19:33:40 Starting compiler/parsing/proofs
Jan 30 19:33:41 Finished compiler/parsing/proofs                                  1s  17MB
Jan 30 19:33:41 Starting compiler/inference/proofs
Jan 30 19:33:43 Finished compiler/inference/proofs                                1s  19MB
Jan 30 19:33:44 Starting compiler/backend/semantics
Jan 30 19:34:57 Finished compiler/backend/semantics                            1m13s   1GB
Jan 30 19:34:57 Starting compiler/backend/reg_alloc/proofs
Jan 30 19:34:59 Finished compiler/backend/reg_alloc/proofs                        1s  19MB
Jan 30 19:34:59 Starting compiler/backend/proofs
Jan 30 19:36:01 Finished compiler/backend/proofs                               1m01s   3GB
Jan 30 19:36:01 Starting compiler/backend/serialiser
Jan 30 19:36:04 Finished compiler/backend/serialiser                              2s  38MB
Jan 30 19:36:05 Starting compiler/encoders/x64/proofs
Jan 30 19:45:52 Finished compiler/encoders/x64/proofs                          9m47s   6GB
Jan 30 19:45:52 Starting compiler/encoders/arm7/proofs
Jan 30 19:59:30 Finished compiler/encoders/arm7/proofs                        13m37s   6GB
Jan 30 19:59:30 Starting compiler/encoders/arm8/proofs
Jan 30 20:06:29 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Jan 30 20:06:29 Starting compiler/encoders/arm8_asl/proofs
Jan 30 20:59:22 Finished compiler/encoders/arm8_asl/proofs                    52m52s  12GB
Jan 30 20:59:22 Starting compiler/encoders/mips/proofs
Jan 30 21:10:13 Finished compiler/encoders/mips/proofs                        10m50s   2GB
Jan 30 21:10:13 Starting compiler/encoders/riscv/proofs
Jan 30 21:19:03 Finished compiler/encoders/riscv/proofs                        8m49s   2GB
Jan 30 21:19:03 Starting compiler/encoders/ag32/proofs
Jan 30 21:21:36 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Jan 30 21:21:36 Starting compiler/backend/x64/proofs
Jan 30 21:22:07 Finished compiler/backend/x64/proofs                             31s   2GB
Jan 30 21:22:07 Starting compiler/backend/arm7/proofs
Jan 30 21:22:40 Finished compiler/backend/arm7/proofs                            33s   2GB
Jan 30 21:22:41 Starting compiler/backend/arm8/proofs
Jan 30 21:23:11 Finished compiler/backend/arm8/proofs                            30s   1GB
Jan 30 21:23:11 Starting compiler/backend/arm8_asl
Jan 30 21:23:35 Finished compiler/backend/arm8_asl                               24s   1GB
Jan 30 21:23:35 Starting compiler/backend/mips/proofs
Jan 30 21:24:07 Finished compiler/backend/mips/proofs                            31s   1GB
Jan 30 21:24:07 Starting compiler/backend/riscv/proofs
Jan 30 21:24:42 Finished compiler/backend/riscv/proofs                           34s   2GB
Jan 30 21:24:42 Starting compiler/backend/ag32/proofs
Jan 30 21:38:32 Finished compiler/backend/ag32/proofs                         13m49s   3GB
Jan 30 21:38:32 Starting candle/set-theory
Jan 30 21:39:11 Finished candle/set-theory                                       39s   1GB
Jan 30 21:39:12 Starting candle/syntax-lib
Jan 30 21:39:13 Finished candle/syntax-lib                                        1s  19MB
Jan 30 21:39:13 Starting candle/standard/syntax
Jan 30 21:39:24 Finished candle/standard/syntax                                  10s 770MB
Jan 30 21:39:24 Starting candle/standard/semantics
Jan 30 21:41:22 Finished candle/standard/semantics                             1m58s   1GB
Jan 30 21:41:22 Starting candle/standard/monadic
Jan 30 21:41:24 Finished candle/standard/monadic                                  1s  22MB
Jan 30 21:41:24 Starting candle/standard/ml_kernel
Jan 30 21:43:04 Finished candle/standard/ml_kernel                             1m39s   2GB
Jan 30 21:43:04 Starting candle/overloading/syntax
Jan 30 21:46:30 Finished candle/overloading/syntax                             3m25s   1GB
Jan 30 21:46:30 Starting candle/overloading/semantics
Jan 30 21:58:44 Finished candle/overloading/semantics                         12m13s   2GB
Jan 30 21:58:44 Starting candle/overloading/monadic
Jan 30 22:01:27 Finished candle/overloading/monadic                            2m42s   1GB
Jan 30 22:01:27 Starting candle/overloading/ml_kernel
Jan 30 22:09:33 Finished candle/overloading/ml_kernel                          8m05s   3GB
Jan 30 22:09:33 Starting candle/overloading/ml_checker
Jan 30 22:12:07 Finished candle/overloading/ml_checker                         2m33s   4GB
Jan 30 22:12:07 Starting candle/prover
Jan 30 22:22:20 Finished candle/prover                                        10m12s   4GB
Jan 30 22:22:20 Starting pancake
Jan 30 22:23:06 Finished pancake                                                 45s 881MB
Jan 30 22:23:06 Starting pancake/ffi
Jan 30 22:23:06 Finished pancake/ffi                                              0s  13MB
Jan 30 22:23:07 Starting pancake/semantics
Jan 30 22:25:33 Finished pancake/semantics                                     2m26s   1GB
Jan 30 22:25:33 Starting pancake/parser
Jan 30 22:25:55 Finished pancake/parser                                          22s 704MB
Jan 30 22:25:56 Starting pancake/proofs
Jan 30 22:59:42 Finished pancake/proofs                                       33m45s   4GB
Jan 30 22:59:42 Starting characteristic/examples
Jan 30 23:01:17 Finished characteristic/examples                               1m35s   3GB
Jan 30 23:01:17 Starting tutorial/solutions
Jan 30 23:17:11 Finished tutorial/solutions                                   15m53s  11GB
Jan 30 23:17:11 Starting translator/monadic/examples
Jan 30 23:21:19 Finished translator/monadic/examples                           4m07s   2GB
Jan 30 23:21:19 Starting examples
Jan 30 23:37:34 Finished examples                                             16m14s   4GB
Jan 30 23:37:34 Starting examples/compilation/x64
Jan 31 01:37:37 Finished examples/compilation/x64                           2h00m02s  21GB
Jan 31 01:37:37 Starting examples/compilation/x64/proofs
Jan 31 01:40:11 Finished examples/compilation/x64/proofs                       2m34s   4GB
Jan 31 01:40:11 Starting examples/compilation/ag32
Jan 31 02:10:23 Finished examples/compilation/ag32                            30m12s   9GB
Jan 31 02:10:24 Starting examples/compilation/ag32/proofs
Jan 31 02:11:29 Finished examples/compilation/ag32/proofs                      1m05s   5GB
Jan 31 02:11:29 Starting examples/compilation/to_word
Jan 31 02:14:51 Finished examples/compilation/to_word                          3m21s   6GB
Jan 31 02:14:52 Starting examples/lpr_checker
Jan 31 02:15:58 Finished examples/lpr_checker                                  1m05s   1GB
Jan 31 02:15:58 Starting examples/lpr_checker/array
Jan 31 02:46:56 Finished examples/lpr_checker/array                           30m57s   6GB
Jan 31 02:46:56 Starting examples/lpr_checker/array/compilation
Jan 31 03:39:06 Finished examples/lpr_checker/array/compilation               52m09s  23GB
Jan 31 03:39:06 Starting examples/lpr_checker/array/compilation/proofs
Jan 31 03:41:08 Finished examples/lpr_checker/array/compilation/proofs         2m02s   3GB
Jan 31 03:41:09 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 31 03:51:18 Finished examples/lpr_checker/array/compilation/proofsARM8    10m08s  23GB
Jan 31 03:51:18 Starting examples/pseudo_bool
Jan 31 03:53:11 Finished examples/pseudo_bool                                  1m53s   1GB
Jan 31 03:53:11 Starting examples/pseudo_bool/cnf_encoding
Jan 31 03:53:37 Finished examples/pseudo_bool/cnf_encoding                       25s 699MB
Jan 31 03:53:37 Starting examples/pseudo_bool/graph_encoding
Jan 31 03:54:20 Finished examples/pseudo_bool/graph_encoding                     43s 770MB
Jan 31 03:54:20 Starting examples/pseudo_bool/array
Jan 31 04:52:13 Finished examples/pseudo_bool/array                           57m52s   6GB
Jan 31 04:52:13 Starting examples/pseudo_bool/array/compilation
Jan 31 08:11:18 Finished examples/pseudo_bool/array/compilation             3h19m04s  31GB
Jan 31 08:11:18 Starting examples/pseudo_bool/array/compilation/proofs
Jan 31 08:14:17 Finished examples/pseudo_bool/array/compilation/proofs         2m58s   5GB
Jan 31 08:14:17 Starting examples/opentheory
Jan 31 08:25:11 Finished examples/opentheory                                  10m54s   5GB
Jan 31 08:25:11 Starting examples/opentheory
Jan 31 08:25:13 Finished examples/opentheory                                      1s  25MB
Jan 31 08:25:13 Starting examples/opentheory/compilation
Jan 31 09:02:16 Finished examples/opentheory/compilation                      37m02s  32GB
Jan 31 09:02:16 Starting examples/opentheory/compilation/proofs
Jan 31 09:03:20 Finished examples/opentheory/compilation/proofs                1m04s   4GB
Jan 31 09:03:20 Starting examples/opentheory/compilation/ag32
Jan 31 09:36:24 Finished examples/opentheory/compilation/ag32                 33m04s  27GB
Jan 31 09:36:24 Starting examples/opentheory/compilation/ag32/proofs
Jan 31 09:38:20 Finished examples/opentheory/compilation/ag32/proofs           1m55s   7GB
Jan 31 09:38:20 Starting examples/sat_encodings
Jan 31 09:40:25 Finished examples/sat_encodings                                2m04s 873MB
Jan 31 09:40:25 Starting examples/sat_encodings/case_studies
Jan 31 09:42:12 Finished examples/sat_encodings/case_studies                   1m47s   1GB
Jan 31 09:42:12 Starting examples/sat_encodings/translation
Jan 31 09:48:28 Finished examples/sat_encodings/translation                    6m15s   5GB
Jan 31 09:48:28 Starting examples/sat_encodings/translation/compilation
Jan 31 10:34:48 Finished examples/sat_encodings/translation/compilation       46m19s  21GB
Jan 31 10:34:48 Starting examples/deflate
Jan 31 10:35:51 Finished examples/deflate                                      1m02s   1GB
Jan 31 10:35:51 Starting examples/deflate/translation
Jan 31 10:37:48 Finished examples/deflate/translation                          1m56s   3GB
Jan 31 10:37:48 Starting examples/deflate/translation/compilation
Jan 31 10:57:55 Finished examples/deflate/translation/compilation             20m06s  14GB
Jan 31 10:57:55 Starting examples/vipr
Jan 31 11:02:01 Finished examples/vipr                                         4m05s   4GB
Jan 31 11:02:01 Starting examples/vipr/compilation
Jan 31 11:23:11 Finished examples/vipr/compilation                            21m09s  16GB
Jan 31 11:23:11 Starting translator/okasaki-examples
Jan 31 11:28:22 Finished translator/okasaki-examples                           5m11s   2GB
Jan 31 11:28:22 Starting translator/other-examples
Jan 31 11:31:56 Finished translator/other-examples                             3m33s   1GB
Jan 31 11:31:56 Starting compiler/parsing/tests
Jan 31 11:32:29 Finished compiler/parsing/tests                                  33s   1GB
Jan 31 11:32:29 Starting compiler/inference/tests
Jan 31 11:41:01 Finished compiler/inference/tests                              8m31s   6GB
Jan 31 11:41:01 Starting compiler/printing/test
Jan 31 11:44:51 Finished compiler/printing/test                                3m49s   3GB
Jan 31 11:44:51 Starting icing/flover
Jan 31 12:29:30 Finished icing/flover                                         44m39s   1GB
Jan 31 12:29:30 Starting icing/
Jan 31 13:23:46 Finished icing/                                               54m15s   7GB
Jan 31 13:23:46 Starting icing/examples
Jan 31 13:25:23 Finished icing/examples                                        1m36s   2GB
Jan 31 13:25:23 Starting compiler/repl
Jan 31 13:34:11 Finished compiler/repl                                         8m47s   5GB
Jan 31 13:34:11 Starting unverified/sexpr-bootstrap/x64/64
Jan 31 13:47:52 Finished unverified/sexpr-bootstrap/x64/64                    13m40s  13GB
Jan 31 13:47:52 Starting unverified/sexpr-bootstrap/x64/32
Jan 31 13:58:48 Finished unverified/sexpr-bootstrap/x64/32                    10m55s  14GB
Jan 31 13:58:49 Starting compiler/benchmarks
Jan 31 14:14:28 Finished compiler/benchmarks                                  15m39s   2GB
Jan 31 14:14:28 Starting compiler/bootstrap/compilation/x64/64
Feb 01 02:16:45 Finished compiler/bootstrap/compilation/x64/64             12h02m16s  64GB
Feb 01 02:16:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 01 02:37:37 Finished compiler/bootstrap/compilation/x64/64/proofs         20m51s  39GB
Feb 01 02:37:37 Starting compiler/bootstrap/compilation/x64/32
Feb 01 09:58:59 Finished compiler/bootstrap/compilation/x64/32              7h21m21s  64GB
Feb 01 09:58:59 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 01 10:01:52 Finished compiler/bootstrap/compilation/x64/32/proofs          2m52s  19GB
Feb 01 10:01:52 Starting compiler/bootstrap/compilation/ag32/32
Feb 01 17:22:18 Finished compiler/bootstrap/compilation/ag32/32             7h20m25s  64GB
Feb 01 17:22:19 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 01 17:29:16 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m57s  44GB
Feb 01 17:29:16 SUCCESS