Job 2244

CakeML:37aeb0eb6fcddea51846bd6fa7d7496e2ace12a5
  Merge pull request #975 from CakeML/byte [Dec 01 09:41:30]
HOL:a6832b79bc2529f8b2e018a232b66652b9cc9e76
  Merge pull request #1167 from binghe/separability_lemma [Nov 30 23:08:33]
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

Dec 02 03:21:47 Claimed job
Dec 02 03:21:54 Building HOL
Dec 02 03:35:41 Starting developers
Dec 02 03:35:46 Finished developers                                               5s 182MB
Dec 02 03:35:47 Starting developers/bin
Dec 02 03:35:53 Finished developers/bin                                           6s   1GB
Dec 02 03:35:53 Starting compiler/proofs
Dec 02 05:29:34 Finished compiler/proofs                                    1h53m40s  19GB
Dec 02 05:29:34 Starting compiler/bootstrap/translation
Dec 02 13:49:05 Finished compiler/bootstrap/translation                     8h19m31s  44GB
Dec 02 13:49:05 Starting semantics/ffi
Dec 02 13:49:10 Finished semantics/ffi                                            4s 386MB
Dec 02 13:49:10 Starting semantics
Dec 02 13:49:12 Finished semantics                                                1s  18MB
Dec 02 13:49:12 Starting semantics/proofs
Dec 02 13:49:44 Finished semantics/proofs                                        32s 734MB
Dec 02 13:49:44 Starting semantics/alt_semantics
Dec 02 13:50:16 Finished semantics/alt_semantics                                 31s 894MB
Dec 02 13:50:16 Starting semantics/alt_semantics/proofs
Dec 02 14:02:11 Finished semantics/alt_semantics/proofs                       11m54s   1GB
Dec 02 14:02:11 Starting basis/pure
Dec 02 14:02:12 Finished basis/pure                                               1s  20MB
Dec 02 14:02:13 Starting translator
Dec 02 14:04:02 Finished translator                                            1m49s   1GB
Dec 02 14:04:02 Starting compiler/parsing
Dec 02 14:04:04 Finished compiler/parsing                                         1s  18MB
Dec 02 14:04:04 Starting characteristic
Dec 02 14:04:06 Finished characteristic                                           1s  22MB
Dec 02 14:04:06 Starting translator/monadic
Dec 02 14:04:08 Finished translator/monadic                                       1s  20MB
Dec 02 14:04:08 Starting basis
Dec 02 14:07:51 Finished basis                                                 3m42s   2GB
Dec 02 14:07:51 Starting compiler/inference
Dec 02 14:07:52 Finished compiler/inference                                       1s  21MB
Dec 02 14:07:53 Starting compiler/backend/reg_alloc
Dec 02 14:07:54 Finished compiler/backend/reg_alloc                               1s  18MB
Dec 02 14:07:54 Starting compiler/backend/gc
Dec 02 14:07:57 Finished compiler/backend/gc                                      2s  25MB
Dec 02 14:07:57 Starting compiler/backend
Dec 02 14:08:09 Finished compiler/backend                                        12s 736MB
Dec 02 14:08:09 Starting compiler/encoders/asm
Dec 02 14:08:11 Finished compiler/encoders/asm                                    1s  19MB
Dec 02 14:08:11 Starting compiler/encoders/x64
Dec 02 14:08:13 Finished compiler/encoders/x64                                    1s  28MB
Dec 02 14:08:13 Starting compiler/encoders/arm7
Dec 02 14:08:15 Finished compiler/encoders/arm7                                   1s  22MB
Dec 02 14:08:15 Starting compiler/encoders/arm8
Dec 02 14:08:17 Finished compiler/encoders/arm8                                   1s  20MB
Dec 02 14:08:17 Starting compiler/encoders/arm8_asl
Dec 02 16:35:36 Finished compiler/encoders/arm8_asl                         2h27m18s  48GB
Dec 02 16:35:36 Starting compiler/encoders/mips
Dec 02 16:35:38 Finished compiler/encoders/mips                                   1s  23MB
Dec 02 16:35:38 Starting compiler/encoders/riscv
Dec 02 16:35:40 Finished compiler/encoders/riscv                                  1s  23MB
Dec 02 16:35:40 Starting compiler/encoders/ag32
Dec 02 16:35:42 Finished compiler/encoders/ag32                                   1s  19MB
Dec 02 16:35:42 Starting compiler/backend/x64
Dec 02 16:35:44 Finished compiler/backend/x64                                     2s  24MB
Dec 02 16:35:44 Starting compiler/backend/arm7
Dec 02 16:35:46 Finished compiler/backend/arm7                                    2s  25MB
Dec 02 16:35:47 Starting compiler/backend/arm8
Dec 02 16:35:49 Finished compiler/backend/arm8                                    2s  29MB
Dec 02 16:35:49 Starting compiler/backend/mips
Dec 02 16:35:51 Finished compiler/backend/mips                                    2s  24MB
Dec 02 16:35:51 Starting compiler/backend/riscv
Dec 02 16:35:53 Finished compiler/backend/riscv                                   2s  22MB
Dec 02 16:35:54 Starting compiler/backend/ag32
Dec 02 16:37:19 Finished compiler/backend/ag32                                 1m25s   1GB
Dec 02 16:37:19 Starting compiler/parsing/proofs
Dec 02 16:37:21 Finished compiler/parsing/proofs                                  1s  20MB
Dec 02 16:37:21 Starting compiler/inference/proofs
Dec 02 16:37:23 Finished compiler/inference/proofs                                1s  21MB
Dec 02 16:37:23 Starting compiler/backend/semantics
Dec 02 16:38:38 Finished compiler/backend/semantics                            1m14s   1GB
Dec 02 16:38:38 Starting compiler/backend/reg_alloc/proofs
Dec 02 16:38:40 Finished compiler/backend/reg_alloc/proofs                        1s  24MB
Dec 02 16:38:40 Starting compiler/backend/proofs
Dec 02 16:39:38 Finished compiler/backend/proofs                                 58s   2GB
Dec 02 16:39:38 Starting compiler/backend/serialiser
Dec 02 16:39:41 Finished compiler/backend/serialiser                              2s  29MB
Dec 02 16:39:41 Starting compiler/encoders/x64/proofs
Dec 02 16:49:47 Finished compiler/encoders/x64/proofs                         10m05s   4GB
Dec 02 16:49:47 Starting compiler/encoders/arm7/proofs
Dec 02 17:03:34 Finished compiler/encoders/arm7/proofs                        13m47s   4GB
Dec 02 17:03:34 Starting compiler/encoders/arm8/proofs
Dec 02 17:10:28 Finished compiler/encoders/arm8/proofs                         6m53s   1GB
Dec 02 17:10:28 Starting compiler/encoders/arm8_asl/proofs
Dec 02 18:02:58 Finished compiler/encoders/arm8_asl/proofs                    52m29s   8GB
Dec 02 18:02:58 Starting compiler/encoders/mips/proofs
Dec 02 18:13:46 Finished compiler/encoders/mips/proofs                        10m47s   2GB
Dec 02 18:13:46 Starting compiler/encoders/riscv/proofs
Dec 02 18:22:53 Finished compiler/encoders/riscv/proofs                        9m07s   1GB
Dec 02 18:22:53 Starting compiler/encoders/ag32/proofs
Dec 02 18:25:39 Finished compiler/encoders/ag32/proofs                         2m46s 580MB
Dec 02 18:25:39 Starting compiler/backend/x64/proofs
Dec 02 18:26:09 Finished compiler/backend/x64/proofs                             29s   1GB
Dec 02 18:26:09 Starting compiler/backend/arm7/proofs
Dec 02 18:26:43 Finished compiler/backend/arm7/proofs                            33s   2GB
Dec 02 18:26:43 Starting compiler/backend/arm8/proofs
Dec 02 18:27:13 Finished compiler/backend/arm8/proofs                            29s   1GB
Dec 02 18:27:13 Starting compiler/backend/arm8_asl
Dec 02 18:27:37 Finished compiler/backend/arm8_asl                               24s   2GB
Dec 02 18:27:37 Starting compiler/backend/mips/proofs
Dec 02 18:28:08 Finished compiler/backend/mips/proofs                            30s   1GB
Dec 02 18:28:08 Starting compiler/backend/riscv/proofs
Dec 02 18:28:43 Finished compiler/backend/riscv/proofs                           34s   2GB
Dec 02 18:28:43 Starting compiler/backend/ag32/proofs
Dec 02 18:42:26 Finished compiler/backend/ag32/proofs                         13m43s   3GB
Dec 02 18:42:27 Starting candle/set-theory
Dec 02 18:43:06 Finished candle/set-theory                                       39s 988MB
Dec 02 18:43:06 Starting candle/syntax-lib
Dec 02 18:43:08 Finished candle/syntax-lib                                        1s  24MB
Dec 02 18:43:08 Starting candle/standard/syntax
Dec 02 18:43:18 Finished candle/standard/syntax                                  10s 553MB
Dec 02 18:43:18 Starting candle/standard/semantics
Dec 02 18:45:20 Finished candle/standard/semantics                             2m01s   1GB
Dec 02 18:45:20 Starting candle/standard/monadic
Dec 02 18:45:22 Finished candle/standard/monadic                                  1s  25MB
Dec 02 18:45:22 Starting candle/standard/ml_kernel
Dec 02 18:47:01 Finished candle/standard/ml_kernel                             1m38s   3GB
Dec 02 18:47:01 Starting candle/overloading/syntax
Dec 02 18:50:25 Finished candle/overloading/syntax                             3m23s   1GB
Dec 02 18:50:25 Starting candle/overloading/semantics
Dec 02 19:02:46 Finished candle/overloading/semantics                         12m21s   2GB
Dec 02 19:02:46 Starting candle/overloading/monadic
Dec 02 19:05:30 Finished candle/overloading/monadic                            2m43s   1GB
Dec 02 19:05:30 Starting candle/overloading/ml_kernel
Dec 02 19:13:25 Finished candle/overloading/ml_kernel                          7m55s   3GB
Dec 02 19:13:26 Starting candle/overloading/ml_checker
Dec 02 19:15:59 Finished candle/overloading/ml_checker                         2m33s   3GB
Dec 02 19:15:59 Starting candle/prover
Dec 02 19:26:01 Finished candle/prover                                        10m02s   3GB
Dec 02 19:26:02 Starting pancake
Dec 02 19:26:45 Finished pancake                                                 43s 859MB
Dec 02 19:26:45 Starting pancake/ffi
Dec 02 19:26:46 Finished pancake/ffi                                              0s  13MB
Dec 02 19:26:46 Starting pancake/semantics
Dec 02 19:29:11 Finished pancake/semantics                                     2m24s   1GB
Dec 02 19:29:11 Starting pancake/parser
Dec 02 19:29:33 Finished pancake/parser                                          22s   1GB
Dec 02 19:29:33 Starting pancake/proofs
Dec 02 20:02:43 Finished pancake/proofs                                       33m09s   6GB
Dec 02 20:02:43 Starting characteristic/examples
Dec 02 20:04:18 Finished characteristic/examples                               1m35s   1GB
Dec 02 20:04:19 Starting tutorial/solutions
Dec 02 20:19:43 Finished tutorial/solutions                                   15m24s  11GB
Dec 02 20:19:43 Starting translator/monadic/examples
Dec 02 20:23:49 Finished translator/monadic/examples                           4m05s   3GB
Dec 02 20:23:49 Starting examples
Dec 02 20:39:48 Finished examples                                             15m58s   5GB
Dec 02 20:39:48 Starting examples/compilation/x64
Dec 02 22:39:10 Finished examples/compilation/x64                           1h59m22s  18GB
Dec 02 22:39:10 Starting examples/compilation/x64/proofs
Dec 02 22:41:48 Finished examples/compilation/x64/proofs                       2m37s   4GB
Dec 02 22:41:48 Starting examples/compilation/ag32
Dec 02 23:11:45 Finished examples/compilation/ag32                            29m56s  11GB
Dec 02 23:11:45 Starting examples/compilation/ag32/proofs
Dec 02 23:12:48 Finished examples/compilation/ag32/proofs                      1m02s   4GB
Dec 02 23:12:48 Starting examples/compilation/to_word
Dec 02 23:16:25 Finished examples/compilation/to_word                          3m36s   5GB
Dec 02 23:16:25 Starting examples/lpr_checker
Dec 02 23:17:31 Finished examples/lpr_checker                                  1m06s   1GB
Dec 02 23:17:31 Starting examples/lpr_checker/array
Dec 02 23:48:43 Finished examples/lpr_checker/array                           31m11s   5GB
Dec 02 23:48:43 Starting examples/lpr_checker/array/compilation
Dec 03 00:37:42 Finished examples/lpr_checker/array/compilation               48m58s  21GB
Dec 03 00:37:42 Starting examples/lpr_checker/array/compilation/proofs
Dec 03 00:39:42 Finished examples/lpr_checker/array/compilation/proofs         2m00s   3GB
Dec 03 00:39:42 Starting examples/lpr_checker/array/compilation/proofsARM8
Dec 03 00:46:46 Finished examples/lpr_checker/array/compilation/proofsARM8     7m03s  20GB
Dec 03 00:46:46 Starting examples/pseudo_bool
Dec 03 00:48:36 Finished examples/pseudo_bool                                  1m49s   1GB
Dec 03 00:48:36 Starting examples/pseudo_bool/cnf_encoding
Dec 03 00:49:01 Finished examples/pseudo_bool/cnf_encoding                       24s 794MB
Dec 03 00:49:01 Starting examples/pseudo_bool/graph_encoding
Dec 03 00:49:44 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Dec 03 00:49:44 Starting examples/pseudo_bool/array
Dec 03 01:43:04 Finished examples/pseudo_bool/array                           53m19s   7GB
Dec 03 01:43:04 Starting examples/pseudo_bool/array/compilation
Dec 03 04:42:57 Finished examples/pseudo_bool/array/compilation             2h59m52s  50GB
Dec 03 04:42:57 Starting examples/pseudo_bool/array/compilation/proofs
Dec 03 04:45:46 Finished examples/pseudo_bool/array/compilation/proofs         2m49s   5GB
Dec 03 04:45:46 Starting examples/opentheory
Dec 03 04:56:48 Finished examples/opentheory                                  11m01s   7GB
Dec 03 04:56:48 Starting examples/opentheory
Dec 03 04:56:50 Finished examples/opentheory                                      1s  24MB
Dec 03 04:56:50 Starting examples/opentheory/compilation
Dec 03 05:33:50 Finished examples/opentheory/compilation                      37m00s  30GB
Dec 03 05:33:50 Starting examples/opentheory/compilation/proofs
Dec 03 05:34:51 Finished examples/opentheory/compilation/proofs                1m00s   4GB
Dec 03 05:34:51 Starting examples/opentheory/compilation/ag32
Dec 03 06:10:03 Finished examples/opentheory/compilation/ag32                 35m11s  31GB
Dec 03 06:10:03 Starting examples/opentheory/compilation/ag32/proofs
Dec 03 06:12:01 Finished examples/opentheory/compilation/ag32/proofs           1m57s   8GB
Dec 03 06:12:01 Starting examples/sat_encodings
Dec 03 06:14:03 Finished examples/sat_encodings                                2m01s   1GB
Dec 03 06:14:03 Starting examples/sat_encodings/case_studies
Dec 03 06:15:48 Finished examples/sat_encodings/case_studies                   1m45s   1GB
Dec 03 06:15:49 Starting examples/sat_encodings/translation
Dec 03 06:22:06 Finished examples/sat_encodings/translation                    6m17s   4GB
Dec 03 06:22:06 Starting examples/sat_encodings/translation/compilation
Dec 03 07:09:07 Finished examples/sat_encodings/translation/compilation       47m00s  22GB
Dec 03 07:09:07 Starting examples/deflate
Dec 03 07:10:09 Finished examples/deflate                                      1m01s 870MB
Dec 03 07:10:09 Starting examples/deflate/translation
Dec 03 07:12:02 Finished examples/deflate/translation                          1m52s   3GB
Dec 03 07:12:02 Starting examples/deflate/translation/compilation
Dec 03 07:32:20 Finished examples/deflate/translation/compilation             20m18s  13GB
Dec 03 07:32:20 Starting examples/vipr
Dec 03 07:36:23 Finished examples/vipr                                         4m02s   3GB
Dec 03 07:36:23 Starting examples/vipr/compilation
Dec 03 07:57:40 Finished examples/vipr/compilation                            21m16s  16GB
Dec 03 07:57:40 Starting translator/okasaki-examples
Dec 03 08:02:52 Finished translator/okasaki-examples                           5m12s   2GB
Dec 03 08:02:52 Starting translator/other-examples
Dec 03 08:05:35 Finished translator/other-examples                             2m43s   1GB
Dec 03 08:05:35 Starting compiler/parsing/tests
Dec 03 08:06:08 Finished compiler/parsing/tests                                  32s 923MB
Dec 03 08:06:08 Starting compiler/inference/tests
Dec 03 08:14:42 Finished compiler/inference/tests                              8m33s   5GB
Dec 03 08:14:42 Starting compiler/printing/test
Dec 03 08:18:38 Finished compiler/printing/test                                3m55s   2GB
Dec 03 08:18:38 Starting icing/flover
Dec 03 09:02:45 Finished icing/flover                                         44m06s   2GB
Dec 03 09:02:45 Starting icing/
Dec 03 09:57:02 Finished icing/                                               54m17s   8GB
Dec 03 09:57:02 Starting icing/examples
Dec 03 09:58:41 Finished icing/examples                                        1m38s   4GB
Dec 03 09:58:41 Starting compiler/repl
Dec 03 10:07:26 Finished compiler/repl                                         8m44s   5GB
Dec 03 10:07:26 Starting unverified/sexpr-bootstrap/x64/64
Dec 03 10:21:04 Finished unverified/sexpr-bootstrap/x64/64                    13m36s  15GB
Dec 03 10:21:04 Starting unverified/sexpr-bootstrap/x64/32
Dec 03 10:32:11 Finished unverified/sexpr-bootstrap/x64/32                    11m06s  14GB
Dec 03 10:32:11 Starting compiler/benchmarks
Dec 03 10:47:47 Finished compiler/benchmarks                                  15m36s   2GB
Dec 03 10:47:47 Starting compiler/bootstrap/compilation/x64/64
Dec 03 23:41:17 Finished compiler/bootstrap/compilation/x64/64             12h53m29s  64GB
Dec 03 23:41:17 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 04 00:03:22 Finished compiler/bootstrap/compilation/x64/64/proofs         22m05s  44GB
Dec 04 00:03:22 Starting compiler/bootstrap/compilation/x64/32
Dec 04 07:14:10 Finished compiler/bootstrap/compilation/x64/32              7h10m47s  64GB
Dec 04 07:14:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 04 07:17:27 Finished compiler/bootstrap/compilation/x64/32/proofs          3m16s  18GB
Dec 04 07:17:27 Starting compiler/bootstrap/compilation/ag32/32
Dec 04 14:36:43 Finished compiler/bootstrap/compilation/ag32/32             7h19m16s  64GB
Dec 04 14:36:44 Starting compiler/bootstrap/compilation/ag32/32/proofs
Dec 04 14:43:49 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m05s  23GB
Dec 04 14:43:49 SUCCESS