Job 2274

CakeML:e026a91d58aabda091e58bb8b4b8ca67b192f07c
  Fix mlvector given changes in HOL [Jan 17 02:43:46]
HOL:4103c90e68aea21ac033b5e9205a8521e7a51b71
  FTBFS HolBdd and temporal_deep examples [Jan 17 23:33:26]
Machine:stove 5.15.0-86-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 19 09:35:15 Claimed job
Jan 19 09:35:21 Building HOL
Jan 19 09:49:05 Starting developers
Jan 19 09:49:10 Finished developers                                               5s 110MB
Jan 19 09:49:10 Starting developers/bin
Jan 19 09:49:19 Finished developers/bin                                           8s   1GB
Jan 19 09:49:19 Starting compiler/proofs
Jan 19 11:43:00 Finished compiler/proofs                                    1h53m41s  15GB
Jan 19 11:43:00 Starting compiler/bootstrap/translation
Jan 19 19:54:08 Finished compiler/bootstrap/translation                     8h11m08s  44GB
Jan 19 19:54:09 Starting semantics/ffi
Jan 19 19:54:15 Finished semantics/ffi                                            5s 212MB
Jan 19 19:54:15 Starting semantics
Jan 19 19:54:16 Finished semantics                                                1s  21MB
Jan 19 19:54:16 Starting semantics/proofs
Jan 19 19:54:48 Finished semantics/proofs                                        31s 754MB
Jan 19 19:54:48 Starting semantics/alt_semantics
Jan 19 19:55:20 Finished semantics/alt_semantics                                 31s 874MB
Jan 19 19:55:20 Starting semantics/alt_semantics/proofs
Jan 19 20:07:25 Finished semantics/alt_semantics/proofs                       12m04s   1GB
Jan 19 20:07:25 Starting basis/pure
Jan 19 20:07:27 Finished basis/pure                                               1s  19MB
Jan 19 20:07:27 Starting translator
Jan 19 20:09:18 Finished translator                                            1m51s   1GB
Jan 19 20:09:18 Starting compiler/parsing
Jan 19 20:09:20 Finished compiler/parsing                                         1s  19MB
Jan 19 20:09:20 Starting characteristic
Jan 19 20:09:22 Finished characteristic                                           1s  23MB
Jan 19 20:09:22 Starting translator/monadic
Jan 19 20:09:24 Finished translator/monadic                                       1s  20MB
Jan 19 20:09:24 Starting basis
Jan 19 20:13:05 Finished basis                                                 3m41s   2GB
Jan 19 20:13:06 Starting compiler/inference
Jan 19 20:13:07 Finished compiler/inference                                       1s  22MB
Jan 19 20:13:07 Starting compiler/backend/reg_alloc
Jan 19 20:13:09 Finished compiler/backend/reg_alloc                               1s  22MB
Jan 19 20:13:09 Starting compiler/backend/gc
Jan 19 20:13:11 Finished compiler/backend/gc                                      2s  24MB
Jan 19 20:13:11 Starting compiler/backend
Jan 19 20:13:24 Finished compiler/backend                                        12s 793MB
Jan 19 20:13:25 Starting compiler/encoders/asm
Jan 19 20:13:26 Finished compiler/encoders/asm                                    1s  24MB
Jan 19 20:13:26 Starting compiler/encoders/x64
Jan 19 20:13:28 Finished compiler/encoders/x64                                    1s  23MB
Jan 19 20:13:28 Starting compiler/encoders/arm7
Jan 19 20:13:30 Finished compiler/encoders/arm7                                   1s  26MB
Jan 19 20:13:30 Starting compiler/encoders/arm8
Jan 19 20:13:32 Finished compiler/encoders/arm8                                   1s  20MB
Jan 19 20:13:32 Starting compiler/encoders/arm8_asl
Jan 19 22:38:48 Finished compiler/encoders/arm8_asl                         2h25m15s  37GB
Jan 19 22:38:48 Starting compiler/encoders/mips
Jan 19 22:38:50 Finished compiler/encoders/mips                                   1s  23MB
Jan 19 22:38:50 Starting compiler/encoders/riscv
Jan 19 22:38:51 Finished compiler/encoders/riscv                                  1s  23MB
Jan 19 22:38:51 Starting compiler/encoders/ag32
Jan 19 22:38:53 Finished compiler/encoders/ag32                                   1s  24MB
Jan 19 22:38:53 Starting compiler/backend/x64
Jan 19 22:38:56 Finished compiler/backend/x64                                     2s  22MB
Jan 19 22:38:56 Starting compiler/backend/arm7
Jan 19 22:38:58 Finished compiler/backend/arm7                                    2s  21MB
Jan 19 22:38:58 Starting compiler/backend/arm8
Jan 19 22:39:00 Finished compiler/backend/arm8                                    2s  21MB
Jan 19 22:39:00 Starting compiler/backend/mips
Jan 19 22:39:03 Finished compiler/backend/mips                                    2s  22MB
Jan 19 22:39:03 Starting compiler/backend/riscv
Jan 19 22:39:05 Finished compiler/backend/riscv                                   2s  21MB
Jan 19 22:39:05 Starting compiler/backend/ag32
Jan 19 22:40:31 Finished compiler/backend/ag32                                 1m25s   1GB
Jan 19 22:40:31 Starting compiler/parsing/proofs
Jan 19 22:40:32 Finished compiler/parsing/proofs                                  1s  22MB
Jan 19 22:40:32 Starting compiler/inference/proofs
Jan 19 22:40:34 Finished compiler/inference/proofs                                1s  21MB
Jan 19 22:40:34 Starting compiler/backend/semantics
Jan 19 22:41:48 Finished compiler/backend/semantics                            1m13s   1GB
Jan 19 22:41:48 Starting compiler/backend/reg_alloc/proofs
Jan 19 22:41:50 Finished compiler/backend/reg_alloc/proofs                        1s  25MB
Jan 19 22:41:50 Starting compiler/backend/proofs
Jan 19 22:42:50 Finished compiler/backend/proofs                               1m00s   3GB
Jan 19 22:42:50 Starting compiler/backend/serialiser
Jan 19 22:42:53 Finished compiler/backend/serialiser                              2s  32MB
Jan 19 22:42:53 Starting compiler/encoders/x64/proofs
Jan 19 22:52:41 Finished compiler/encoders/x64/proofs                          9m47s   5GB
Jan 19 22:52:42 Starting compiler/encoders/arm7/proofs
Jan 19 23:06:36 Finished compiler/encoders/arm7/proofs                        13m53s   4GB
Jan 19 23:06:36 Starting compiler/encoders/arm8/proofs
Jan 19 23:13:25 Finished compiler/encoders/arm8/proofs                         6m48s   1GB
Jan 19 23:13:25 Starting compiler/encoders/arm8_asl/proofs
Jan 20 00:06:11 Finished compiler/encoders/arm8_asl/proofs                    52m45s   8GB
Jan 20 00:06:11 Starting compiler/encoders/mips/proofs
Jan 20 00:16:54 Finished compiler/encoders/mips/proofs                        10m43s   2GB
Jan 20 00:16:55 Starting compiler/encoders/riscv/proofs
Jan 20 00:25:39 Finished compiler/encoders/riscv/proofs                        8m44s   2GB
Jan 20 00:25:39 Starting compiler/encoders/ag32/proofs
Jan 20 00:28:10 Finished compiler/encoders/ag32/proofs                         2m30s   1GB
Jan 20 00:28:10 Starting compiler/backend/x64/proofs
Jan 20 00:28:40 Finished compiler/backend/x64/proofs                             29s   1GB
Jan 20 00:28:40 Starting compiler/backend/arm7/proofs
Jan 20 00:29:14 Finished compiler/backend/arm7/proofs                            33s   2GB
Jan 20 00:29:14 Starting compiler/backend/arm8/proofs
Jan 20 00:29:45 Finished compiler/backend/arm8/proofs                            30s   1GB
Jan 20 00:29:45 Starting compiler/backend/arm8_asl
Jan 20 00:30:10 Finished compiler/backend/arm8_asl                               24s   2GB
Jan 20 00:30:10 Starting compiler/backend/mips/proofs
Jan 20 00:30:41 Finished compiler/backend/mips/proofs                            31s   2GB
Jan 20 00:30:41 Starting compiler/backend/riscv/proofs
Jan 20 00:31:15 Finished compiler/backend/riscv/proofs                           33s   2GB
Jan 20 00:31:16 Starting compiler/backend/ag32/proofs
Jan 20 00:44:53 Finished compiler/backend/ag32/proofs                         13m37s   4GB
Jan 20 00:44:53 Starting candle/set-theory
Jan 20 00:45:33 Finished candle/set-theory                                       39s   1GB
Jan 20 00:45:33 Starting candle/syntax-lib
Jan 20 00:45:34 Finished candle/syntax-lib                                        1s  23MB
Jan 20 00:45:34 Starting candle/standard/syntax
Jan 20 00:45:47 Finished candle/standard/syntax                                  12s 698MB
Jan 20 00:45:47 Starting candle/standard/semantics
Jan 20 00:47:47 Finished candle/standard/semantics                             2m00s   1GB
Jan 20 00:47:47 Starting candle/standard/monadic
Jan 20 00:47:49 Finished candle/standard/monadic                                  1s  20MB
Jan 20 00:47:49 Starting candle/standard/ml_kernel
Jan 20 00:49:29 Finished candle/standard/ml_kernel                             1m39s   3GB
Jan 20 00:49:29 Starting candle/overloading/syntax
Jan 20 00:52:53 Finished candle/overloading/syntax                             3m24s   1GB
Jan 20 00:52:54 Starting candle/overloading/semantics
Jan 20 01:05:03 Finished candle/overloading/semantics                         12m09s   3GB
Jan 20 01:05:03 Starting candle/overloading/monadic
Jan 20 01:07:48 Finished candle/overloading/monadic                            2m45s   2GB
Jan 20 01:07:48 Starting candle/overloading/ml_kernel
Jan 20 01:15:48 Finished candle/overloading/ml_kernel                          7m59s   3GB
Jan 20 01:15:48 Starting candle/overloading/ml_checker
Jan 20 01:18:27 Finished candle/overloading/ml_checker                         2m39s   2GB
Jan 20 01:18:27 Starting candle/prover
Jan 20 01:28:28 Finished candle/prover                                        10m00s   3GB
Jan 20 01:28:28 Starting pancake
Jan 20 01:29:12 Finished pancake                                                 43s 837MB
Jan 20 01:29:12 Starting pancake/ffi
Jan 20 01:29:12 Finished pancake/ffi                                              0s  12MB
Jan 20 01:29:13 Starting pancake/semantics
Jan 20 01:31:40 Finished pancake/semantics                                     2m27s   1GB
Jan 20 01:31:40 Starting pancake/parser
Jan 20 01:32:04 Finished pancake/parser                                          23s   1GB
Jan 20 01:32:04 Starting pancake/proofs
Jan 20 02:05:45 Finished pancake/proofs                                       33m40s   6GB
Jan 20 02:05:45 Starting characteristic/examples
Jan 20 02:07:33 Finished characteristic/examples                               1m48s   3GB
Jan 20 02:07:34 Starting tutorial/solutions
Jan 20 02:23:07 Finished tutorial/solutions                                   15m33s  10GB
Jan 20 02:23:07 Starting translator/monadic/examples
Jan 20 02:27:13 Finished translator/monadic/examples                           4m04s   3GB
Jan 20 02:27:13 Starting examples
Jan 20 17:04:54 Resuming examples
Jan 20 17:06:28 Finished examples                                              1m33s   3GB
Jan 20 17:06:28 Starting examples/compilation/x64
Jan 20 19:07:21 Finished examples/compilation/x64                           2h00m52s  18GB
Jan 20 19:07:21 Starting examples/compilation/x64/proofs
Jan 20 19:09:56 Finished examples/compilation/x64/proofs                       2m34s   4GB
Jan 20 19:09:56 Starting examples/compilation/ag32
Jan 20 19:40:31 Finished examples/compilation/ag32                            30m35s   6GB
Jan 20 19:40:32 Starting examples/compilation/ag32/proofs
Jan 20 19:41:55 Finished examples/compilation/ag32/proofs                      1m23s   4GB
Jan 20 19:41:55 Starting examples/compilation/to_word
Jan 20 19:45:18 Finished examples/compilation/to_word                          3m22s   4GB
Jan 20 19:45:18 Starting examples/lpr_checker
Jan 20 19:46:24 Finished examples/lpr_checker                                  1m05s   1GB
Jan 20 19:46:24 Starting examples/lpr_checker/array
Jan 20 20:17:07 Finished examples/lpr_checker/array                           30m43s   7GB
Jan 20 20:17:07 Starting examples/lpr_checker/array/compilation
Jan 20 21:06:10 Finished examples/lpr_checker/array/compilation               49m02s  33GB
Jan 20 21:06:10 Starting examples/lpr_checker/array/compilation/proofs
Jan 20 21:08:13 Finished examples/lpr_checker/array/compilation/proofs         2m02s   3GB
Jan 20 21:08:13 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 20 21:13:51 Finished examples/lpr_checker/array/compilation/proofsARM8     5m37s  17GB
Jan 20 21:13:51 Starting examples/pseudo_bool
Jan 20 21:15:40 Finished examples/pseudo_bool                                  1m48s   1GB
Jan 20 21:15:40 Starting examples/pseudo_bool/cnf_encoding
Jan 20 21:16:05 Finished examples/pseudo_bool/cnf_encoding                       25s 768MB
Jan 20 21:16:05 Starting examples/pseudo_bool/graph_encoding
Jan 20 21:16:47 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Jan 20 21:16:47 Starting examples/pseudo_bool/array
Jan 20 22:10:27 Finished examples/pseudo_bool/array                           53m39s   6GB
Jan 20 22:10:27 Starting examples/pseudo_bool/array/compilation
Jan 21 01:02:14 Finished examples/pseudo_bool/array/compilation             2h51m46s  33GB
Jan 21 01:02:14 Starting examples/pseudo_bool/array/compilation/proofs
Jan 21 01:05:02 Finished examples/pseudo_bool/array/compilation/proofs         2m47s   6GB
Jan 21 01:05:02 Starting examples/opentheory
Jan 21 01:15:59 Finished examples/opentheory                                  10m56s   4GB
Jan 21 01:15:59 Starting examples/opentheory
Jan 21 01:16:00 Finished examples/opentheory                                      1s  36MB
Jan 21 01:16:01 Starting examples/opentheory/compilation
Jan 21 01:54:23 Finished examples/opentheory/compilation                      38m21s  29GB
Jan 21 01:54:23 Starting examples/opentheory/compilation/proofs
Jan 21 01:55:26 Finished examples/opentheory/compilation/proofs                1m03s   4GB
Jan 21 01:55:26 Starting examples/opentheory/compilation/ag32
Jan 21 02:28:57 Finished examples/opentheory/compilation/ag32                 33m30s  30GB
Jan 21 02:28:58 Starting examples/opentheory/compilation/ag32/proofs
Jan 21 02:30:53 Finished examples/opentheory/compilation/ag32/proofs           1m55s   7GB
Jan 21 02:30:53 Starting examples/sat_encodings
Jan 21 02:32:58 Finished examples/sat_encodings                                2m04s   1GB
Jan 21 02:32:58 Starting examples/sat_encodings/case_studies
Jan 21 02:34:42 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Jan 21 02:34:42 Starting examples/sat_encodings/translation
Jan 21 02:40:53 Finished examples/sat_encodings/translation                    6m10s   5GB
Jan 21 02:40:53 Starting examples/sat_encodings/translation/compilation
Jan 21 03:27:19 Finished examples/sat_encodings/translation/compilation       46m26s  20GB
Jan 21 03:27:19 Starting examples/deflate
Jan 21 03:28:19 Finished examples/deflate                                        59s 990MB
Jan 21 03:28:19 Starting examples/deflate/translation
Jan 21 03:30:03 Finished examples/deflate/translation                          1m43s   3GB
Jan 21 03:30:03 Starting examples/deflate/translation/compilation
Jan 21 03:50:20 Finished examples/deflate/translation/compilation             20m16s  14GB
Jan 21 03:50:20 Starting examples/vipr
Jan 21 03:54:28 Finished examples/vipr                                         4m07s   3GB
Jan 21 03:54:28 Starting examples/vipr/compilation
Jan 21 04:15:00 Finished examples/vipr/compilation                            20m31s  17GB
Jan 21 04:15:00 Starting translator/okasaki-examples
Jan 21 04:20:14 Finished translator/okasaki-examples                           5m14s   2GB
Jan 21 04:20:14 Starting translator/other-examples
Jan 21 04:23:04 Finished translator/other-examples                             2m49s   1GB
Jan 21 04:23:04 Starting compiler/parsing/tests
Jan 21 04:23:37 Finished compiler/parsing/tests                                  32s 812MB
Jan 21 04:23:37 Starting compiler/inference/tests
Jan 21 04:32:18 Finished compiler/inference/tests                              8m41s   6GB
Jan 21 04:32:18 Starting compiler/printing/test
Jan 21 04:36:12 Finished compiler/printing/test                                3m54s   3GB
Jan 21 04:36:13 Starting icing/flover
Jan 21 05:19:38 Finished icing/flover                                         43m24s   2GB
Jan 21 05:19:38 Starting icing/
Jan 21 06:14:20 Finished icing/                                               54m42s   9GB
Jan 21 06:14:20 Starting icing/examples
Jan 21 06:15:55 Finished icing/examples                                        1m34s   6GB
Jan 21 06:15:55 Starting compiler/repl
Jan 21 06:24:42 Finished compiler/repl                                         8m46s   5GB
Jan 21 06:24:42 Starting unverified/sexpr-bootstrap/x64/64
Jan 21 06:38:26 Finished unverified/sexpr-bootstrap/x64/64                    13m43s  15GB
Jan 21 06:38:27 Starting unverified/sexpr-bootstrap/x64/32
Jan 21 06:49:33 Finished unverified/sexpr-bootstrap/x64/32                    11m05s  13GB
Jan 21 06:49:33 Starting compiler/benchmarks
Jan 21 07:05:12 Finished compiler/benchmarks                                  15m39s   2GB
Jan 21 07:05:12 Starting compiler/bootstrap/compilation/x64/64
Jan 21 19:16:02 Finished compiler/bootstrap/compilation/x64/64             12h10m48s  64GB
Jan 21 19:16:02 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 21 19:36:46 Finished compiler/bootstrap/compilation/x64/64/proofs         20m44s  31GB
Jan 21 19:36:46 Starting compiler/bootstrap/compilation/x64/32
Jan 22 02:48:12 Finished compiler/bootstrap/compilation/x64/32              7h11m25s  64GB
Jan 22 02:48:12 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 22 02:51:32 Finished compiler/bootstrap/compilation/x64/32/proofs          3m19s  22GB
Jan 22 02:51:32 Starting compiler/bootstrap/compilation/ag32/32
Jan 22 10:06:07 Finished compiler/bootstrap/compilation/ag32/32             7h14m34s  64GB
Jan 22 10:06:07 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 22 10:13:18 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m10s  44GB
Jan 22 10:13:18 SUCCESS