Job 2257

CakeML:6dbde1638d8954eb5b8977247e781c0e7f92246f
  Fix for change in HOL [Dec 19 10:21:15]
HOL:d587e1c70b4c059edc079ed4a529b5b7423223b8
  Add ltree_every and ltree_finite_branching (#1172) [Dec 11 22:22:54]
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

Dec 19 10:22:34 Claimed job
Dec 19 10:22:41 Reusing HOL
Dec 19 10:23:22 Starting developers
Dec 19 10:23:28 Finished developers                                               5s 105MB
Dec 19 10:23:28 Starting developers/bin
Dec 19 10:23:36 Finished developers/bin                                           8s   1GB
Dec 19 10:23:36 Starting compiler/proofs
Dec 19 12:15:02 Finished compiler/proofs                                    1h51m25s  20GB
Dec 19 12:15:02 Starting compiler/bootstrap/translation
Dec 19 20:28:11 Finished compiler/bootstrap/translation                     8h13m08s  33GB
Dec 19 20:28:11 Starting semantics/ffi
Dec 19 20:28:17 Finished semantics/ffi                                            5s 216MB
Dec 19 20:28:17 Starting semantics
Dec 19 20:28:19 Finished semantics                                                1s  19MB
Dec 19 20:28:19 Starting semantics/proofs
Dec 19 20:28:52 Finished semantics/proofs                                        33s 708MB
Dec 19 20:28:52 Starting semantics/alt_semantics
Dec 19 20:29:24 Finished semantics/alt_semantics                                 31s 924MB
Dec 19 20:29:24 Starting semantics/alt_semantics/proofs
Dec 19 20:41:06 Finished semantics/alt_semantics/proofs                       11m41s   1GB
Dec 19 20:41:06 Starting basis/pure
Dec 19 20:41:08 Finished basis/pure                                               1s  19MB
Dec 19 20:41:08 Starting translator
Dec 19 20:42:58 Finished translator                                            1m50s   1GB
Dec 19 20:42:58 Starting compiler/parsing
Dec 19 20:43:00 Finished compiler/parsing                                         1s  19MB
Dec 19 20:43:00 Starting characteristic
Dec 19 20:43:02 Finished characteristic                                           1s  22MB
Dec 19 20:43:02 Starting translator/monadic
Dec 19 20:43:04 Finished translator/monadic                                       1s  24MB
Dec 19 20:43:04 Starting basis
Dec 19 20:46:51 Finished basis                                                 3m46s   2GB
Dec 19 20:46:51 Starting compiler/inference
Dec 19 20:46:53 Finished compiler/inference                                       1s  22MB
Dec 19 20:46:53 Starting compiler/backend/reg_alloc
Dec 19 20:46:54 Finished compiler/backend/reg_alloc                               1s  17MB
Dec 19 20:46:54 Starting compiler/backend/gc
Dec 19 20:46:57 Finished compiler/backend/gc                                      2s  27MB
Dec 19 20:46:57 Starting compiler/backend
Dec 19 20:47:09 Finished compiler/backend                                        12s 775MB
Dec 19 20:47:09 Starting compiler/encoders/asm
Dec 19 20:47:11 Finished compiler/encoders/asm                                    1s  18MB
Dec 19 20:47:11 Starting compiler/encoders/x64
Dec 19 20:47:13 Finished compiler/encoders/x64                                    1s  22MB
Dec 19 20:47:13 Starting compiler/encoders/arm7
Dec 19 20:47:15 Finished compiler/encoders/arm7                                   1s  19MB
Dec 19 20:47:15 Starting compiler/encoders/arm8
Dec 19 20:47:17 Finished compiler/encoders/arm8                                   1s  20MB
Dec 19 20:47:17 Starting compiler/encoders/arm8_asl
Dec 19 23:13:58 Finished compiler/encoders/arm8_asl                         2h26m41s  39GB
Dec 19 23:13:58 Starting compiler/encoders/mips
Dec 19 23:14:00 Finished compiler/encoders/mips                                   1s  20MB
Dec 19 23:14:00 Starting compiler/encoders/riscv
Dec 19 23:14:02 Finished compiler/encoders/riscv                                  1s  24MB
Dec 19 23:14:02 Starting compiler/encoders/ag32
Dec 19 23:14:04 Finished compiler/encoders/ag32                                   1s  24MB
Dec 19 23:14:04 Starting compiler/backend/x64
Dec 19 23:14:06 Finished compiler/backend/x64                                     2s  27MB
Dec 19 23:14:07 Starting compiler/backend/arm7
Dec 19 23:14:09 Finished compiler/backend/arm7                                    2s  28MB
Dec 19 23:14:09 Starting compiler/backend/arm8
Dec 19 23:14:11 Finished compiler/backend/arm8                                    2s  29MB
Dec 19 23:14:11 Starting compiler/backend/mips
Dec 19 23:14:13 Finished compiler/backend/mips                                    2s  24MB
Dec 19 23:14:14 Starting compiler/backend/riscv
Dec 19 23:14:16 Finished compiler/backend/riscv                                   2s  28MB
Dec 19 23:14:16 Starting compiler/backend/ag32
Dec 19 23:15:40 Finished compiler/backend/ag32                                 1m23s   1GB
Dec 19 23:15:40 Starting compiler/parsing/proofs
Dec 19 23:15:41 Finished compiler/parsing/proofs                                  1s  23MB
Dec 19 23:15:41 Starting compiler/inference/proofs
Dec 19 23:15:43 Finished compiler/inference/proofs                                1s  21MB
Dec 19 23:15:43 Starting compiler/backend/semantics
Dec 19 23:16:58 Finished compiler/backend/semantics                            1m14s   1GB
Dec 19 23:16:58 Starting compiler/backend/reg_alloc/proofs
Dec 19 23:17:00 Finished compiler/backend/reg_alloc/proofs                        1s  24MB
Dec 19 23:17:00 Starting compiler/backend/proofs
Dec 19 23:17:57 Finished compiler/backend/proofs                                 56s   2GB
Dec 19 23:17:57 Starting compiler/backend/serialiser
Dec 19 23:18:00 Finished compiler/backend/serialiser                              2s  34MB
Dec 19 23:18:00 Starting compiler/encoders/x64/proofs
Dec 19 23:27:49 Finished compiler/encoders/x64/proofs                          9m49s   5GB
Dec 19 23:27:49 Starting compiler/encoders/arm7/proofs
Dec 19 23:41:23 Finished compiler/encoders/arm7/proofs                        13m33s   5GB
Dec 19 23:41:23 Starting compiler/encoders/arm8/proofs
Dec 19 23:48:15 Finished compiler/encoders/arm8/proofs                         6m52s   1GB
Dec 19 23:48:15 Starting compiler/encoders/arm8_asl/proofs
Dec 20 00:41:17 Finished compiler/encoders/arm8_asl/proofs                    53m01s  10GB
Dec 20 00:41:17 Starting compiler/encoders/mips/proofs
Dec 20 00:52:04 Finished compiler/encoders/mips/proofs                        10m47s   2GB
Dec 20 00:52:04 Starting compiler/encoders/riscv/proofs
Dec 20 01:01:01 Finished compiler/encoders/riscv/proofs                        8m56s   1GB
Dec 20 01:01:02 Starting compiler/encoders/ag32/proofs
Dec 20 01:03:34 Finished compiler/encoders/ag32/proofs                         2m32s   1GB
Dec 20 01:03:34 Starting compiler/backend/x64/proofs
Dec 20 01:04:05 Finished compiler/backend/x64/proofs                             30s   1GB
Dec 20 01:04:05 Starting compiler/backend/arm7/proofs
Dec 20 01:04:38 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 20 01:04:38 Starting compiler/backend/arm8/proofs
Dec 20 01:05:09 Finished compiler/backend/arm8/proofs                            29s   1GB
Dec 20 01:05:09 Starting compiler/backend/arm8_asl
Dec 20 01:05:34 Finished compiler/backend/arm8_asl                               25s   2GB
Dec 20 01:05:34 Starting compiler/backend/mips/proofs
Dec 20 01:06:05 Finished compiler/backend/mips/proofs                            30s   2GB
Dec 20 01:06:05 Starting compiler/backend/riscv/proofs
Dec 20 01:06:39 Finished compiler/backend/riscv/proofs                           33s   2GB
Dec 20 01:06:39 Starting compiler/backend/ag32/proofs
Dec 20 01:20:33 Finished compiler/backend/ag32/proofs                         13m53s   3GB
Dec 20 01:20:33 Starting candle/set-theory
Dec 20 01:21:12 Finished candle/set-theory                                       38s   1GB
Dec 20 01:21:12 Starting candle/syntax-lib
Dec 20 01:21:13 Finished candle/syntax-lib                                        1s  22MB
Dec 20 01:21:13 Starting candle/standard/syntax
Dec 20 01:21:24 Finished candle/standard/syntax                                  10s 732MB
Dec 20 01:21:24 Starting candle/standard/semantics
Dec 20 01:23:21 Finished candle/standard/semantics                             1m56s   1GB
Dec 20 01:23:21 Starting candle/standard/monadic
Dec 20 01:23:23 Finished candle/standard/monadic                                  1s  23MB
Dec 20 01:23:23 Starting candle/standard/ml_kernel
Dec 20 01:24:57 Finished candle/standard/ml_kernel                             1m34s   3GB
Dec 20 01:24:58 Starting candle/overloading/syntax
Dec 20 01:28:20 Finished candle/overloading/syntax                             3m22s   1GB
Dec 20 01:28:21 Starting candle/overloading/semantics
Dec 20 01:40:34 Finished candle/overloading/semantics                         12m13s   2GB
Dec 20 01:40:34 Starting candle/overloading/monadic
Dec 20 01:43:18 Finished candle/overloading/monadic                            2m44s   1GB
Dec 20 01:43:19 Starting candle/overloading/ml_kernel
Dec 20 01:51:18 Finished candle/overloading/ml_kernel                          7m59s   3GB
Dec 20 01:51:18 Starting candle/overloading/ml_checker
Dec 20 01:53:54 Finished candle/overloading/ml_checker                         2m35s   2GB
Dec 20 01:53:54 Starting candle/prover
Dec 20 02:03:56 Finished candle/prover                                        10m01s   2GB
Dec 20 02:03:56 Starting pancake
Dec 20 02:04:41 Finished pancake                                                 44s 919MB
Dec 20 02:04:41 Starting pancake/ffi
Dec 20 02:04:41 Finished pancake/ffi                                              0s  13MB
Dec 20 02:04:41 Starting pancake/semantics
Dec 20 02:07:09 Finished pancake/semantics                                     2m27s   1GB
Dec 20 02:07:09 Starting pancake/parser
Dec 20 02:07:32 Finished pancake/parser                                          23s   1GB
Dec 20 02:07:32 Starting pancake/proofs
Dec 20 02:40:52 Finished pancake/proofs                                       33m19s   7GB
Dec 20 02:40:53 Starting characteristic/examples
Dec 20 02:42:30 Finished characteristic/examples                               1m36s   3GB
Dec 20 02:42:30 Starting tutorial/solutions
Dec 20 02:57:52 Finished tutorial/solutions                                   15m22s   8GB
Dec 20 02:57:53 Starting translator/monadic/examples
Dec 20 03:01:55 Finished translator/monadic/examples                           4m02s   2GB
Dec 20 03:01:55 Starting examples
Dec 20 03:17:58 Finished examples                                             16m02s   7GB
Dec 20 03:17:58 Starting examples/compilation/x64
Dec 20 05:18:08 Finished examples/compilation/x64                           2h00m09s  18GB
Dec 20 05:18:08 Starting examples/compilation/x64/proofs
Dec 20 05:20:43 Finished examples/compilation/x64/proofs                       2m34s   4GB
Dec 20 05:20:43 Starting examples/compilation/ag32
Dec 20 05:51:11 Finished examples/compilation/ag32                            30m27s   9GB
Dec 20 05:51:11 Starting examples/compilation/ag32/proofs
Dec 20 05:52:20 Finished examples/compilation/ag32/proofs                      1m09s   4GB
Dec 20 05:52:20 Starting examples/compilation/to_word
Dec 20 05:55:42 Finished examples/compilation/to_word                          3m21s   7GB
Dec 20 05:55:42 Starting examples/lpr_checker
Dec 20 05:56:47 Finished examples/lpr_checker                                  1m05s   1GB
Dec 20 05:56:47 Starting examples/lpr_checker/array
Dec 20 06:28:06 Finished examples/lpr_checker/array                           31m18s   6GB
Dec 20 06:28:07 Starting examples/lpr_checker/array/compilation
Dec 20 07:20:37 Finished examples/lpr_checker/array/compilation               52m29s  29GB
Dec 20 07:20:37 Starting examples/lpr_checker/array/compilation/proofs
Dec 20 07:22:38 Finished examples/lpr_checker/array/compilation/proofs         2m01s   3GB
Dec 20 07:22:39 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 20 07:28:08 Finished examples/lpr_checker/array/compilation/proofsARM8     5m28s  17GB
Dec 20 07:28:08 Starting examples/pseudo_bool
Dec 20 07:29:56 Finished examples/pseudo_bool                                  1m48s   1GB
Dec 20 07:29:56 Starting examples/pseudo_bool/cnf_encoding
Dec 20 07:30:21 Finished examples/pseudo_bool/cnf_encoding                       24s 617MB
Dec 20 07:30:21 Starting examples/pseudo_bool/graph_encoding
Dec 20 07:31:04 Finished examples/pseudo_bool/graph_encoding                     42s   1GB
Dec 20 07:31:04 Starting examples/pseudo_bool/array
Dec 20 08:25:11 Finished examples/pseudo_bool/array                           54m06s   6GB
Dec 20 08:25:11 Starting examples/pseudo_bool/array/compilation
Dec 20 11:17:20 Finished examples/pseudo_bool/array/compilation             2h52m08s  35GB
Dec 20 11:17:20 Starting examples/pseudo_bool/array/compilation/proofs
Dec 20 11:20:11 Finished examples/pseudo_bool/array/compilation/proofs         2m51s   6GB
Dec 20 11:20:11 Starting examples/opentheory
Dec 20 11:31:06 Finished examples/opentheory                                  10m54s   4GB
Dec 20 11:31:06 Starting examples/opentheory
Dec 20 11:31:08 Finished examples/opentheory                                      1s  26MB
Dec 20 11:31:08 Starting examples/opentheory/compilation
Dec 20 12:08:30 Finished examples/opentheory/compilation                      37m22s  32GB
Dec 20 12:08:30 Starting examples/opentheory/compilation/proofs
Dec 20 12:09:32 Finished examples/opentheory/compilation/proofs                1m01s   5GB
Dec 20 12:09:32 Starting examples/opentheory/compilation/ag32
Dec 20 12:42:52 Finished examples/opentheory/compilation/ag32                 33m19s  30GB
Dec 20 12:42:52 Starting examples/opentheory/compilation/ag32/proofs
Dec 20 12:44:44 Finished examples/opentheory/compilation/ag32/proofs           1m51s   4GB
Dec 20 12:44:44 Starting examples/sat_encodings
Dec 20 12:46:48 Finished examples/sat_encodings                                2m04s 921MB
Dec 20 12:46:48 Starting examples/sat_encodings/case_studies
Dec 20 12:48:35 Finished examples/sat_encodings/case_studies                   1m47s   1GB
Dec 20 12:48:36 Starting examples/sat_encodings/translation
Dec 20 12:54:46 Finished examples/sat_encodings/translation                    6m10s   3GB
Dec 20 12:54:46 Starting examples/sat_encodings/translation/compilation
Dec 20 13:43:23 Finished examples/sat_encodings/translation/compilation       48m37s  21GB
Dec 20 13:43:24 Starting examples/deflate
Dec 20 13:44:24 Finished examples/deflate                                      1m00s 883MB
Dec 20 13:44:24 Starting examples/deflate/translation
Dec 20 13:46:06 Finished examples/deflate/translation                          1m42s   3GB
Dec 20 13:46:07 Starting examples/deflate/translation/compilation
Dec 20 14:06:28 Finished examples/deflate/translation/compilation             20m21s  13GB
Dec 20 14:06:28 Starting examples/vipr
Dec 20 14:10:37 Finished examples/vipr                                         4m08s   4GB
Dec 20 14:10:37 Starting examples/vipr/compilation
Dec 20 14:31:34 Finished examples/vipr/compilation                            20m57s  20GB
Dec 20 14:31:34 Starting translator/okasaki-examples
Dec 20 14:36:44 Finished translator/okasaki-examples                           5m09s   2GB
Dec 20 14:36:44 Starting translator/other-examples
Dec 20 14:39:29 Finished translator/other-examples                             2m44s   1GB
Dec 20 14:39:29 Starting compiler/parsing/tests
Dec 20 14:40:01 Finished compiler/parsing/tests                                  32s 813MB
Dec 20 14:40:01 Starting compiler/inference/tests
Dec 20 14:48:36 Finished compiler/inference/tests                              8m34s   4GB
Dec 20 14:48:36 Starting compiler/printing/test
Dec 20 14:52:33 Finished compiler/printing/test                                3m57s   3GB
Dec 20 14:52:33 Starting icing/flover
Dec 20 15:36:14 Finished icing/flover                                         43m40s   2GB
Dec 20 15:36:14 Starting icing/
Dec 20 16:30:40 Finished icing/                                               54m25s   7GB
Dec 20 16:30:41 Starting icing/examples
Dec 20 16:32:20 Finished icing/examples                                        1m39s   6GB
Dec 20 16:32:20 Starting compiler/repl
Dec 20 16:41:19 Finished compiler/repl                                         8m58s   6GB
Dec 20 16:41:19 Starting unverified/sexpr-bootstrap/x64/64
Dec 20 16:55:05 Finished unverified/sexpr-bootstrap/x64/64                    13m45s  16GB
Dec 20 16:55:05 Starting unverified/sexpr-bootstrap/x64/32
Dec 20 17:06:06 Finished unverified/sexpr-bootstrap/x64/32                    11m00s  13GB
Dec 20 17:06:06 Starting compiler/benchmarks
Dec 20 17:21:46 Finished compiler/benchmarks                                  15m39s   2GB
Dec 20 17:21:46 Starting compiler/bootstrap/compilation/x64/64
Dec 21 06:04:49 Finished compiler/bootstrap/compilation/x64/64             12h43m02s  64GB
Dec 21 06:04:49 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 21 06:26:07 Finished compiler/bootstrap/compilation/x64/64/proofs         21m17s  21GB
Dec 21 06:26:07 Starting compiler/bootstrap/compilation/x64/32
Dec 21 13:37:09 Finished compiler/bootstrap/compilation/x64/32              7h11m01s  64GB
Dec 21 13:37:09 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 21 13:40:28 Finished compiler/bootstrap/compilation/x64/32/proofs          3m18s  17GB
Dec 21 13:40:28 Starting compiler/bootstrap/compilation/ag32/32
Dec 21 21:01:15 Finished compiler/bootstrap/compilation/ag32/32             7h20m46s  64GB
Dec 21 21:01:15 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 21 21:08:26 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m11s  48GB
Dec 21 21:08:26 SUCCESS