Job 2283

CakeML:e026a91d58aabda091e58bb8b4b8ca67b192f07c
  Fix mlvector given changes in HOL [Jan 17 02:43:46]
HOL:9cad9796b244296e244411fc6c6d33db5b2e0f31
  [rich_list] Added characterisation of IS_PREFIX in terms of TAKE [Jan 24 22:36:21]
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 26 08:21:40 Claimed job
Jan 26 08:21:42 Reusing HOL
Jan 26 08:22:23 Starting developers
Jan 26 08:22:28 Finished developers                                               5s 144MB
Jan 26 08:22:28 Starting developers/bin
Jan 26 08:22:34 Finished developers/bin                                           5s   1GB
Jan 26 08:22:34 Starting compiler/proofs
Jan 26 10:16:22 Finished compiler/proofs                                    1h53m47s  18GB
Jan 26 10:16:23 Starting compiler/bootstrap/translation
Jan 26 18:29:42 Finished compiler/bootstrap/translation                     8h13m19s  34GB
Jan 26 18:29:43 Starting semantics/ffi
Jan 26 18:29:49 Finished semantics/ffi                                            5s 215MB
Jan 26 18:29:49 Starting semantics
Jan 26 18:29:50 Finished semantics                                                1s  17MB
Jan 26 18:29:50 Starting semantics/proofs
Jan 26 18:30:22 Finished semantics/proofs                                        31s 839MB
Jan 26 18:30:22 Starting semantics/alt_semantics
Jan 26 18:30:54 Finished semantics/alt_semantics                                 32s 890MB
Jan 26 18:30:55 Starting semantics/alt_semantics/proofs
Jan 26 18:42:49 Finished semantics/alt_semantics/proofs                       11m53s   1GB
Jan 26 18:42:49 Starting basis/pure
Jan 26 18:42:50 Finished basis/pure                                               1s  20MB
Jan 26 18:42:50 Starting translator
Jan 26 18:44:41 Finished translator                                            1m50s   2GB
Jan 26 18:44:41 Starting compiler/parsing
Jan 26 18:44:43 Finished compiler/parsing                                         1s  21MB
Jan 26 18:44:43 Starting characteristic
Jan 26 18:44:45 Finished characteristic                                           1s  21MB
Jan 26 18:44:45 Starting translator/monadic
Jan 26 18:44:47 Finished translator/monadic                                       1s  19MB
Jan 26 18:44:47 Starting basis
Jan 26 18:48:35 Finished basis                                                 3m47s   3GB
Jan 26 18:48:35 Starting compiler/inference
Jan 26 18:48:36 Finished compiler/inference                                       1s  26MB
Jan 26 18:48:36 Starting compiler/backend/reg_alloc
Jan 26 18:48:38 Finished compiler/backend/reg_alloc                               1s  21MB
Jan 26 18:48:38 Starting compiler/backend/gc
Jan 26 18:48:40 Finished compiler/backend/gc                                      2s  24MB
Jan 26 18:48:41 Starting compiler/backend
Jan 26 18:48:54 Finished compiler/backend                                        12s 776MB
Jan 26 18:48:54 Starting compiler/encoders/asm
Jan 26 18:48:55 Finished compiler/encoders/asm                                    1s  23MB
Jan 26 18:48:56 Starting compiler/encoders/x64
Jan 26 18:48:57 Finished compiler/encoders/x64                                    1s  26MB
Jan 26 18:48:57 Starting compiler/encoders/arm7
Jan 26 18:48:59 Finished compiler/encoders/arm7                                   1s  20MB
Jan 26 18:48:59 Starting compiler/encoders/arm8
Jan 26 18:49:01 Finished compiler/encoders/arm8                                   1s  20MB
Jan 26 18:49:01 Starting compiler/encoders/arm8_asl
Jan 26 21:15:50 Finished compiler/encoders/arm8_asl                         2h26m48s  48GB
Jan 26 21:15:50 Starting compiler/encoders/mips
Jan 26 21:15:52 Finished compiler/encoders/mips                                   1s  20MB
Jan 26 21:15:52 Starting compiler/encoders/riscv
Jan 26 21:15:54 Finished compiler/encoders/riscv                                  1s  26MB
Jan 26 21:15:54 Starting compiler/encoders/ag32
Jan 26 21:15:56 Finished compiler/encoders/ag32                                   1s  22MB
Jan 26 21:15:56 Starting compiler/backend/x64
Jan 26 21:15:58 Finished compiler/backend/x64                                     2s  28MB
Jan 26 21:15:58 Starting compiler/backend/arm7
Jan 26 21:16:01 Finished compiler/backend/arm7                                    2s  22MB
Jan 26 21:16:01 Starting compiler/backend/arm8
Jan 26 21:16:03 Finished compiler/backend/arm8                                    2s  23MB
Jan 26 21:16:03 Starting compiler/backend/mips
Jan 26 21:16:05 Finished compiler/backend/mips                                    2s  24MB
Jan 26 21:16:06 Starting compiler/backend/riscv
Jan 26 21:16:08 Finished compiler/backend/riscv                                   2s  24MB
Jan 26 21:16:08 Starting compiler/backend/ag32
Jan 26 21:17:33 Finished compiler/backend/ag32                                 1m24s   1GB
Jan 26 21:17:33 Starting compiler/parsing/proofs
Jan 26 21:17:35 Finished compiler/parsing/proofs                                  1s  19MB
Jan 26 21:17:35 Starting compiler/inference/proofs
Jan 26 21:17:37 Finished compiler/inference/proofs                                1s  19MB
Jan 26 21:17:37 Starting compiler/backend/semantics
Jan 26 21:18:51 Finished compiler/backend/semantics                            1m14s   1GB
Jan 26 21:18:51 Starting compiler/backend/reg_alloc/proofs
Jan 26 21:18:53 Finished compiler/backend/reg_alloc/proofs                        1s  22MB
Jan 26 21:18:54 Starting compiler/backend/proofs
Jan 26 21:19:53 Finished compiler/backend/proofs                                 59s   2GB
Jan 26 21:19:53 Starting compiler/backend/serialiser
Jan 26 21:19:56 Finished compiler/backend/serialiser                              2s  33MB
Jan 26 21:19:56 Starting compiler/encoders/x64/proofs
Jan 26 21:29:47 Finished compiler/encoders/x64/proofs                          9m51s   5GB
Jan 26 21:29:47 Starting compiler/encoders/arm7/proofs
Jan 26 21:43:35 Finished compiler/encoders/arm7/proofs                        13m47s   4GB
Jan 26 21:43:35 Starting compiler/encoders/arm8/proofs
Jan 26 21:50:35 Finished compiler/encoders/arm8/proofs                         7m00s   1GB
Jan 26 21:50:35 Starting compiler/encoders/arm8_asl/proofs
Jan 26 22:43:29 Finished compiler/encoders/arm8_asl/proofs                    52m53s   8GB
Jan 26 22:43:29 Starting compiler/encoders/mips/proofs
Jan 26 22:54:16 Finished compiler/encoders/mips/proofs                        10m46s   2GB
Jan 26 22:54:16 Starting compiler/encoders/riscv/proofs
Jan 26 23:03:00 Finished compiler/encoders/riscv/proofs                        8m43s   2GB
Jan 26 23:03:00 Starting compiler/encoders/ag32/proofs
Jan 26 23:05:33 Finished compiler/encoders/ag32/proofs                         2m32s 982MB
Jan 26 23:05:33 Starting compiler/backend/x64/proofs
Jan 26 23:06:04 Finished compiler/backend/x64/proofs                             30s   1GB
Jan 26 23:06:04 Starting compiler/backend/arm7/proofs
Jan 26 23:06:40 Finished compiler/backend/arm7/proofs                            35s   2GB
Jan 26 23:06:40 Starting compiler/backend/arm8/proofs
Jan 26 23:07:10 Finished compiler/backend/arm8/proofs                            29s   1GB
Jan 26 23:07:10 Starting compiler/backend/arm8_asl
Jan 26 23:07:35 Finished compiler/backend/arm8_asl                               24s   2GB
Jan 26 23:07:35 Starting compiler/backend/mips/proofs
Jan 26 23:08:09 Finished compiler/backend/mips/proofs                            33s   2GB
Jan 26 23:08:09 Starting compiler/backend/riscv/proofs
Jan 26 23:08:43 Finished compiler/backend/riscv/proofs                           33s   3GB
Jan 26 23:08:43 Starting compiler/backend/ag32/proofs
Jan 26 23:22:30 Finished compiler/backend/ag32/proofs                         13m47s   3GB
Jan 26 23:22:30 Starting candle/set-theory
Jan 26 23:23:10 Finished candle/set-theory                                       39s   1GB
Jan 26 23:23:10 Starting candle/syntax-lib
Jan 26 23:23:12 Finished candle/syntax-lib                                        1s  20MB
Jan 26 23:23:12 Starting candle/standard/syntax
Jan 26 23:23:23 Finished candle/standard/syntax                                  11s 695MB
Jan 26 23:23:23 Starting candle/standard/semantics
Jan 26 23:25:22 Finished candle/standard/semantics                             1m58s   1GB
Jan 26 23:25:22 Starting candle/standard/monadic
Jan 26 23:25:24 Finished candle/standard/monadic                                  1s  29MB
Jan 26 23:25:24 Starting candle/standard/ml_kernel
Jan 26 23:27:02 Finished candle/standard/ml_kernel                             1m37s   3GB
Jan 26 23:27:02 Starting candle/overloading/syntax
Jan 26 23:30:24 Finished candle/overloading/syntax                             3m22s   1GB
Jan 26 23:30:24 Starting candle/overloading/semantics
Jan 26 23:42:39 Finished candle/overloading/semantics                         12m15s   3GB
Jan 26 23:42:39 Starting candle/overloading/monadic
Jan 26 23:45:25 Finished candle/overloading/monadic                            2m46s   1GB
Jan 26 23:45:26 Starting candle/overloading/ml_kernel
Jan 26 23:53:22 Finished candle/overloading/ml_kernel                          7m55s   3GB
Jan 26 23:53:22 Starting candle/overloading/ml_checker
Jan 26 23:56:01 Finished candle/overloading/ml_checker                         2m39s   2GB
Jan 26 23:56:01 Starting candle/prover
Jan 27 00:06:01 Finished candle/prover                                        10m00s   4GB
Jan 27 00:06:02 Starting pancake
Jan 27 00:06:48 Finished pancake                                                 46s 952MB
Jan 27 00:06:48 Starting pancake/ffi
Jan 27 00:06:49 Finished pancake/ffi                                              0s  13MB
Jan 27 00:06:49 Starting pancake/semantics
Jan 27 00:09:15 Finished pancake/semantics                                     2m26s   1GB
Jan 27 00:09:15 Starting pancake/parser
Jan 27 00:09:39 Finished pancake/parser                                          24s   1GB
Jan 27 00:09:40 Starting pancake/proofs
Jan 27 00:42:59 Finished pancake/proofs                                       33m18s   7GB
Jan 27 00:42:59 Starting characteristic/examples
Jan 27 00:44:32 Finished characteristic/examples                               1m33s   2GB
Jan 27 00:44:32 Starting tutorial/solutions
Jan 27 00:59:40 Finished tutorial/solutions                                   15m07s  10GB
Jan 27 00:59:40 Starting translator/monadic/examples
Jan 27 01:03:46 Finished translator/monadic/examples                           4m05s   2GB
Jan 27 01:03:46 Starting examples
Jan 27 01:19:44 Finished examples                                             15m58s   5GB
Jan 27 01:19:44 Starting examples/compilation/x64
Jan 27 03:18:57 Finished examples/compilation/x64                           1h59m12s  19GB
Jan 27 03:18:57 Starting examples/compilation/x64/proofs
Jan 27 03:21:38 Finished examples/compilation/x64/proofs                       2m40s   3GB
Jan 27 03:21:38 Starting examples/compilation/ag32
Jan 27 03:51:47 Finished examples/compilation/ag32                            30m09s  10GB
Jan 27 03:51:47 Starting examples/compilation/ag32/proofs
Jan 27 03:52:51 Finished examples/compilation/ag32/proofs                      1m03s   5GB
Jan 27 03:52:51 Starting examples/compilation/to_word
Jan 27 03:56:16 Finished examples/compilation/to_word                          3m25s   7GB
Jan 27 03:56:16 Starting examples/lpr_checker
Jan 27 03:57:23 Finished examples/lpr_checker                                  1m06s   1GB
Jan 27 03:57:23 Starting examples/lpr_checker/array
Jan 27 04:28:24 Finished examples/lpr_checker/array                           31m01s   6GB
Jan 27 04:28:24 Starting examples/lpr_checker/array/compilation
Jan 27 05:16:52 Finished examples/lpr_checker/array/compilation               48m27s  33GB
Jan 27 05:16:52 Starting examples/lpr_checker/array/compilation/proofs
Jan 27 05:18:57 Finished examples/lpr_checker/array/compilation/proofs         2m05s   3GB
Jan 27 05:18:57 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 27 05:24:41 Finished examples/lpr_checker/array/compilation/proofsARM8     5m43s  23GB
Jan 27 05:24:41 Starting examples/pseudo_bool
Jan 27 05:26:29 Finished examples/pseudo_bool                                  1m47s   1GB
Jan 27 05:26:29 Starting examples/pseudo_bool/cnf_encoding
Jan 27 05:26:54 Finished examples/pseudo_bool/cnf_encoding                       24s 693MB
Jan 27 05:26:54 Starting examples/pseudo_bool/graph_encoding
Jan 27 05:27:38 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Jan 27 05:27:38 Starting examples/pseudo_bool/array
Jan 27 06:21:37 Finished examples/pseudo_bool/array                           53m58s   7GB
Jan 27 06:21:37 Starting examples/pseudo_bool/array/compilation
Jan 27 09:13:34 Finished examples/pseudo_bool/array/compilation             2h51m56s  32GB
Jan 27 09:13:34 Starting examples/pseudo_bool/array/compilation/proofs
Jan 27 09:16:22 Finished examples/pseudo_bool/array/compilation/proofs         2m47s   5GB
Jan 27 09:16:22 Starting examples/opentheory
Jan 27 09:27:25 Finished examples/opentheory                                  11m02s   6GB
Jan 27 09:27:25 Starting examples/opentheory
Jan 27 09:27:27 Finished examples/opentheory                                      1s  28MB
Jan 27 09:27:27 Starting examples/opentheory/compilation
Jan 27 10:04:44 Finished examples/opentheory/compilation                      37m16s  31GB
Jan 27 10:04:44 Starting examples/opentheory/compilation/proofs
Jan 27 10:05:44 Finished examples/opentheory/compilation/proofs                  59s   4GB
Jan 27 10:05:44 Starting examples/opentheory/compilation/ag32
Jan 27 10:38:44 Finished examples/opentheory/compilation/ag32                 32m59s  30GB
Jan 27 10:38:44 Starting examples/opentheory/compilation/ag32/proofs
Jan 27 10:40:40 Finished examples/opentheory/compilation/ag32/proofs           1m56s   7GB
Jan 27 10:40:40 Starting examples/sat_encodings
Jan 27 10:42:47 Finished examples/sat_encodings                                2m06s   1GB
Jan 27 10:42:47 Starting examples/sat_encodings/case_studies
Jan 27 10:44:36 Finished examples/sat_encodings/case_studies                   1m49s   1GB
Jan 27 10:44:36 Starting examples/sat_encodings/translation
Jan 27 10:50:46 Finished examples/sat_encodings/translation                    6m10s   5GB
Jan 27 10:50:47 Starting examples/sat_encodings/translation/compilation
Jan 27 11:36:32 Finished examples/sat_encodings/translation/compilation       45m45s  23GB
Jan 27 11:36:32 Starting examples/deflate
Jan 27 11:37:32 Finished examples/deflate                                      1m00s 875MB
Jan 27 11:37:32 Starting examples/deflate/translation
Jan 27 11:39:16 Finished examples/deflate/translation                          1m43s   3GB
Jan 27 11:39:16 Starting examples/deflate/translation/compilation
Jan 27 11:59:28 Finished examples/deflate/translation/compilation             20m12s  15GB
Jan 27 11:59:28 Starting examples/vipr
Jan 27 12:03:33 Finished examples/vipr                                         4m04s   2GB
Jan 27 12:03:33 Starting examples/vipr/compilation
Jan 27 12:23:48 Finished examples/vipr/compilation                            20m14s  16GB
Jan 27 12:23:48 Starting translator/okasaki-examples
Jan 27 12:29:02 Finished translator/okasaki-examples                           5m13s   2GB
Jan 27 12:29:02 Starting translator/other-examples
Jan 27 12:32:34 Finished translator/other-examples                             3m31s   1GB
Jan 27 12:32:34 Starting compiler/parsing/tests
Jan 27 12:33:06 Finished compiler/parsing/tests                                  32s 808MB
Jan 27 12:33:06 Starting compiler/inference/tests
Jan 27 12:41:33 Finished compiler/inference/tests                              8m26s   5GB
Jan 27 12:41:33 Starting compiler/printing/test
Jan 27 12:45:24 Finished compiler/printing/test                                3m50s   3GB
Jan 27 12:45:24 Starting icing/flover
Jan 27 13:29:18 Finished icing/flover                                         43m53s   2GB
Jan 27 13:29:18 Starting icing/
Jan 27 14:23:56 Finished icing/                                               54m37s   7GB
Jan 27 14:23:56 Starting icing/examples
Jan 27 14:25:35 Finished icing/examples                                        1m39s   5GB
Jan 27 14:25:35 Starting compiler/repl
Jan 27 14:34:26 Finished compiler/repl                                         8m50s   6GB
Jan 27 14:34:26 Starting unverified/sexpr-bootstrap/x64/64
Jan 27 14:48:16 Finished unverified/sexpr-bootstrap/x64/64                    13m49s  15GB
Jan 27 14:48:16 Starting unverified/sexpr-bootstrap/x64/32
Jan 27 14:59:23 Finished unverified/sexpr-bootstrap/x64/32                    11m06s  12GB
Jan 27 14:59:24 Starting compiler/benchmarks
Jan 27 15:15:03 Finished compiler/benchmarks                                  15m39s   2GB
Jan 27 15:15:03 Starting compiler/bootstrap/compilation/x64/64
Jan 28 03:36:01 Finished compiler/bootstrap/compilation/x64/64             12h20m57s  64GB
Jan 28 03:36:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 28 03:58:45 Finished compiler/bootstrap/compilation/x64/64/proofs         22m44s  34GB
Jan 28 03:58:45 Starting compiler/bootstrap/compilation/x64/32
Jan 28 11:33:53 Finished compiler/bootstrap/compilation/x64/32              7h35m06s  64GB
Jan 28 11:33:53 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 28 11:37:24 Finished compiler/bootstrap/compilation/x64/32/proofs          3m31s  19GB
Jan 28 11:37:24 Starting compiler/bootstrap/compilation/ag32/32
Jan 28 19:13:26 Finished compiler/bootstrap/compilation/ag32/32             7h36m01s  64GB
Jan 28 19:13:26 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 28 19:27:03 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m37s  23GB
Jan 28 19:27:04 SUCCESS