Job 2264

CakeML:45534e558612704f938386fc12b79bc991c3afa3
  Update for new year [Jan 01 02:20:21]
HOL:d587e1c70b4c059edc079ed4a529b5b7423223b8
  Add ltree_every and ltree_finite_branching (#1172) [Dec 11 22:22:54]
Machine:pavlova
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 04 23:38:55 Claimed job
Jan 04 23:39:01 Reusing HOL
Jan 04 23:39:12 Starting developers
Jan 04 23:39:15 Finished developers                                               2s 215MB
Jan 04 23:39:16 Starting developers/bin
Jan 04 23:39:26 Finished developers/bin                                           9s   1GB
Jan 04 23:39:27 Starting compiler/proofs
Jan 05 01:20:50 Finished compiler/proofs                                    1h41m22s  31GB
Jan 05 01:20:51 Starting compiler/bootstrap/translation
Jan 05 09:33:41 Finished compiler/bootstrap/translation                     8h12m48s  74GB
Jan 05 09:33:42 Starting semantics/ffi
Jan 05 09:33:50 Finished semantics/ffi                                            7s 580MB
Jan 05 09:33:51 Starting semantics
Jan 05 09:33:52 Finished semantics                                                0s  67MB
Jan 05 09:33:53 Starting semantics/proofs
Jan 05 09:34:31 Finished semantics/proofs                                        37s   1GB
Jan 05 09:34:32 Starting semantics/alt_semantics
Jan 05 09:35:12 Finished semantics/alt_semantics                                 38s   1GB
Jan 05 09:35:13 Starting semantics/alt_semantics/proofs
Jan 05 09:46:03 Finished semantics/alt_semantics/proofs                       10m49s   3GB
Jan 05 09:46:04 Starting basis/pure
Jan 05 09:46:05 Finished basis/pure                                               0s  67MB
Jan 05 09:46:06 Starting translator
Jan 05 09:47:50 Finished translator                                            1m43s   3GB
Jan 05 09:47:51 Starting compiler/parsing
Jan 05 09:47:52 Finished compiler/parsing                                         0s  73MB
Jan 05 09:47:53 Starting characteristic
Jan 05 09:47:55 Finished characteristic                                           0s  89MB
Jan 05 09:47:56 Starting translator/monadic
Jan 05 09:47:57 Finished translator/monadic                                       0s  98MB
Jan 05 09:47:58 Starting basis
Jan 05 09:51:35 Finished basis                                                 3m36s   6GB
Jan 05 09:51:36 Starting compiler/inference
Jan 05 09:51:37 Finished compiler/inference                                       0s  79MB
Jan 05 09:51:38 Starting compiler/backend/reg_alloc
Jan 05 09:51:40 Finished compiler/backend/reg_alloc                               0s  65MB
Jan 05 09:51:40 Starting compiler/backend/gc
Jan 05 09:51:42 Finished compiler/backend/gc                                      0s 137MB
Jan 05 09:51:43 Starting compiler/backend
Jan 05 09:52:00 Finished compiler/backend                                        15s   1GB
Jan 05 09:52:01 Starting compiler/encoders/asm
Jan 05 09:52:02 Finished compiler/encoders/asm                                    0s  92MB
Jan 05 09:52:03 Starting compiler/encoders/x64
Jan 05 09:52:04 Finished compiler/encoders/x64                                    0s  94MB
Jan 05 09:52:05 Starting compiler/encoders/arm7
Jan 05 09:52:06 Finished compiler/encoders/arm7                                   0s  94MB
Jan 05 09:52:07 Starting compiler/encoders/arm8
Jan 05 09:52:09 Finished compiler/encoders/arm8                                   0s  93MB
Jan 05 09:52:10 Starting compiler/encoders/arm8_asl
Jan 05 09:54:27 Finished compiler/encoders/arm8_asl                            2m16s   1GB
Jan 05 09:54:28 Starting compiler/encoders/mips
Jan 05 09:54:29 Finished compiler/encoders/mips                                   0s  92MB
Jan 05 09:54:30 Starting compiler/encoders/riscv
Jan 05 09:54:31 Finished compiler/encoders/riscv                                  0s  91MB
Jan 05 09:54:32 Starting compiler/encoders/ag32
Jan 05 09:54:34 Finished compiler/encoders/ag32                                   0s  85MB
Jan 05 09:54:35 Starting compiler/backend/x64
Jan 05 09:54:36 Finished compiler/backend/x64                                     0s 129MB
Jan 05 09:54:37 Starting compiler/backend/arm7
Jan 05 09:54:39 Finished compiler/backend/arm7                                    0s 124MB
Jan 05 09:54:40 Starting compiler/backend/arm8
Jan 05 09:54:41 Finished compiler/backend/arm8                                    0s 121MB
Jan 05 09:54:42 Starting compiler/backend/mips
Jan 05 09:54:44 Finished compiler/backend/mips                                    0s 122MB
Jan 05 09:54:45 Starting compiler/backend/riscv
Jan 05 09:54:46 Finished compiler/backend/riscv                                   0s 121MB
Jan 05 09:54:47 Starting compiler/backend/ag32
Jan 05 09:56:05 Finished compiler/backend/ag32                                 1m16s   3GB
Jan 05 09:56:05 Starting compiler/parsing/proofs
Jan 05 09:56:07 Finished compiler/parsing/proofs                                  0s  75MB
Jan 05 09:56:08 Starting compiler/inference/proofs
Jan 05 09:56:09 Finished compiler/inference/proofs                                0s  86MB
Jan 05 09:56:10 Starting compiler/backend/semantics
Jan 05 09:57:37 Finished compiler/backend/semantics                            1m26s   3GB
Jan 05 09:57:38 Starting compiler/backend/reg_alloc/proofs
Jan 05 09:57:39 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Jan 05 09:57:40 Starting compiler/backend/proofs
Jan 05 09:58:41 Finished compiler/backend/proofs                               1m00s   3GB
Jan 05 09:58:42 Starting compiler/backend/serialiser
Jan 05 09:58:44 Finished compiler/backend/serialiser                              1s 195MB
Jan 05 09:58:45 Starting compiler/encoders/x64/proofs
Jan 05 10:08:11 Finished compiler/encoders/x64/proofs                          9m25s   5GB
Jan 05 10:08:12 Starting compiler/encoders/arm7/proofs
Jan 05 10:20:58 Finished compiler/encoders/arm7/proofs                        12m44s  11GB
Jan 05 10:20:59 Starting compiler/encoders/arm8/proofs
Jan 05 10:27:32 Finished compiler/encoders/arm8/proofs                         6m32s   5GB
Jan 05 10:27:33 Starting compiler/encoders/arm8_asl/proofs
Jan 05 10:41:30 Finished compiler/encoders/arm8_asl/proofs                    13m55s   4GB
Jan 05 10:41:31 Starting compiler/encoders/mips/proofs
Jan 05 10:51:34 Finished compiler/encoders/mips/proofs                        10m02s   5GB
Jan 05 10:51:35 Starting compiler/encoders/riscv/proofs
Jan 05 10:59:50 Finished compiler/encoders/riscv/proofs                        8m14s   4GB
Jan 05 10:59:51 Starting compiler/encoders/ag32/proofs
Jan 05 11:02:14 Finished compiler/encoders/ag32/proofs                         2m22s   2GB
Jan 05 11:02:15 Starting compiler/backend/x64/proofs
Jan 05 11:02:56 Finished compiler/backend/x64/proofs                             40s   2GB
Jan 05 11:02:57 Starting compiler/backend/arm7/proofs
Jan 05 11:03:38 Finished compiler/backend/arm7/proofs                            40s   2GB
Jan 05 11:03:39 Starting compiler/backend/arm8/proofs
Jan 05 11:04:17 Finished compiler/backend/arm8/proofs                            37s   2GB
Jan 05 11:04:18 Starting compiler/backend/arm8_asl
Jan 05 11:04:47 Finished compiler/backend/arm8_asl                               27s   2GB
Jan 05 11:04:47 Starting compiler/backend/mips/proofs
Jan 05 11:05:31 Finished compiler/backend/mips/proofs                            43s   3GB
Jan 05 11:05:32 Starting compiler/backend/riscv/proofs
Jan 05 11:06:23 Finished compiler/backend/riscv/proofs                           49s   3GB
Jan 05 11:06:24 Starting compiler/backend/ag32/proofs
Jan 05 11:19:19 Finished compiler/backend/ag32/proofs                         12m54s   5GB
Jan 05 11:19:20 Starting candle/set-theory
Jan 05 11:20:04 Finished candle/set-theory                                       43s   1GB
Jan 05 11:20:05 Starting candle/syntax-lib
Jan 05 11:20:06 Finished candle/syntax-lib                                        0s  67MB
Jan 05 11:20:07 Starting candle/standard/syntax
Jan 05 11:20:24 Finished candle/standard/syntax                                  15s   1GB
Jan 05 11:20:24 Starting candle/standard/semantics
Jan 05 11:22:47 Finished candle/standard/semantics                             2m21s   3GB
Jan 05 11:22:48 Starting candle/standard/monadic
Jan 05 11:22:49 Finished candle/standard/monadic                                  0s 104MB
Jan 05 11:22:50 Starting candle/standard/ml_kernel
Jan 05 11:24:36 Finished candle/standard/ml_kernel                             1m45s   4GB
Jan 05 11:24:37 Starting candle/overloading/syntax
Jan 05 11:27:55 Finished candle/overloading/syntax                             3m17s   2GB
Jan 05 11:27:56 Starting candle/overloading/semantics
Jan 05 11:39:08 Finished candle/overloading/semantics                         11m11s   5GB
Jan 05 11:39:09 Starting candle/overloading/monadic
Jan 05 11:41:45 Finished candle/overloading/monadic                            2m35s   3GB
Jan 05 11:41:46 Starting candle/overloading/ml_kernel
Jan 05 11:49:13 Finished candle/overloading/ml_kernel                          7m25s   6GB
Jan 05 11:49:14 Starting candle/overloading/ml_checker
Jan 05 11:51:46 Finished candle/overloading/ml_checker                         2m31s   7GB
Jan 05 11:51:47 Starting candle/prover
Jan 05 12:01:30 Finished candle/prover                                         9m41s   5GB
Jan 05 12:01:31 Starting pancake
Jan 05 12:02:29 Finished pancake                                                 58s   1GB
Jan 05 12:02:30 Starting pancake/ffi
Jan 05 12:02:31 Finished pancake/ffi                                              0s  21MB
Jan 05 12:02:32 Starting pancake/semantics
Jan 05 12:04:56 Finished pancake/semantics                                     2m22s   2GB
Jan 05 12:04:57 Starting pancake/parser
Jan 05 12:05:24 Finished pancake/parser                                          26s   2GB
Jan 05 12:05:25 Starting pancake/proofs
Jan 05 12:34:55 Finished pancake/proofs                                       29m29s   8GB
Jan 05 12:34:56 Starting characteristic/examples
Jan 05 12:36:33 Finished characteristic/examples                               1m36s   5GB
Jan 05 12:36:34 Starting tutorial/solutions
Jan 05 12:51:53 Finished tutorial/solutions                                   15m18s  10GB
Jan 05 12:51:54 Starting translator/monadic/examples
Jan 05 12:55:38 Finished translator/monadic/examples                           3m42s   4GB
Jan 05 12:55:39 Starting examples
Jan 05 13:10:08 Finished examples                                             14m27s   7GB
Jan 05 13:10:08 Starting examples/compilation/x64
Jan 05 15:07:32 Finished examples/compilation/x64                           1h57m22s  33GB
Jan 05 15:07:33 Starting examples/compilation/x64/proofs
Jan 05 15:11:22 Finished examples/compilation/x64/proofs                       3m48s   6GB
Jan 05 15:11:23 Starting examples/compilation/ag32
Jan 05 15:40:57 Finished examples/compilation/ag32                            29m33s  14GB
Jan 05 15:40:58 Starting examples/compilation/ag32/proofs
Jan 05 15:42:26 Finished examples/compilation/ag32/proofs                      1m27s   6GB
Jan 05 15:42:27 Starting examples/compilation/to_word
Jan 05 15:46:14 Finished examples/compilation/to_word                          3m46s  11GB
Jan 05 15:46:15 Starting examples/lpr_checker
Jan 05 15:47:30 Finished examples/lpr_checker                                  1m14s   2GB
Jan 05 15:47:31 Starting examples/lpr_checker/array
Jan 05 16:16:14 Finished examples/lpr_checker/array                           28m42s  11GB
Jan 05 16:16:14 Starting examples/lpr_checker/array/compilation
Jan 05 16:50:36 Finished examples/lpr_checker/array/compilation               34m20s  54GB
Jan 05 16:50:37 Starting examples/lpr_checker/array/compilation/proofs
Jan 05 16:52:26 Finished examples/lpr_checker/array/compilation/proofs         1m48s   9GB
Jan 05 16:52:27 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 05 17:04:24 Finished examples/lpr_checker/array/compilation/proofsARM8    11m55s  39GB
Jan 05 17:04:24 Starting examples/pseudo_bool
Jan 05 17:06:23 Finished examples/pseudo_bool                                  1m58s   2GB
Jan 05 17:06:24 Starting examples/pseudo_bool/cnf_encoding
Jan 05 17:07:00 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Jan 05 17:07:01 Starting examples/pseudo_bool/graph_encoding
Jan 05 17:07:51 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Jan 05 17:07:52 Starting examples/pseudo_bool/array
Jan 05 17:57:29 Finished examples/pseudo_bool/array                           49m35s  17GB
Jan 05 17:57:29 Starting examples/pseudo_bool/array/compilation
Jan 05 19:45:44 Finished examples/pseudo_bool/array/compilation             1h48m13s  97GB
Jan 05 19:45:44 Starting examples/pseudo_bool/array/compilation/proofs
Jan 05 19:48:44 Finished examples/pseudo_bool/array/compilation/proofs         2m58s   7GB
Jan 05 19:48:44 Starting examples/opentheory
Jan 05 19:59:16 Finished examples/opentheory                                  10m30s   7GB
Jan 05 19:59:16 Starting examples/opentheory
Jan 05 19:59:18 Finished examples/opentheory                                      0s 123MB
Jan 05 19:59:19 Starting examples/opentheory/compilation
Jan 05 20:34:38 Finished examples/opentheory/compilation                      35m18s  65GB
Jan 05 20:34:39 Starting examples/opentheory/compilation/proofs
Jan 05 20:36:06 Finished examples/opentheory/compilation/proofs                1m25s   6GB
Jan 05 20:36:07 Starting examples/opentheory/compilation/ag32
Jan 05 21:07:24 Finished examples/opentheory/compilation/ag32                 31m15s  45GB
Jan 05 21:07:25 Starting examples/opentheory/compilation/ag32/proofs
Jan 05 21:09:40 Finished examples/opentheory/compilation/ag32/proofs           2m14s  11GB
Jan 05 21:09:41 Starting examples/sat_encodings
Jan 05 21:12:14 Finished examples/sat_encodings                                2m31s   1GB
Jan 05 21:12:14 Starting examples/sat_encodings/case_studies
Jan 05 21:14:12 Finished examples/sat_encodings/case_studies                   1m56s   2GB
Jan 05 21:14:12 Starting examples/sat_encodings/translation
Jan 05 21:20:15 Finished examples/sat_encodings/translation                    6m01s   7GB
Jan 05 21:20:16 Starting examples/sat_encodings/translation/compilation
Jan 05 21:55:25 Finished examples/sat_encodings/translation/compilation       35m08s  38GB
Jan 05 21:55:26 Starting examples/deflate
Jan 05 21:56:40 Finished examples/deflate                                      1m13s   1GB
Jan 05 21:56:41 Starting examples/deflate/translation
Jan 05 21:58:20 Finished examples/deflate/translation                          1m38s   7GB
Jan 05 21:58:21 Starting examples/deflate/translation/compilation
Jan 05 22:14:31 Finished examples/deflate/translation/compilation             16m08s  14GB
Jan 05 22:14:32 Starting examples/vipr
Jan 05 22:18:30 Finished examples/vipr                                         3m57s   7GB
Jan 05 22:18:31 Starting examples/vipr/compilation
Jan 05 22:37:58 Finished examples/vipr/compilation                            19m26s  33GB
Jan 05 22:37:59 Starting translator/okasaki-examples
Jan 05 22:42:58 Finished translator/okasaki-examples                           4m57s   4GB
Jan 05 22:42:59 Starting translator/other-examples
Jan 05 22:46:33 Finished translator/other-examples                             3m33s   3GB
Jan 05 22:46:34 Starting compiler/parsing/tests
Jan 05 22:47:07 Finished compiler/parsing/tests                                  32s   1GB
Jan 05 22:47:08 Starting compiler/inference/tests
Jan 05 22:54:38 Finished compiler/inference/tests                              7m29s   7GB
Jan 05 22:54:39 Starting compiler/printing/test
Jan 05 22:58:09 Finished compiler/printing/test                                3m29s   6GB
Jan 05 22:58:10 Starting icing/flover
Jan 05 23:33:19 Finished icing/flover                                         35m08s   4GB
Jan 05 23:33:20 Starting icing/
Jan 06 00:28:06 Finished icing/                                               54m44s  25GB
Jan 06 00:28:07 Starting icing/examples
Jan 06 00:29:50 Finished icing/examples                                        1m42s   8GB
Jan 06 00:29:51 Starting compiler/repl
Jan 06 00:38:27 Finished compiler/repl                                         8m35s   9GB
Jan 06 00:38:28 Starting unverified/sexpr-bootstrap/x64/64
Jan 06 00:49:44 Finished unverified/sexpr-bootstrap/x64/64                    10m54s  15GB
Jan 06 00:49:45 Starting unverified/sexpr-bootstrap/x64/32
Jan 06 00:58:54 Finished unverified/sexpr-bootstrap/x64/32                     8m51s  13GB
Jan 06 00:58:55 Starting compiler/benchmarks
Jan 06 00:59:40 Finished compiler/benchmarks                                     43s 713MB
Jan 06 00:59:40 Starting compiler/bootstrap/compilation/x64/64
Jan 06 15:21:39 Finished compiler/bootstrap/compilation/x64/64             14h21m46s 139GB
Jan 06 15:21:40 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 06 15:42:47 Finished compiler/bootstrap/compilation/x64/64/proofs         21m06s  45GB
Jan 06 15:42:48 Starting compiler/bootstrap/compilation/x64/32
Jan 06 22:50:01 Finished compiler/bootstrap/compilation/x64/32              7h07m05s 114GB
Jan 06 22:50:02 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 06 22:53:39 Finished compiler/bootstrap/compilation/x64/32/proofs          3m36s  18GB
Jan 06 22:53:40 Starting compiler/bootstrap/compilation/ag32/32
Jan 07 06:23:46 Finished compiler/bootstrap/compilation/ag32/32             7h30m04s 135GB
Jan 07 06:23:47 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 07 06:31:03 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m14s  38GB
Jan 07 06:31:04 SUCCESS