Job 2344

CakeML:98d0d03c9e52b27a9895186563d385583deb75a2
  Merge pull request #984 from CakeML/compression [Mar 10 14:36:06]
HOL:3a51c81db857b7722efa0871ac507883adf6d440
  Remove compilerTheory (put its content at end of codegenTheory) [Mar 11 19:26:17]
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

Mar 16 00:03:01 Claimed job
Mar 16 00:03:06 Reusing HOL
Mar 16 00:03:48 Starting developers
Mar 16 00:03:53 Finished developers                                               5s 136MB
Mar 16 00:03:53 Starting developers/bin
Mar 16 00:04:00 Finished developers/bin                                           5s   1GB
Mar 16 00:04:00 Starting compiler/proofs
Mar 16 01:55:58 Finished compiler/proofs                                    1h51m58s  25GB
Mar 16 01:55:59 Starting compiler/bootstrap/translation
Mar 16 10:11:50 Finished compiler/bootstrap/translation                     8h15m51s  36GB
Mar 16 10:11:50 Starting semantics/ffi
Mar 16 10:11:56 Finished semantics/ffi                                            5s 206MB
Mar 16 10:11:56 Starting semantics
Mar 16 10:11:58 Finished semantics                                                1s  21MB
Mar 16 10:11:58 Starting semantics/proofs
Mar 16 10:12:31 Finished semantics/proofs                                        32s 724MB
Mar 16 10:12:31 Starting semantics/alt_semantics
Mar 16 10:13:03 Finished semantics/alt_semantics                                 31s 653MB
Mar 16 10:13:03 Starting semantics/alt_semantics/proofs
Mar 16 10:24:56 Finished semantics/alt_semantics/proofs                       11m53s   1GB
Mar 16 10:24:56 Starting basis/pure
Mar 16 10:24:58 Finished basis/pure                                               1s  20MB
Mar 16 10:24:58 Starting translator
Mar 16 10:26:51 Finished translator                                            1m52s   1GB
Mar 16 10:26:51 Starting compiler/parsing
Mar 16 10:26:52 Finished compiler/parsing                                         1s  18MB
Mar 16 10:26:53 Starting characteristic
Mar 16 10:26:55 Finished characteristic                                           1s  24MB
Mar 16 10:26:55 Starting translator/monadic
Mar 16 10:26:57 Finished translator/monadic                                       1s  20MB
Mar 16 10:26:57 Starting basis
Mar 16 10:30:37 Finished basis                                                 3m40s   3GB
Mar 16 10:30:37 Starting compiler/inference
Mar 16 10:30:39 Finished compiler/inference                                       1s  25MB
Mar 16 10:30:39 Starting compiler/backend/reg_alloc
Mar 16 10:30:41 Finished compiler/backend/reg_alloc                               1s  20MB
Mar 16 10:30:41 Starting compiler/backend/gc
Mar 16 10:30:43 Finished compiler/backend/gc                                      2s  25MB
Mar 16 10:30:43 Starting compiler/backend
Mar 16 10:30:56 Finished compiler/backend                                        12s 822MB
Mar 16 10:30:56 Starting compiler/encoders/asm
Mar 16 10:30:58 Finished compiler/encoders/asm                                    1s  23MB
Mar 16 10:30:58 Starting compiler/encoders/x64
Mar 16 10:31:00 Finished compiler/encoders/x64                                    1s  20MB
Mar 16 10:31:00 Starting compiler/encoders/arm7
Mar 16 10:31:02 Finished compiler/encoders/arm7                                   1s  20MB
Mar 16 10:31:02 Starting compiler/encoders/arm8
Mar 16 10:31:04 Finished compiler/encoders/arm8                                   1s  23MB
Mar 16 10:31:04 Starting compiler/encoders/arm8_asl
Mar 16 10:34:18 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Mar 16 10:34:18 Starting compiler/encoders/mips
Mar 16 10:34:20 Finished compiler/encoders/mips                                   1s  23MB
Mar 16 10:34:20 Starting compiler/encoders/riscv
Mar 16 10:34:22 Finished compiler/encoders/riscv                                  1s  25MB
Mar 16 10:34:22 Starting compiler/encoders/ag32
Mar 16 10:34:24 Finished compiler/encoders/ag32                                   1s  24MB
Mar 16 10:34:24 Starting compiler/backend/x64
Mar 16 10:34:26 Finished compiler/backend/x64                                     2s  26MB
Mar 16 10:34:26 Starting compiler/backend/arm7
Mar 16 10:34:29 Finished compiler/backend/arm7                                    2s  26MB
Mar 16 10:34:29 Starting compiler/backend/arm8
Mar 16 10:34:31 Finished compiler/backend/arm8                                    2s  25MB
Mar 16 10:34:31 Starting compiler/backend/mips
Mar 16 10:34:33 Finished compiler/backend/mips                                    2s  27MB
Mar 16 10:34:33 Starting compiler/backend/riscv
Mar 16 10:34:36 Finished compiler/backend/riscv                                   2s  27MB
Mar 16 10:34:36 Starting compiler/backend/ag32
Mar 16 10:36:01 Finished compiler/backend/ag32                                 1m25s   1GB
Mar 16 10:36:01 Starting compiler/parsing/proofs
Mar 16 10:36:03 Finished compiler/parsing/proofs                                  1s  19MB
Mar 16 10:36:03 Starting compiler/inference/proofs
Mar 16 10:36:05 Finished compiler/inference/proofs                                1s  22MB
Mar 16 10:36:05 Starting compiler/backend/semantics
Mar 16 10:37:19 Finished compiler/backend/semantics                            1m13s   1GB
Mar 16 10:37:19 Starting compiler/backend/reg_alloc/proofs
Mar 16 10:37:21 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Mar 16 10:37:21 Starting compiler/backend/proofs
Mar 16 10:38:18 Finished compiler/backend/proofs                                 57s   2GB
Mar 16 10:38:18 Starting compiler/backend/serialiser
Mar 16 10:38:21 Finished compiler/backend/serialiser                              2s  33MB
Mar 16 10:38:22 Starting compiler/encoders/x64/proofs
Mar 16 10:48:11 Finished compiler/encoders/x64/proofs                          9m49s   5GB
Mar 16 10:48:11 Starting compiler/encoders/arm7/proofs
Mar 16 11:01:56 Finished compiler/encoders/arm7/proofs                        13m44s   4GB
Mar 16 11:01:56 Starting compiler/encoders/arm8/proofs
Mar 16 11:08:56 Finished compiler/encoders/arm8/proofs                         7m00s   1GB
Mar 16 11:08:56 Starting compiler/encoders/arm8_asl/proofs
Mar 16 11:24:44 Finished compiler/encoders/arm8_asl/proofs                    15m47s   2GB
Mar 16 11:24:44 Starting compiler/encoders/mips/proofs
Mar 16 11:35:25 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Mar 16 11:35:25 Starting compiler/encoders/riscv/proofs
Mar 16 11:44:36 Finished compiler/encoders/riscv/proofs                        9m10s   1GB
Mar 16 11:44:36 Starting compiler/encoders/ag32/proofs
Mar 16 11:47:07 Finished compiler/encoders/ag32/proofs                         2m31s   1GB
Mar 16 11:47:07 Starting compiler/backend/x64/proofs
Mar 16 11:47:39 Finished compiler/backend/x64/proofs                             31s   2GB
Mar 16 11:47:39 Starting compiler/backend/arm7/proofs
Mar 16 11:48:11 Finished compiler/backend/arm7/proofs                            32s   1GB
Mar 16 11:48:11 Starting compiler/backend/arm8/proofs
Mar 16 11:48:41 Finished compiler/backend/arm8/proofs                            29s   1GB
Mar 16 11:48:41 Starting compiler/backend/arm8_asl
Mar 16 11:49:06 Finished compiler/backend/arm8_asl                               24s   2GB
Mar 16 11:49:06 Starting compiler/backend/mips/proofs
Mar 16 11:49:40 Finished compiler/backend/mips/proofs                            33s   2GB
Mar 16 11:49:40 Starting compiler/backend/riscv/proofs
Mar 16 11:50:14 Finished compiler/backend/riscv/proofs                           33s   2GB
Mar 16 11:50:14 Starting compiler/backend/ag32/proofs
Mar 16 12:04:00 Finished compiler/backend/ag32/proofs                         13m45s   2GB
Mar 16 12:04:00 Starting candle/set-theory
Mar 16 12:04:40 Finished candle/set-theory                                       39s   1GB
Mar 16 12:04:40 Starting candle/syntax-lib
Mar 16 12:04:41 Finished candle/syntax-lib                                        1s  20MB
Mar 16 12:04:41 Starting candle/standard/syntax
Mar 16 12:04:53 Finished candle/standard/syntax                                  11s 671MB
Mar 16 12:04:53 Starting candle/standard/semantics
Mar 16 12:06:52 Finished candle/standard/semantics                             1m59s   2GB
Mar 16 12:06:52 Starting candle/standard/monadic
Mar 16 12:06:54 Finished candle/standard/monadic                                  1s  27MB
Mar 16 12:06:54 Starting candle/standard/ml_kernel
Mar 16 12:08:36 Finished candle/standard/ml_kernel                             1m41s   3GB
Mar 16 12:08:36 Starting candle/overloading/syntax
Mar 16 12:12:03 Finished candle/overloading/syntax                             3m27s   1GB
Mar 16 12:12:03 Starting candle/overloading/semantics
Mar 16 12:24:37 Finished candle/overloading/semantics                         12m33s   2GB
Mar 16 12:24:37 Starting candle/overloading/monadic
Mar 16 12:27:24 Finished candle/overloading/monadic                            2m46s   1GB
Mar 16 12:27:24 Starting candle/overloading/ml_kernel
Mar 16 12:35:27 Finished candle/overloading/ml_kernel                          8m03s   3GB
Mar 16 12:35:27 Starting candle/overloading/ml_checker
Mar 16 12:38:03 Finished candle/overloading/ml_checker                         2m36s   2GB
Mar 16 12:38:04 Starting candle/prover
Mar 16 12:47:59 Finished candle/prover                                         9m55s   4GB
Mar 16 12:48:00 Starting pancake
Mar 16 12:48:45 Finished pancake                                                 45s 849MB
Mar 16 12:48:45 Starting pancake/ffi
Mar 16 12:48:45 Finished pancake/ffi                                              0s  13MB
Mar 16 12:48:45 Starting pancake/semantics
Mar 16 12:51:12 Finished pancake/semantics                                     2m26s   1GB
Mar 16 12:51:12 Starting pancake/parser
Mar 16 12:51:34 Finished pancake/parser                                          22s   1GB
Mar 16 12:51:34 Starting pancake/proofs
Mar 16 13:25:01 Finished pancake/proofs                                       33m26s   5GB
Mar 16 13:25:01 Starting characteristic/examples
Mar 16 13:26:36 Finished characteristic/examples                               1m34s   2GB
Mar 16 13:26:36 Starting tutorial/solutions
Mar 16 13:41:50 Finished tutorial/solutions                                   15m13s   9GB
Mar 16 13:41:50 Starting translator/monadic/examples
Mar 16 13:45:57 Finished translator/monadic/examples                           4m06s   3GB
Mar 16 13:45:57 Starting examples
Mar 16 14:01:37 Finished examples                                             15m39s   5GB
Mar 16 14:01:37 Starting examples/compilation/x64
Mar 16 16:00:37 Finished examples/compilation/x64                           1h59m00s  19GB
Mar 16 16:00:37 Starting examples/compilation/x64/proofs
Mar 16 16:03:12 Finished examples/compilation/x64/proofs                       2m34s   4GB
Mar 16 16:03:12 Starting examples/compilation/ag32
Mar 16 16:33:34 Finished examples/compilation/ag32                            30m21s   6GB
Mar 16 16:33:34 Starting examples/compilation/ag32/proofs
Mar 16 16:34:36 Finished examples/compilation/ag32/proofs                      1m01s   4GB
Mar 16 16:34:36 Starting examples/compilation/to_word
Mar 16 16:38:01 Finished examples/compilation/to_word                          3m25s   6GB
Mar 16 16:38:01 Starting examples/lpr_checker
Mar 16 16:39:08 Finished examples/lpr_checker                                  1m06s   1GB
Mar 16 16:39:08 Starting examples/lpr_checker/array
Mar 16 17:11:41 Finished examples/lpr_checker/array                           32m32s   6GB
Mar 16 17:11:41 Starting examples/lpr_checker/array/compilation
Mar 16 18:02:28 Finished examples/lpr_checker/array/compilation               50m46s  24GB
Mar 16 18:02:28 Starting examples/lpr_checker/array/compilation/proofs
Mar 16 18:04:15 Finished examples/lpr_checker/array/compilation/proofs         1m46s   3GB
Mar 16 18:04:15 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 16 18:09:48 Finished examples/lpr_checker/array/compilation/proofsARM8     5m32s  20GB
Mar 16 18:09:48 Starting examples/xlrup_checker
Mar 16 18:10:48 Finished examples/xlrup_checker                                1m00s   1GB
Mar 16 18:10:48 Starting examples/xlrup_checker/array
Mar 16 18:28:37 Finished examples/xlrup_checker/array                         17m48s   4GB
Mar 16 18:28:37 Starting examples/xlrup_checker/array/compilation
Mar 16 18:50:47 Finished examples/xlrup_checker/array/compilation             22m09s  16GB
Mar 16 18:50:47 Starting examples/xlrup_checker/array/compilation/proofs
Mar 16 18:51:47 Finished examples/xlrup_checker/array/compilation/proofs         59s   4GB
Mar 16 18:51:47 Starting examples/pseudo_bool
Mar 16 18:53:43 Finished examples/pseudo_bool                                  1m56s   1GB
Mar 16 18:53:43 Starting examples/pseudo_bool/cnf_encoding
Mar 16 18:54:10 Finished examples/pseudo_bool/cnf_encoding                       26s 632MB
Mar 16 18:54:10 Starting examples/pseudo_bool/graph_encoding
Mar 16 18:54:52 Finished examples/pseudo_bool/graph_encoding                     42s 758MB
Mar 16 18:54:53 Starting examples/pseudo_bool/array
Mar 16 20:02:04 Finished examples/pseudo_bool/array                         1h07m11s   8GB
Mar 16 20:02:04 Starting examples/pseudo_bool/array/compilation
Mar 17 03:28:06 Finished examples/pseudo_bool/array/compilation             7h26m01s  62GB
Mar 17 03:28:06 Starting examples/pseudo_bool/array/compilation/proofs
Mar 17 03:30:44 Finished examples/pseudo_bool/array/compilation/proofs         2m38s   6GB
Mar 17 03:30:44 Starting examples/opentheory
Mar 17 03:41:44 Finished examples/opentheory                                  11m00s   4GB
Mar 17 03:41:45 Starting examples/opentheory
Mar 17 03:41:46 Finished examples/opentheory                                      1s  28MB
Mar 17 03:41:46 Starting examples/opentheory/compilation
Mar 17 04:19:54 Finished examples/opentheory/compilation                      38m06s  32GB
Mar 17 04:19:54 Starting examples/opentheory/compilation/proofs
Mar 17 04:20:55 Finished examples/opentheory/compilation/proofs                1m00s   5GB
Mar 17 04:20:55 Starting examples/opentheory/compilation/ag32
Mar 17 04:54:29 Finished examples/opentheory/compilation/ag32                 33m34s  30GB
Mar 17 04:54:29 Starting examples/opentheory/compilation/ag32/proofs
Mar 17 04:56:23 Finished examples/opentheory/compilation/ag32/proofs           1m53s   5GB
Mar 17 04:56:23 Starting examples/sat_encodings
Mar 17 04:58:29 Finished examples/sat_encodings                                2m06s 905MB
Mar 17 04:58:29 Starting examples/sat_encodings/case_studies
Mar 17 05:00:16 Finished examples/sat_encodings/case_studies                   1m46s   1GB
Mar 17 05:00:16 Starting examples/sat_encodings/translation
Mar 17 05:06:30 Finished examples/sat_encodings/translation                    6m14s   3GB
Mar 17 05:06:30 Starting examples/sat_encodings/translation/compilation
Mar 17 05:53:10 Finished examples/sat_encodings/translation/compilation       46m39s  19GB
Mar 17 05:53:10 Starting examples/deflate
Mar 17 05:54:11 Finished examples/deflate                                      1m00s 951MB
Mar 17 05:54:11 Starting examples/deflate/translation
Mar 17 05:56:02 Finished examples/deflate/translation                          1m50s   3GB
Mar 17 05:56:02 Starting examples/deflate/translation/compilation
Mar 17 06:16:12 Finished examples/deflate/translation/compilation             20m10s  14GB
Mar 17 06:16:12 Starting examples/vipr
Mar 17 06:20:18 Finished examples/vipr                                         4m05s   3GB
Mar 17 06:20:18 Starting examples/vipr/compilation
Mar 17 06:41:52 Finished examples/vipr/compilation                            21m33s  18GB
Mar 17 06:41:52 Starting translator/okasaki-examples
Mar 17 06:47:04 Finished translator/okasaki-examples                           5m11s   1GB
Mar 17 06:47:04 Starting translator/other-examples
Mar 17 06:47:58 Finished translator/other-examples                               53s   1GB
Mar 17 06:47:59 Starting compiler/parsing/tests
Mar 17 06:48:31 Finished compiler/parsing/tests                                  32s 800MB
Mar 17 06:48:31 Starting compiler/inference/tests
Mar 17 06:57:07 Finished compiler/inference/tests                              8m35s   4GB
Mar 17 06:57:07 Starting compiler/printing/test
Mar 17 07:00:54 Finished compiler/printing/test                                3m47s   3GB
Mar 17 07:00:54 Starting icing/flover
Mar 17 07:44:41 Finished icing/flover                                         43m46s   2GB
Mar 17 07:44:41 Starting icing/
Mar 17 08:39:00 Finished icing/                                               54m19s  11GB
Mar 17 08:39:00 Starting icing/examples
Mar 17 08:40:34 Finished icing/examples                                        1m33s   4GB
Mar 17 08:40:34 Starting compiler/repl
Mar 17 08:49:27 Finished compiler/repl                                         8m52s   5GB
Mar 17 08:49:27 Starting unverified/sexpr-bootstrap/x64/64
Mar 17 09:03:18 Finished unverified/sexpr-bootstrap/x64/64                    13m49s  15GB
Mar 17 09:03:18 Starting unverified/sexpr-bootstrap/x64/32
Mar 17 09:14:20 Finished unverified/sexpr-bootstrap/x64/32                    11m01s  14GB
Mar 17 09:14:20 Starting compiler/benchmarks
Mar 17 09:29:57 Finished compiler/benchmarks                                  15m37s   2GB
Mar 17 09:29:57 Starting compiler/bootstrap/compilation/x64/64
Mar 17 21:44:58 Finished compiler/bootstrap/compilation/x64/64             12h14m59s  64GB
Mar 17 21:44:58 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 17 22:06:10 Finished compiler/bootstrap/compilation/x64/64/proofs         21m11s  31GB
Mar 17 22:06:10 Starting compiler/bootstrap/compilation/x64/32
Mar 18 05:17:57 Finished compiler/bootstrap/compilation/x64/32              7h11m46s  64GB
Mar 18 05:17:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 18 05:21:26 Finished compiler/bootstrap/compilation/x64/32/proofs          3m29s  18GB
Mar 18 05:21:27 Starting compiler/bootstrap/compilation/ag32/32
Mar 18 13:05:50 Finished compiler/bootstrap/compilation/ag32/32             7h44m22s  64GB
Mar 18 13:05:50 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 18 13:13:01 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m11s  39GB
Mar 18 13:13:02 SUCCESS