Job 2695

CakeML:8c68847abd8fee8b25a2e9fbacd3a2089f6e986d
  Merge pull request #1087 from CakeML/mktnk3-patch-1 [Nov 12 07:20:53]
HOL:2de6b3ccc36da9c19998787a835c3ef9c81466fe
  Add a cute problem to examples/misc [Oct 30 04:33:10]
Machine:lammmington
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 18:57:06 Claimed job
Nov 12 18:57:09 Reusing HOL
Nov 12 18:57:21 Starting developers
Nov 12 18:57:25 Finished developers                                               3s  87MB
Nov 12 18:57:26 Starting developers/bin
Nov 12 18:57:49 Finished developers/bin                                          22s   1GB
Nov 12 18:57:50 Starting compiler/proofs
Nov 12 20:40:45 Finished compiler/proofs                                    1h42m54s  28GB
Nov 12 20:40:46 Starting compiler/bootstrap/translation
Nov 13 05:42:30 Finished compiler/bootstrap/translation                     9h01m42s  56GB
Nov 13 05:42:31 Starting semantics/ffi
Nov 13 05:42:47 Finished semantics/ffi                                           15s   1GB
Nov 13 05:42:48 Starting semantics
Nov 13 05:42:49 Finished semantics                                                0s  62MB
Nov 13 05:42:50 Starting semantics/proofs
Nov 13 05:43:14 Finished semantics/proofs                                        23s 647MB
Nov 13 05:43:15 Starting semantics/alt_semantics
Nov 13 05:43:36 Finished semantics/alt_semantics                                 20s 487MB
Nov 13 05:43:38 Starting semantics/alt_semantics/proofs
Nov 13 05:53:51 Finished semantics/alt_semantics/proofs                       10m12s   2GB
Nov 13 05:53:52 Starting basis/pure
Nov 13 05:53:53 Finished basis/pure                                               0s  70MB
Nov 13 05:53:54 Starting translator
Nov 13 05:55:27 Finished translator                                            1m31s   2GB
Nov 13 05:55:27 Starting compiler/parsing
Nov 13 05:55:29 Finished compiler/parsing                                         0s  72MB
Nov 13 05:55:30 Starting characteristic
Nov 13 05:55:32 Finished characteristic                                           0s  93MB
Nov 13 05:55:32 Starting translator/monadic
Nov 13 05:55:34 Finished translator/monadic                                       0s  99MB
Nov 13 05:55:35 Starting basis
Nov 13 05:57:56 Finished basis                                                 2m20s   4GB
Nov 13 05:57:57 Starting compiler/inference
Nov 13 05:57:59 Finished compiler/inference                                       0s  93MB
Nov 13 05:58:00 Starting compiler/backend/reg_alloc
Nov 13 05:58:01 Finished compiler/backend/reg_alloc                               0s  65MB
Nov 13 05:58:02 Starting compiler/backend/gc
Nov 13 05:58:04 Finished compiler/backend/gc                                      1s 138MB
Nov 13 05:58:05 Starting compiler/backend
Nov 13 05:58:10 Finished compiler/backend                                         4s 307MB
Nov 13 05:58:11 Starting compiler/encoders/asm
Nov 13 05:58:13 Finished compiler/encoders/asm                                    0s  89MB
Nov 13 05:58:14 Starting compiler/encoders/x64
Nov 13 05:58:15 Finished compiler/encoders/x64                                    0s 103MB
Nov 13 05:58:16 Starting compiler/encoders/arm7
Nov 13 05:58:18 Finished compiler/encoders/arm7                                   0s 101MB
Nov 13 05:58:19 Starting compiler/encoders/arm8
Nov 13 05:58:20 Finished compiler/encoders/arm8                                   0s  99MB
Nov 13 05:58:21 Starting compiler/encoders/arm8_asl
Nov 13 06:00:36 Finished compiler/encoders/arm8_asl                            2m13s   1GB
Nov 13 06:00:37 Starting compiler/encoders/mips
Nov 13 06:00:38 Finished compiler/encoders/mips                                   0s  99MB
Nov 13 06:00:39 Starting compiler/encoders/riscv
Nov 13 06:00:41 Finished compiler/encoders/riscv                                  0s  99MB
Nov 13 06:00:42 Starting compiler/encoders/ag32
Nov 13 06:00:43 Finished compiler/encoders/ag32                                   0s  97MB
Nov 13 06:00:44 Starting compiler/backend/x64
Nov 13 06:00:46 Finished compiler/backend/x64                                     1s 137MB
Nov 13 06:00:47 Starting compiler/backend/arm7
Nov 13 06:00:49 Finished compiler/backend/arm7                                    1s 138MB
Nov 13 06:00:50 Starting compiler/backend/arm8
Nov 13 06:00:52 Finished compiler/backend/arm8                                    1s 138MB
Nov 13 06:00:53 Starting compiler/backend/mips
Nov 13 06:00:55 Finished compiler/backend/mips                                    1s 138MB
Nov 13 06:00:56 Starting compiler/backend/riscv
Nov 13 06:00:58 Finished compiler/backend/riscv                                   1s 138MB
Nov 13 06:00:59 Starting compiler/backend/ag32
Nov 13 06:02:10 Finished compiler/backend/ag32                                 1m10s   2GB
Nov 13 06:02:11 Starting compiler/parsing/proofs
Nov 13 06:02:13 Finished compiler/parsing/proofs                                  0s  73MB
Nov 13 06:02:14 Starting compiler/inference/proofs
Nov 13 06:02:15 Finished compiler/inference/proofs                                0s  99MB
Nov 13 06:02:16 Starting compiler/backend/semantics
Nov 13 06:05:31 Finished compiler/backend/semantics                            3m13s   2GB
Nov 13 06:05:32 Starting compiler/backend/reg_alloc/proofs
Nov 13 06:05:34 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Nov 13 06:05:35 Starting compiler/backend/proofs
Nov 13 06:06:28 Finished compiler/backend/proofs                                 52s   3GB
Nov 13 06:06:29 Starting compiler/backend/serialiser
Nov 13 06:06:31 Finished compiler/backend/serialiser                              1s 140MB
Nov 13 06:06:32 Starting compiler/encoders/x64/proofs
Nov 13 06:16:44 Finished compiler/encoders/x64/proofs                         10m11s   5GB
Nov 13 06:16:45 Starting compiler/encoders/arm7/proofs
Nov 13 06:29:50 Finished compiler/encoders/arm7/proofs                        13m04s   7GB
Nov 13 06:29:51 Starting compiler/encoders/arm8/proofs
Nov 13 06:36:46 Finished compiler/encoders/arm8/proofs                         6m54s   4GB
Nov 13 06:36:47 Starting compiler/encoders/arm8_asl/proofs
Nov 13 06:51:43 Finished compiler/encoders/arm8_asl/proofs                    14m55s   4GB
Nov 13 06:51:44 Starting compiler/encoders/mips/proofs
Nov 13 07:01:47 Finished compiler/encoders/mips/proofs                        10m01s   5GB
Nov 13 07:01:48 Starting compiler/encoders/riscv/proofs
Nov 13 07:09:54 Finished compiler/encoders/riscv/proofs                        8m05s   3GB
Nov 13 07:09:55 Starting compiler/encoders/ag32/proofs
Nov 13 07:12:49 Finished compiler/encoders/ag32/proofs                         2m53s   2GB
Nov 13 07:12:50 Starting compiler/backend/x64/proofs
Nov 13 07:13:36 Finished compiler/backend/x64/proofs                             44s   3GB
Nov 13 07:13:37 Starting compiler/backend/arm7/proofs
Nov 13 07:14:25 Finished compiler/backend/arm7/proofs                            45s   2GB
Nov 13 07:14:26 Starting compiler/backend/arm8/proofs
Nov 13 07:15:11 Finished compiler/backend/arm8/proofs                            44s   3GB
Nov 13 07:15:12 Starting compiler/backend/arm8_asl
Nov 13 07:15:45 Finished compiler/backend/arm8_asl                               31s   2GB
Nov 13 07:15:46 Starting compiler/backend/mips/proofs
Nov 13 07:16:36 Finished compiler/backend/mips/proofs                            48s   3GB
Nov 13 07:16:37 Starting compiler/backend/riscv/proofs
Nov 13 07:17:31 Finished compiler/backend/riscv/proofs                           53s   3GB
Nov 13 07:17:32 Starting compiler/backend/ag32/proofs
Nov 13 07:31:59 Finished compiler/backend/ag32/proofs                         14m26s   6GB
Nov 13 07:32:00 Starting compiler/backend/cv_compute
Nov 13 07:33:51 Finished compiler/backend/cv_compute                           1m50s   4GB
Nov 13 07:33:52 Starting cv_translator
Nov 13 07:53:50 Finished cv_translator                                        19m57s  13GB
Nov 13 07:53:51 Starting candle/set-theory
Nov 13 07:54:38 Finished candle/set-theory                                       46s   1GB
Nov 13 07:54:39 Starting candle/syntax-lib
Nov 13 07:54:40 Finished candle/syntax-lib                                        0s  69MB
Nov 13 07:54:41 Starting candle/standard/syntax
Nov 13 07:55:00 Finished candle/standard/syntax                                  18s   1GB
Nov 13 07:55:01 Starting candle/standard/semantics
Nov 13 07:57:46 Finished candle/standard/semantics                             2m43s   3GB
Nov 13 07:57:47 Starting candle/standard/monadic
Nov 13 07:57:48 Finished candle/standard/monadic                                  0s 102MB
Nov 13 07:57:49 Starting candle/standard/ml_kernel
Nov 13 07:59:55 Finished candle/standard/ml_kernel                             2m04s   5GB
Nov 13 07:59:56 Starting candle/overloading/syntax
Nov 13 08:03:29 Finished candle/overloading/syntax                             3m32s   2GB
Nov 13 08:03:30 Starting candle/overloading/semantics
Nov 13 08:14:59 Finished candle/overloading/semantics                         11m27s   5GB
Nov 13 08:15:00 Starting candle/overloading/monadic
Nov 13 08:17:25 Finished candle/overloading/monadic                            2m24s   2GB
Nov 13 08:17:26 Starting candle/overloading/ml_kernel
Nov 13 08:25:24 Finished candle/overloading/ml_kernel                          7m56s   6GB
Nov 13 08:25:25 Starting candle/overloading/ml_checker
Nov 13 08:28:11 Finished candle/overloading/ml_checker                         2m46s   7GB
Nov 13 08:28:12 Starting candle/prover
Nov 13 08:38:44 Finished candle/prover                                        10m31s   5GB
Nov 13 08:38:45 Starting pancake
Nov 13 08:39:12 Finished pancake                                                 25s 980MB
Nov 13 08:39:13 Starting pancake/ffi
Nov 13 08:39:13 Finished pancake/ffi                                              0s  22MB
Nov 13 08:39:14 Starting pancake/semantics
Nov 13 08:41:19 Finished pancake/semantics                                     2m03s   2GB
Nov 13 08:41:20 Starting pancake/parser
Nov 13 08:41:44 Finished pancake/parser                                          22s 569MB
Nov 13 08:41:44 Starting pancake/proofs
Nov 13 08:57:40 Finished pancake/proofs                                       15m54s   5GB
Nov 13 08:57:41 Starting compiler/dafny
Nov 13 09:00:18 Finished compiler/dafny                                        2m35s   8GB
Nov 13 09:00:19 Starting compiler/dafny/translation
Nov 13 09:28:53 Finished compiler/dafny/translation                           28m33s  24GB
Nov 13 09:28:54 Starting compiler/dafny/compilation
Nov 13 09:32:32 Finished compiler/dafny/compilation                            3m36s  14GB
Nov 13 09:32:33 Starting compiler/dafny/semantics
Nov 13 09:33:08 Finished compiler/dafny/semantics                                34s   1GB
Nov 13 09:33:09 Starting characteristic/examples
Nov 13 09:34:38 Finished characteristic/examples                               1m28s   5GB
Nov 13 09:34:39 Starting tutorial/solutions
Nov 13 09:37:28 Finished tutorial/solutions                                    2m48s   5GB
Nov 13 09:37:29 Starting translator/monadic/examples
Nov 13 09:40:33 Finished translator/monadic/examples                           3m02s   4GB
Nov 13 09:40:34 Starting examples
Nov 13 09:52:40 Finished examples                                             12m05s   5GB
Nov 13 09:52:41 Starting examples/compilation/x64
Nov 13 10:02:49 Finished examples/compilation/x64                             10m07s   7GB
Nov 13 10:02:50 Starting examples/compilation/x64/proofs
Nov 13 10:07:36 Finished examples/compilation/x64/proofs                       4m44s   7GB
Nov 13 10:07:37 Starting examples/compilation/ag32
Nov 13 10:10:29 Finished examples/compilation/ag32                             2m50s   5GB
Nov 13 10:10:30 Starting examples/compilation/ag32/proofs
Nov 13 10:12:23 Finished examples/compilation/ag32/proofs                      1m52s  10GB
Nov 13 10:12:24 Starting examples/compilation/to_word
Nov 13 10:16:38 Finished examples/compilation/to_word                          4m12s  13GB
Nov 13 10:16:39 Starting examples/lpr_checker
Nov 13 10:17:09 Finished examples/lpr_checker                                    29s   1GB
Nov 13 10:17:10 Starting examples/lpr_checker/array
Nov 13 10:43:04 Finished examples/lpr_checker/array                           25m53s  18GB
Nov 13 10:43:05 Starting examples/lpr_checker/array/compilation
Nov 13 10:45:45 Finished examples/lpr_checker/array/compilation                2m39s  10GB
Nov 13 10:45:46 Starting examples/lpr_checker/array/compilation/proofs
Nov 13 10:47:51 Finished examples/lpr_checker/array/compilation/proofs         2m03s   8GB
Nov 13 10:47:52 Starting examples/lpr_checker/array/compilation/proofsARM8
Nov 13 10:49:46 Finished examples/lpr_checker/array/compilation/proofsARM8     1m53s   9GB
Nov 13 10:49:47 Starting examples/xlrup_checker
Nov 13 10:50:22 Finished examples/xlrup_checker                                  33s   1GB
Nov 13 10:50:22 Starting examples/xlrup_checker/array
Nov 13 11:03:23 Finished examples/xlrup_checker/array                         12m59s   9GB
Nov 13 11:03:24 Starting examples/xlrup_checker/array/compilation
Nov 13 11:04:54 Finished examples/xlrup_checker/array/compilation              1m29s   7GB
Nov 13 11:04:55 Starting examples/xlrup_checker/array/compilation/proofs
Nov 13 11:06:43 Finished examples/xlrup_checker/array/compilation/proofs       1m46s   8GB
Nov 13 11:06:44 Starting examples/pseudo_bool
Nov 13 11:08:17 Finished examples/pseudo_bool                                  1m32s   2GB
Nov 13 11:08:18 Starting examples/pseudo_bool/cnf_encoding
Nov 13 11:09:00 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Nov 13 11:09:01 Starting examples/pseudo_bool/graph_encoding
Nov 13 11:10:00 Finished examples/pseudo_bool/graph_encoding                     57s   2GB
Nov 13 11:10:01 Starting examples/pseudo_bool/array
Nov 13 12:18:27 Finished examples/pseudo_bool/array                         1h08m25s  38GB
Nov 13 12:18:28 Starting examples/pseudo_bool/array/compilation
Nov 13 12:33:10 Finished examples/pseudo_bool/array/compilation               14m41s  32GB
Nov 13 12:33:11 Starting examples/pseudo_bool/array/compilation/proofs
Nov 13 12:37:36 Finished examples/pseudo_bool/array/compilation/proofs         4m23s   9GB
Nov 13 12:37:37 Starting examples/pseudo_bool/array/compilation/proofsARM8
Nov 13 12:39:36 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m57s   9GB
Nov 13 12:39:36 Starting examples/opentheory
Nov 13 12:48:16 Finished examples/opentheory                                   8m38s   5GB
Nov 13 12:48:17 Starting examples/opentheory
Nov 13 12:48:19 Finished examples/opentheory                                      1s 137MB
Nov 13 12:48:20 Starting examples/opentheory/compilation
Nov 13 12:50:27 Finished examples/opentheory/compilation                       2m06s   9GB
Nov 13 12:50:28 Starting examples/opentheory/compilation/proofs
Nov 13 12:52:18 Finished examples/opentheory/compilation/proofs                1m49s   8GB
Nov 13 12:52:19 Starting examples/opentheory/compilation/ag32
Nov 13 12:54:30 Finished examples/opentheory/compilation/ag32                  2m09s   9GB
Nov 13 12:54:30 Starting examples/opentheory/compilation/ag32/proofs
Nov 13 12:57:06 Finished examples/opentheory/compilation/ag32/proofs           2m34s  12GB
Nov 13 12:57:07 Starting examples/sat_encodings
Nov 13 12:58:07 Finished examples/sat_encodings                                  59s 742MB
Nov 13 12:58:08 Starting examples/sat_encodings/case_studies
Nov 13 13:00:19 Finished examples/sat_encodings/case_studies                   2m10s   2GB
Nov 13 13:00:20 Starting examples/sat_encodings/translation
Nov 13 13:03:52 Finished examples/sat_encodings/translation                    3m30s   2GB
Nov 13 13:03:52 Starting examples/sat_encodings/translation/compilation
Nov 13 13:06:25 Finished examples/sat_encodings/translation/compilation        2m31s   7GB
Nov 13 13:06:26 Starting examples/deflate
Nov 13 13:06:53 Finished examples/deflate                                        26s 735MB
Nov 13 13:06:54 Starting examples/deflate/translation
Nov 13 13:07:53 Finished examples/deflate/translation                            57s   2GB
Nov 13 13:07:53 Starting examples/deflate/translation/compilation
Nov 13 13:09:02 Finished examples/deflate/translation/compilation              1m07s   5GB
Nov 13 13:09:03 Starting examples/vipr
Nov 13 13:12:47 Finished examples/vipr                                         3m43s   7GB
Nov 13 13:12:48 Starting examples/vipr/compilation
Nov 13 13:14:07 Finished examples/vipr/compilation                             1m18s   6GB
Nov 13 13:14:08 Starting translator/okasaki-examples
Nov 13 13:18:23 Finished translator/okasaki-examples                           4m14s   3GB
Nov 13 13:18:24 Starting translator/other-examples
Nov 13 13:19:39 Finished translator/other-examples                             1m13s   3GB
Nov 13 13:19:39 Starting compiler/parsing/tests
Nov 13 13:20:19 Finished compiler/parsing/tests                                  38s   2GB
Nov 13 13:20:19 Starting compiler/inference/tests
Nov 13 13:21:07 Finished compiler/inference/tests                                46s   3GB
Nov 13 13:21:08 Starting compiler/printing/test
Nov 13 13:22:48 Finished compiler/printing/test                                1m38s   7GB
Nov 13 13:22:49 Starting icing/flover
Nov 13 13:59:43 Finished icing/flover                                         36m53s   4GB
Nov 13 13:59:44 Starting icing/
Nov 13 14:27:27 Finished icing/                                               27m42s   9GB
Nov 13 14:27:28 Starting icing/examples
Nov 13 14:29:14 Finished icing/examples                                        1m45s   5GB
Nov 13 14:29:15 Starting compiler/repl
Nov 13 14:38:40 Finished compiler/repl                                         9m24s   9GB
Nov 13 14:38:41 Starting unverified/sexpr-bootstrap/x64/64
Nov 13 14:52:55 Finished unverified/sexpr-bootstrap/x64/64                    13m47s  18GB
Nov 13 14:52:56 Starting unverified/sexpr-bootstrap/x64/32
Nov 13 15:04:26 Finished unverified/sexpr-bootstrap/x64/32                    11m09s  17GB
Nov 13 15:04:27 Starting compiler/benchmarks
Nov 13 15:05:12 Finished compiler/benchmarks                                     44s 711MB
Nov 13 15:05:13 Starting compiler/bootstrap/compilation/x64/64
Nov 13 15:52:03 Finished compiler/bootstrap/compilation/x64/64                46m37s 133GB
Nov 13 15:52:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 13 16:16:38 Finished compiler/bootstrap/compilation/x64/64/proofs         24m32s  49GB
Nov 13 16:16:39 Starting compiler/bootstrap/compilation/x64/32
Nov 13 16:59:23 Finished compiler/bootstrap/compilation/x64/32                42m30s 104GB
Nov 13 16:59:23 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 13 17:04:33 Finished compiler/bootstrap/compilation/x64/32/proofs          5m08s  24GB
Nov 13 17:04:34 Starting compiler/bootstrap/compilation/arm8/64
Nov 13 18:05:17 Finished compiler/bootstrap/compilation/arm8/64             1h00m34s 129GB
Nov 13 18:05:18 Starting compiler/bootstrap/compilation/arm8/64/proofs
Nov 13 18:11:14 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m54s  29GB
Nov 13 18:11:15 Starting compiler/bootstrap/compilation/ag32/32
Nov 13 18:52:39 Finished compiler/bootstrap/compilation/ag32/32               41m23s 109GB
Nov 13 18:52:40 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 13 18:58:21 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m40s  31GB
Nov 13 18:58:22 SUCCESS