Job 2696

CakeML:6437d8c9f25ff64ea9e67c86f1bbde12de199ed7
  Merge pull request #1084 from CakeML/use_eval_raw [Nov 12 19:49:44]
HOL:2de6b3ccc36da9c19998787a835c3ef9c81466fe
  Add a cute problem to examples/misc [Oct 30 04:33:10]
Machine:pavlova
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-arm8-64.tar.gz
cake-x64-32.tar.gz

Nov 12 20:20:46 Claimed job
Nov 12 20:20:53 Reusing HOL
Nov 12 20:21:05 Starting developers
Nov 12 20:21:09 Finished developers                                               3s 216MB
Nov 12 20:21:10 Starting developers/bin
Nov 12 20:21:31 Finished developers/bin                                          20s   1GB
Nov 12 20:21:32 Starting compiler/proofs
Nov 12 22:05:16 Finished compiler/proofs                                    1h43m42s  50GB
Nov 12 22:05:17 Starting compiler/bootstrap/translation
Nov 13 07:09:45 Finished compiler/bootstrap/translation                     9h04m26s  57GB
Nov 13 07:09:45 Starting semantics/ffi
Nov 13 07:10:02 Finished semantics/ffi                                           15s   1GB
Nov 13 07:10:03 Starting semantics
Nov 13 07:10:04 Finished semantics                                                0s  62MB
Nov 13 07:10:05 Starting semantics/proofs
Nov 13 07:10:28 Finished semantics/proofs                                        22s 863MB
Nov 13 07:10:29 Starting semantics/alt_semantics
Nov 13 07:10:51 Finished semantics/alt_semantics                                 20s 643MB
Nov 13 07:10:52 Starting semantics/alt_semantics/proofs
Nov 13 07:21:00 Finished semantics/alt_semantics/proofs                       10m06s   2GB
Nov 13 07:21:01 Starting basis/pure
Nov 13 07:21:02 Finished basis/pure                                               0s  70MB
Nov 13 07:21:03 Starting translator
Nov 13 07:22:40 Finished translator                                            1m35s   4GB
Nov 13 07:22:41 Starting compiler/parsing
Nov 13 07:22:42 Finished compiler/parsing                                         0s  72MB
Nov 13 07:22:43 Starting characteristic
Nov 13 07:22:45 Finished characteristic                                           0s  95MB
Nov 13 07:22:46 Starting translator/monadic
Nov 13 07:22:48 Finished translator/monadic                                       0s  99MB
Nov 13 07:22:50 Starting basis
Nov 13 07:25:12 Finished basis                                                 2m21s   4GB
Nov 13 07:25:13 Starting compiler/inference
Nov 13 07:25:18 Finished compiler/inference                                       0s  92MB
Nov 13 07:25:19 Starting compiler/backend/reg_alloc
Nov 13 07:25:21 Finished compiler/backend/reg_alloc                               0s  67MB
Nov 13 07:25:22 Starting compiler/backend/gc
Nov 13 07:25:24 Finished compiler/backend/gc                                      1s 148MB
Nov 13 07:25:25 Starting compiler/backend
Nov 13 07:25:30 Finished compiler/backend                                         4s 327MB
Nov 13 07:25:31 Starting compiler/encoders/asm
Nov 13 07:25:33 Finished compiler/encoders/asm                                    0s  89MB
Nov 13 07:25:34 Starting compiler/encoders/x64
Nov 13 07:25:35 Finished compiler/encoders/x64                                    0s  99MB
Nov 13 07:25:37 Starting compiler/encoders/arm7
Nov 13 07:25:38 Finished compiler/encoders/arm7                                   0s 105MB
Nov 13 07:25:40 Starting compiler/encoders/arm8
Nov 13 07:25:42 Finished compiler/encoders/arm8                                   0s  99MB
Nov 13 07:25:43 Starting compiler/encoders/arm8_asl
Nov 13 07:27:56 Finished compiler/encoders/arm8_asl                            2m11s   1GB
Nov 13 07:27:57 Starting compiler/encoders/mips
Nov 13 07:27:58 Finished compiler/encoders/mips                                   0s  99MB
Nov 13 07:27:59 Starting compiler/encoders/riscv
Nov 13 07:28:01 Finished compiler/encoders/riscv                                  0s  98MB
Nov 13 07:28:02 Starting compiler/encoders/ag32
Nov 13 07:28:05 Finished compiler/encoders/ag32                                   0s  89MB
Nov 13 07:28:06 Starting compiler/backend/x64
Nov 13 07:28:09 Finished compiler/backend/x64                                     1s 139MB
Nov 13 07:28:10 Starting compiler/backend/arm7
Nov 13 07:28:12 Finished compiler/backend/arm7                                    1s 139MB
Nov 13 07:28:13 Starting compiler/backend/arm8
Nov 13 07:28:15 Finished compiler/backend/arm8                                    1s 137MB
Nov 13 07:28:16 Starting compiler/backend/mips
Nov 13 07:28:18 Finished compiler/backend/mips                                    1s 137MB
Nov 13 07:28:19 Starting compiler/backend/riscv
Nov 13 07:28:21 Finished compiler/backend/riscv                                   1s 137MB
Nov 13 07:28:22 Starting compiler/backend/ag32
Nov 13 07:29:34 Finished compiler/backend/ag32                                 1m11s   3GB
Nov 13 07:29:36 Starting compiler/parsing/proofs
Nov 13 07:29:37 Finished compiler/parsing/proofs                                  0s  75MB
Nov 13 07:29:38 Starting compiler/inference/proofs
Nov 13 07:29:42 Finished compiler/inference/proofs                                0s 100MB
Nov 13 07:29:43 Starting compiler/backend/semantics
Nov 13 07:32:52 Finished compiler/backend/semantics                            3m08s   2GB
Nov 13 07:32:53 Starting compiler/backend/reg_alloc/proofs
Nov 13 07:32:55 Finished compiler/backend/reg_alloc/proofs                        0s 102MB
Nov 13 07:32:56 Starting compiler/backend/proofs
Nov 13 07:33:52 Finished compiler/backend/proofs                                 55s   2GB
Nov 13 07:33:53 Starting compiler/backend/serialiser
Nov 13 07:33:55 Finished compiler/backend/serialiser                              1s 148MB
Nov 13 07:33:56 Starting compiler/encoders/x64/proofs
Nov 13 07:44:04 Finished compiler/encoders/x64/proofs                         10m06s   5GB
Nov 13 07:44:05 Starting compiler/encoders/arm7/proofs
Nov 13 07:57:13 Finished compiler/encoders/arm7/proofs                        13m07s   9GB
Nov 13 07:57:14 Starting compiler/encoders/arm8/proofs
Nov 13 08:04:14 Finished compiler/encoders/arm8/proofs                         6m59s   4GB
Nov 13 08:04:15 Starting compiler/encoders/arm8_asl/proofs
Nov 13 08:19:18 Finished compiler/encoders/arm8_asl/proofs                    15m02s   4GB
Nov 13 08:19:19 Starting compiler/encoders/mips/proofs
Nov 13 08:29:41 Finished compiler/encoders/mips/proofs                        10m20s   5GB
Nov 13 08:29:42 Starting compiler/encoders/riscv/proofs
Nov 13 08:38:07 Finished compiler/encoders/riscv/proofs                        8m24s   3GB
Nov 13 08:38:08 Starting compiler/encoders/ag32/proofs
Nov 13 08:41:05 Finished compiler/encoders/ag32/proofs                         2m55s   2GB
Nov 13 08:41:06 Starting compiler/backend/x64/proofs
Nov 13 08:41:53 Finished compiler/backend/x64/proofs                             46s   3GB
Nov 13 08:41:54 Starting compiler/backend/arm7/proofs
Nov 13 08:42:43 Finished compiler/backend/arm7/proofs                            48s   3GB
Nov 13 08:42:44 Starting compiler/backend/arm8/proofs
Nov 13 08:43:31 Finished compiler/backend/arm8/proofs                            46s   3GB
Nov 13 08:43:32 Starting compiler/backend/arm8_asl
Nov 13 08:44:05 Finished compiler/backend/arm8_asl                               31s   2GB
Nov 13 08:44:06 Starting compiler/backend/mips/proofs
Nov 13 08:44:56 Finished compiler/backend/mips/proofs                            49s   3GB
Nov 13 08:44:57 Starting compiler/backend/riscv/proofs
Nov 13 08:45:55 Finished compiler/backend/riscv/proofs                           56s   4GB
Nov 13 08:45:56 Starting compiler/backend/ag32/proofs
Nov 13 09:00:23 Finished compiler/backend/ag32/proofs                         14m26s   6GB
Nov 13 09:00:24 Starting compiler/backend/cv_compute
Nov 13 09:02:15 Finished compiler/backend/cv_compute                           1m50s   3GB
Nov 13 09:02:16 Starting cv_translator
Nov 13 09:21:59 Finished cv_translator                                        19m41s  13GB
Nov 13 09:22:00 Starting candle/set-theory
Nov 13 09:22:47 Finished candle/set-theory                                       46s   1GB
Nov 13 09:22:48 Starting candle/syntax-lib
Nov 13 09:22:49 Finished candle/syntax-lib                                        0s  69MB
Nov 13 09:22:50 Starting candle/standard/syntax
Nov 13 09:23:09 Finished candle/standard/syntax                                  18s   1GB
Nov 13 09:23:10 Starting candle/standard/semantics
Nov 13 09:25:53 Finished candle/standard/semantics                             2m42s   3GB
Nov 13 09:25:54 Starting candle/standard/monadic
Nov 13 09:25:55 Finished candle/standard/monadic                                  0s 102MB
Nov 13 09:25:56 Starting candle/standard/ml_kernel
Nov 13 09:28:01 Finished candle/standard/ml_kernel                             2m03s   5GB
Nov 13 09:28:02 Starting candle/overloading/syntax
Nov 13 09:31:35 Finished candle/overloading/syntax                             3m32s   2GB
Nov 13 09:31:36 Starting candle/overloading/semantics
Nov 13 09:43:14 Finished candle/overloading/semantics                         11m37s   3GB
Nov 13 09:43:15 Starting candle/overloading/monadic
Nov 13 09:45:42 Finished candle/overloading/monadic                            2m26s   2GB
Nov 13 09:45:43 Starting candle/overloading/ml_kernel
Nov 13 09:53:39 Finished candle/overloading/ml_kernel                          7m55s   6GB
Nov 13 09:53:40 Starting candle/overloading/ml_checker
Nov 13 09:56:24 Finished candle/overloading/ml_checker                         2m43s   7GB
Nov 13 09:56:25 Starting candle/prover
Nov 13 10:07:02 Finished candle/prover                                        10m36s   6GB
Nov 13 10:07:03 Starting pancake
Nov 13 10:07:30 Finished pancake                                                 25s 968MB
Nov 13 10:07:31 Starting pancake/ffi
Nov 13 10:07:32 Finished pancake/ffi                                              0s  23MB
Nov 13 10:07:33 Starting pancake/semantics
Nov 13 10:09:39 Finished pancake/semantics                                     2m05s   2GB
Nov 13 10:09:40 Starting pancake/parser
Nov 13 10:10:05 Finished pancake/parser                                          24s 475MB
Nov 13 10:10:06 Starting pancake/proofs
Nov 13 10:26:11 Finished pancake/proofs                                       16m03s   6GB
Nov 13 10:26:12 Starting compiler/dafny
Nov 13 10:28:43 Finished compiler/dafny                                        2m30s  10GB
Nov 13 10:28:44 Starting compiler/dafny/translation
Nov 13 10:57:42 Finished compiler/dafny/translation                           28m56s  19GB
Nov 13 10:57:43 Starting compiler/dafny/compilation
Nov 13 11:00:19 Finished compiler/dafny/compilation                            2m35s  10GB
Nov 13 11:00:20 Starting compiler/dafny/semantics
Nov 13 11:00:55 Finished compiler/dafny/semantics                                33s   1GB
Nov 13 11:00:56 Starting characteristic/examples
Nov 13 11:02:26 Finished characteristic/examples                               1m29s   5GB
Nov 13 11:02:27 Starting tutorial/solutions
Nov 13 11:05:01 Finished tutorial/solutions                                    2m33s   6GB
Nov 13 11:05:02 Starting translator/monadic/examples
Nov 13 11:08:09 Finished translator/monadic/examples                           3m05s   3GB
Nov 13 11:08:10 Starting examples
Nov 13 11:20:27 Finished examples                                             12m16s   4GB
Nov 13 11:20:28 Starting examples/compilation/x64
Nov 13 11:28:22 Finished examples/compilation/x64                              7m52s   6GB
Nov 13 11:28:23 Starting examples/compilation/x64/proofs
Nov 13 11:33:20 Finished examples/compilation/x64/proofs                       4m55s   7GB
Nov 13 11:33:20 Starting examples/compilation/ag32
Nov 13 11:35:40 Finished examples/compilation/ag32                             2m18s   3GB
Nov 13 11:35:41 Starting examples/compilation/ag32/proofs
Nov 13 11:37:41 Finished examples/compilation/ag32/proofs                      1m58s  10GB
Nov 13 11:37:42 Starting examples/compilation/to_word
Nov 13 11:41:56 Finished examples/compilation/to_word                          4m13s  13GB
Nov 13 11:41:57 Starting examples/lpr_checker
Nov 13 11:42:27 Finished examples/lpr_checker                                    29s   1GB
Nov 13 11:42:28 Starting examples/lpr_checker/array
Nov 13 12:08:40 Finished examples/lpr_checker/array                           26m10s  23GB
Nov 13 12:08:41 Starting examples/lpr_checker/array/compilation
Nov 13 12:10:31 Finished examples/lpr_checker/array/compilation                1m48s   7GB
Nov 13 12:10:32 Starting examples/lpr_checker/array/compilation/proofs
Nov 13 12:12:40 Finished examples/lpr_checker/array/compilation/proofs         2m07s   7GB
Nov 13 12:12:41 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 13 12:14:37 Finished examples/lpr_checker/array/compilation/proofsARM8     1m55s   8GB
Nov 13 12:14:38 Starting examples/xlrup_checker
Nov 13 12:15:13 Finished examples/xlrup_checker                                  34s   1GB
Nov 13 12:15:14 Starting examples/xlrup_checker/array
Nov 13 12:28:24 Finished examples/xlrup_checker/array                         13m08s   8GB
Nov 13 12:28:25 Starting examples/xlrup_checker/array/compilation
Nov 13 12:29:27 Finished examples/xlrup_checker/array/compilation              1m00s   4GB
Nov 13 12:29:28 Starting examples/xlrup_checker/array/compilation/proofs
Nov 13 12:31:19 Finished examples/xlrup_checker/array/compilation/proofs       1m50s   8GB
Nov 13 12:31:20 Starting examples/pseudo_bool
Nov 13 12:32:51 Finished examples/pseudo_bool                                  1m29s   2GB
Nov 13 12:32:52 Starting examples/pseudo_bool/cnf_encoding
Nov 13 12:33:34 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Nov 13 12:33:35 Starting examples/pseudo_bool/graph_encoding
Nov 13 12:34:31 Finished examples/pseudo_bool/graph_encoding                     55s   1GB
Nov 13 12:34:32 Starting examples/pseudo_bool/array
Nov 13 13:43:25 Finished examples/pseudo_bool/array                         1h08m51s  32GB
Nov 13 13:43:26 Starting examples/pseudo_bool/array/compilation
Nov 13 13:52:25 Finished examples/pseudo_bool/array/compilation                8m58s  16GB
Nov 13 13:52:26 Starting examples/pseudo_bool/array/compilation/proofs
Nov 13 13:56:45 Finished examples/pseudo_bool/array/compilation/proofs         4m17s  11GB
Nov 13 13:56:46 Starting examples/pseudo_bool/array/compilation/proofsARM8
Nov 13 13:58:53 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m06s   7GB
Nov 13 13:58:54 Starting examples/opentheory
Nov 13 14:07:41 Finished examples/opentheory                                   8m45s   5GB
Nov 13 14:07:42 Starting examples/opentheory
Nov 13 14:07:44 Finished examples/opentheory                                      1s 133MB
Nov 13 14:07:44 Starting examples/opentheory/compilation
Nov 13 14:09:15 Finished examples/opentheory/compilation                       1m29s   5GB
Nov 13 14:09:15 Starting examples/opentheory/compilation/proofs
Nov 13 14:11:05 Finished examples/opentheory/compilation/proofs                1m48s   7GB
Nov 13 14:11:06 Starting examples/opentheory/compilation/ag32
Nov 13 14:12:43 Finished examples/opentheory/compilation/ag32                  1m36s   6GB
Nov 13 14:12:44 Starting examples/opentheory/compilation/ag32/proofs
Nov 13 14:15:17 Finished examples/opentheory/compilation/ag32/proofs           2m32s  12GB
Nov 13 14:15:18 Starting examples/sat_encodings
Nov 13 14:16:19 Finished examples/sat_encodings                                1m00s 882MB
Nov 13 14:16:20 Starting examples/sat_encodings/case_studies
Nov 13 14:18:30 Finished examples/sat_encodings/case_studies                   2m09s   2GB
Nov 13 14:18:31 Starting examples/sat_encodings/translation
Nov 13 14:22:09 Finished examples/sat_encodings/translation                    3m36s   4GB
Nov 13 14:22:10 Starting examples/sat_encodings/translation/compilation
Nov 13 14:24:03 Finished examples/sat_encodings/translation/compilation        1m52s   4GB
Nov 13 14:24:04 Starting examples/deflate
Nov 13 14:24:31 Finished examples/deflate                                        26s 673MB
Nov 13 14:24:32 Starting examples/deflate/translation
Nov 13 14:25:31 Finished examples/deflate/translation                            58s   2GB
Nov 13 14:25:32 Starting examples/deflate/translation/compilation
Nov 13 14:26:24 Finished examples/deflate/translation/compilation                51s   3GB
Nov 13 14:26:25 Starting examples/vipr
Nov 13 14:30:08 Finished examples/vipr                                         3m42s   7GB
Nov 13 14:30:09 Starting examples/vipr/compilation
Nov 13 14:31:07 Finished examples/vipr/compilation                               57s   4GB
Nov 13 14:31:08 Starting translator/okasaki-examples
Nov 13 14:35:21 Finished translator/okasaki-examples                           4m11s   3GB
Nov 13 14:35:22 Starting translator/other-examples
Nov 13 14:36:37 Finished translator/other-examples                             1m14s   3GB
Nov 13 14:36:38 Starting compiler/parsing/tests
Nov 13 14:37:17 Finished compiler/parsing/tests                                  38s   2GB
Nov 13 14:37:18 Starting compiler/inference/tests
Nov 13 14:38:03 Finished compiler/inference/tests                                44s   3GB
Nov 13 14:38:04 Starting compiler/printing/test
Nov 13 14:39:45 Finished compiler/printing/test                                1m39s   6GB
Nov 13 14:39:46 Starting icing/flover
Nov 13 15:16:30 Finished icing/flover                                         36m42s   4GB
Nov 13 15:16:30 Starting icing/
Nov 13 15:44:07 Finished icing/                                               27m35s   5GB
Nov 13 15:44:08 Starting icing/examples
Nov 13 15:45:53 Finished icing/examples                                        1m43s   5GB
Nov 13 15:45:53 Starting compiler/repl
Nov 13 15:55:01 Finished compiler/repl                                         9m06s  10GB
Nov 13 15:55:02 Starting unverified/sexpr-bootstrap/x64/64
Nov 13 16:09:18 Finished unverified/sexpr-bootstrap/x64/64                    13m49s  18GB
Nov 13 16:09:19 Starting unverified/sexpr-bootstrap/x64/32
Nov 13 16:20:50 Finished unverified/sexpr-bootstrap/x64/32                    11m11s  15GB
Nov 13 16:20:51 Starting compiler/benchmarks
Nov 13 16:21:36 Finished compiler/benchmarks                                     44s 711MB
Nov 13 16:21:37 Starting compiler/bootstrap/compilation/x64/64
Nov 13 16:44:31 Finished compiler/bootstrap/compilation/x64/64                22m39s  67GB
Nov 13 16:44:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 13 17:10:06 Finished compiler/bootstrap/compilation/x64/64/proofs         25m33s  52GB
Nov 13 17:10:07 Starting compiler/bootstrap/compilation/x64/32
Nov 13 17:35:48 Finished compiler/bootstrap/compilation/x64/32                25m32s  71GB
Nov 13 17:35:49 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 13 17:40:52 Finished compiler/bootstrap/compilation/x64/32/proofs          5m02s  24GB
Nov 13 17:40:53 Starting compiler/bootstrap/compilation/arm8/64
Nov 13 18:16:52 Finished compiler/bootstrap/compilation/arm8/64               35m50s  93GB
Nov 13 18:16:53 Starting compiler/bootstrap/compilation/arm8/64/proofs
Nov 13 18:23:16 Finished compiler/bootstrap/compilation/arm8/64/proofs         6m22s  31GB
Nov 13 18:23:17 Starting compiler/bootstrap/compilation/ag32/32
Nov 13 18:50:41 Finished compiler/bootstrap/compilation/ag32/32               27m23s  46GB
Nov 13 18:50:42 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 13 18:56:33 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m49s  29GB
Nov 13 18:56:34 SUCCESS