Job 2364

CakeML:9c063a7d92cadb36c49a6e45856ae0db734dc9e5
  Merge pull request #989 from CakeML/pan_errors [Apr 11 22:24:05]
HOL:4fbc78b13a185c10c1f054e79a41611c7318dcc0
  Transfer more theorems semi-automatically to monoid as type theory [Apr 09 08:24:34]
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

Apr 11 22:26:53 Claimed job
Apr 11 22:27:00 Building HOL
Apr 11 22:40:04 Starting developers
Apr 11 22:40:10 Finished developers                                               5s 119MB
Apr 11 22:40:10 Starting developers/bin
Apr 11 22:40:16 Finished developers/bin                                           6s   1GB
Apr 11 22:40:16 Starting compiler/proofs
Apr 12 00:41:15 Finished compiler/proofs                                    2h00m58s  18GB
Apr 12 00:41:15 Starting compiler/bootstrap/translation
Apr 12 09:25:04 Finished compiler/bootstrap/translation                     8h43m48s  34GB
Apr 12 09:25:05 Starting semantics/ffi
Apr 12 09:25:10 Finished semantics/ffi                                            4s 385MB
Apr 12 09:25:10 Starting semantics
Apr 12 09:25:11 Finished semantics                                                1s  19MB
Apr 12 09:25:11 Starting semantics/proofs
Apr 12 09:25:44 Finished semantics/proofs                                        32s 804MB
Apr 12 09:25:44 Starting semantics/alt_semantics
Apr 12 09:26:17 Finished semantics/alt_semantics                                 32s 716MB
Apr 12 09:26:17 Starting semantics/alt_semantics/proofs
Apr 12 09:38:13 Finished semantics/alt_semantics/proofs                       11m55s   1GB
Apr 12 09:38:13 Starting basis/pure
Apr 12 09:38:15 Finished basis/pure                                               1s  20MB
Apr 12 09:38:15 Starting translator
Apr 12 09:40:04 Finished translator                                            1m48s   2GB
Apr 12 09:40:04 Starting compiler/parsing
Apr 12 09:40:06 Finished compiler/parsing                                         1s  20MB
Apr 12 09:40:06 Starting characteristic
Apr 12 09:40:08 Finished characteristic                                           1s  22MB
Apr 12 09:40:08 Starting translator/monadic
Apr 12 09:40:10 Finished translator/monadic                                       1s  23MB
Apr 12 09:40:10 Starting basis
Apr 12 09:43:58 Finished basis                                                 3m48s   3GB
Apr 12 09:43:59 Starting compiler/inference
Apr 12 09:44:00 Finished compiler/inference                                       1s  19MB
Apr 12 09:44:00 Starting compiler/backend/reg_alloc
Apr 12 09:44:02 Finished compiler/backend/reg_alloc                               1s  27MB
Apr 12 09:44:02 Starting compiler/backend/gc
Apr 12 09:44:04 Finished compiler/backend/gc                                      2s  21MB
Apr 12 09:44:05 Starting compiler/backend
Apr 12 09:44:17 Finished compiler/backend                                        12s 576MB
Apr 12 09:44:17 Starting compiler/encoders/asm
Apr 12 09:44:19 Finished compiler/encoders/asm                                    1s  27MB
Apr 12 09:44:19 Starting compiler/encoders/x64
Apr 12 09:44:21 Finished compiler/encoders/x64                                    1s  26MB
Apr 12 09:44:21 Starting compiler/encoders/arm7
Apr 12 09:44:23 Finished compiler/encoders/arm7                                   1s  28MB
Apr 12 09:44:23 Starting compiler/encoders/arm8
Apr 12 09:44:25 Finished compiler/encoders/arm8                                   1s  23MB
Apr 12 09:44:25 Starting compiler/encoders/arm8_asl
Apr 12 12:10:01 Finished compiler/encoders/arm8_asl                         2h25m36s  33GB
Apr 12 12:10:01 Starting compiler/encoders/mips
Apr 12 12:10:03 Finished compiler/encoders/mips                                   1s  20MB
Apr 12 12:10:03 Starting compiler/encoders/riscv
Apr 12 12:10:05 Finished compiler/encoders/riscv                                  1s  24MB
Apr 12 12:10:05 Starting compiler/encoders/ag32
Apr 12 12:10:07 Finished compiler/encoders/ag32                                   1s  24MB
Apr 12 12:10:07 Starting compiler/backend/x64
Apr 12 12:10:09 Finished compiler/backend/x64                                     2s  23MB
Apr 12 12:10:10 Starting compiler/backend/arm7
Apr 12 12:10:12 Finished compiler/backend/arm7                                    2s  26MB
Apr 12 12:10:12 Starting compiler/backend/arm8
Apr 12 12:10:14 Finished compiler/backend/arm8                                    2s  29MB
Apr 12 12:10:14 Starting compiler/backend/mips
Apr 12 12:10:17 Finished compiler/backend/mips                                    2s  27MB
Apr 12 12:10:17 Starting compiler/backend/riscv
Apr 12 12:10:19 Finished compiler/backend/riscv                                   2s  24MB
Apr 12 12:10:19 Starting compiler/backend/ag32
Apr 12 12:11:45 Finished compiler/backend/ag32                                 1m25s   1GB
Apr 12 12:11:45 Starting compiler/parsing/proofs
Apr 12 12:11:47 Finished compiler/parsing/proofs                                  1s  19MB
Apr 12 12:11:47 Starting compiler/inference/proofs
Apr 12 12:11:49 Finished compiler/inference/proofs                                1s  19MB
Apr 12 12:11:49 Starting compiler/backend/semantics
Apr 12 12:15:36 Finished compiler/backend/semantics                            3m46s   1GB
Apr 12 12:15:36 Starting compiler/backend/reg_alloc/proofs
Apr 12 12:15:38 Finished compiler/backend/reg_alloc/proofs                        1s  26MB
Apr 12 12:15:38 Starting compiler/backend/proofs
Apr 12 12:16:38 Finished compiler/backend/proofs                               1m00s   3GB
Apr 12 12:16:38 Starting compiler/backend/serialiser
Apr 12 12:16:41 Finished compiler/backend/serialiser                              2s  35MB
Apr 12 12:16:41 Starting compiler/encoders/x64/proofs
Apr 12 12:26:30 Finished compiler/encoders/x64/proofs                          9m48s   6GB
Apr 12 12:26:30 Starting compiler/encoders/arm7/proofs
Apr 12 12:40:28 Finished compiler/encoders/arm7/proofs                        13m58s   4GB
Apr 12 12:40:28 Starting compiler/encoders/arm8/proofs
Apr 12 12:47:26 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Apr 12 12:47:26 Starting compiler/encoders/arm8_asl/proofs
Apr 12 13:39:32 Finished compiler/encoders/arm8_asl/proofs                    52m05s   7GB
Apr 12 13:39:32 Starting compiler/encoders/mips/proofs
Apr 12 13:50:14 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Apr 12 13:50:14 Starting compiler/encoders/riscv/proofs
Apr 12 13:59:07 Finished compiler/encoders/riscv/proofs                        8m53s   1GB
Apr 12 13:59:07 Starting compiler/encoders/ag32/proofs
Apr 12 14:01:40 Finished compiler/encoders/ag32/proofs                         2m33s   1GB
Apr 12 14:01:40 Starting compiler/backend/x64/proofs
Apr 12 14:02:13 Finished compiler/backend/x64/proofs                             32s   2GB
Apr 12 14:02:13 Starting compiler/backend/arm7/proofs
Apr 12 14:02:48 Finished compiler/backend/arm7/proofs                            35s   2GB
Apr 12 14:02:48 Starting compiler/backend/arm8/proofs
Apr 12 14:03:21 Finished compiler/backend/arm8/proofs                            32s   2GB
Apr 12 14:03:21 Starting compiler/backend/arm8_asl
Apr 12 14:03:46 Finished compiler/backend/arm8_asl                               24s   2GB
Apr 12 14:03:46 Starting compiler/backend/mips/proofs
Apr 12 14:04:18 Finished compiler/backend/mips/proofs                            32s   2GB
Apr 12 14:04:18 Starting compiler/backend/riscv/proofs
Apr 12 14:04:58 Finished compiler/backend/riscv/proofs                           39s   1GB
Apr 12 14:04:58 Starting compiler/backend/ag32/proofs
Apr 12 14:19:47 Finished compiler/backend/ag32/proofs                         14m49s   2GB
Apr 12 14:19:47 Starting candle/set-theory
Apr 12 14:20:27 Finished candle/set-theory                                       39s   1GB
Apr 12 14:20:27 Starting candle/syntax-lib
Apr 12 14:20:28 Finished candle/syntax-lib                                        1s  18MB
Apr 12 14:20:29 Starting candle/standard/syntax
Apr 12 14:20:39 Finished candle/standard/syntax                                  10s 726MB
Apr 12 14:20:40 Starting candle/standard/semantics
Apr 12 14:22:39 Finished candle/standard/semantics                             1m59s   1GB
Apr 12 14:22:39 Starting candle/standard/monadic
Apr 12 14:22:41 Finished candle/standard/monadic                                  1s  28MB
Apr 12 14:22:41 Starting candle/standard/ml_kernel
Apr 12 14:24:23 Finished candle/standard/ml_kernel                             1m41s   3GB
Apr 12 14:24:23 Starting candle/overloading/syntax
Apr 12 14:27:45 Finished candle/overloading/syntax                             3m22s   1GB
Apr 12 14:27:46 Starting candle/overloading/semantics
Apr 12 14:40:21 Finished candle/overloading/semantics                         12m35s   2GB
Apr 12 14:40:22 Starting candle/overloading/monadic
Apr 12 14:43:06 Finished candle/overloading/monadic                            2m44s   1GB
Apr 12 14:43:06 Starting candle/overloading/ml_kernel
Apr 12 14:51:04 Finished candle/overloading/ml_kernel                          7m57s   3GB
Apr 12 14:51:04 Starting candle/overloading/ml_checker
Apr 12 14:53:42 Finished candle/overloading/ml_checker                         2m37s   2GB
Apr 12 14:53:42 Starting candle/prover
Apr 12 15:03:47 Finished candle/prover                                        10m04s   3GB
Apr 12 15:03:47 Starting pancake
Apr 12 15:04:34 Finished pancake                                                 46s 972MB
Apr 12 15:04:34 Starting pancake/ffi
Apr 12 15:04:34 Finished pancake/ffi                                              0s  13MB
Apr 12 15:04:34 Starting pancake/semantics
Apr 12 15:07:17 Finished pancake/semantics                                     2m42s   1GB
Apr 12 15:07:17 Starting pancake/parser
Apr 12 15:07:40 Finished pancake/parser                                          23s 638MB
Apr 12 15:07:41 Starting pancake/proofs
Apr 12 15:42:23 Finished pancake/proofs                                       34m42s   4GB
Apr 12 15:42:23 Starting characteristic/examples
Apr 12 15:43:57 Finished characteristic/examples                               1m34s   2GB
Apr 12 15:43:57 Starting tutorial/solutions
Apr 12 15:59:28 Finished tutorial/solutions                                   15m30s   9GB
Apr 12 15:59:28 Starting translator/monadic/examples
Apr 12 16:03:34 Finished translator/monadic/examples                           4m05s   3GB
Apr 12 16:03:34 Starting examples
Apr 12 16:19:31 Finished examples                                             15m56s   4GB
Apr 12 16:19:31 Starting examples/compilation/x64
Apr 12 18:21:26 Finished examples/compilation/x64                           2h01m55s  22GB
Apr 12 18:21:27 Starting examples/compilation/x64/proofs
Apr 12 18:24:04 Finished examples/compilation/x64/proofs                       2m37s   4GB
Apr 12 18:24:04 Starting examples/compilation/ag32
Apr 12 18:55:20 Finished examples/compilation/ag32                            31m16s   9GB
Apr 12 18:55:20 Starting examples/compilation/ag32/proofs
Apr 12 18:56:32 Finished examples/compilation/ag32/proofs                      1m11s   4GB
Apr 12 18:56:32 Starting examples/compilation/to_word
Apr 12 18:59:59 Finished examples/compilation/to_word                          3m27s   6GB
Apr 12 18:59:59 Starting examples/lpr_checker
Apr 12 19:01:05 Finished examples/lpr_checker                                  1m05s   1GB
Apr 12 19:01:05 Starting examples/lpr_checker/array
Apr 12 19:33:17 Finished examples/lpr_checker/array                           32m11s   6GB
Apr 12 19:33:17 Starting examples/lpr_checker/array/compilation
Apr 12 20:29:37 Finished examples/lpr_checker/array/compilation               56m19s  30GB
Apr 12 20:29:37 Starting examples/lpr_checker/array/compilation/proofs
Apr 12 20:31:23 Finished examples/lpr_checker/array/compilation/proofs         1m46s   3GB
Apr 12 20:31:23 Starting examples/lpr_checker/array/compilation/proofsARM8
Apr 12 20:37:27 Finished examples/lpr_checker/array/compilation/proofsARM8     6m03s  20GB
Apr 12 20:37:27 Starting examples/xlrup_checker
Apr 12 20:38:25 Finished examples/xlrup_checker                                  57s   1GB
Apr 12 20:38:25 Starting examples/xlrup_checker/array
Apr 12 20:55:58 Finished examples/xlrup_checker/array                         17m32s   3GB
Apr 12 20:55:58 Starting examples/xlrup_checker/array/compilation
Apr 12 21:17:59 Finished examples/xlrup_checker/array/compilation             22m00s  16GB
Apr 12 21:17:59 Starting examples/xlrup_checker/array/compilation/proofs
Apr 12 21:19:06 Finished examples/xlrup_checker/array/compilation/proofs       1m06s   5GB
Apr 12 21:19:06 Starting examples/pseudo_bool
Apr 12 21:21:03 Finished examples/pseudo_bool                                  1m56s   1GB
Apr 12 21:21:03 Starting examples/pseudo_bool/cnf_encoding
Apr 12 21:21:29 Finished examples/pseudo_bool/cnf_encoding                       25s 739MB
Apr 12 21:21:29 Starting examples/pseudo_bool/graph_encoding
Apr 12 21:22:13 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Apr 12 21:22:13 Starting examples/pseudo_bool/array
Apr 12 22:38:20 Finished examples/pseudo_bool/array                         1h16m06s   8GB
Apr 12 22:38:20 Starting examples/pseudo_bool/array/compilation
Apr 13 06:25:55 Finished examples/pseudo_bool/array/compilation             7h47m35s  63GB
Apr 13 06:25:55 Starting examples/pseudo_bool/array/compilation/proofs
Apr 13 06:28:37 Finished examples/pseudo_bool/array/compilation/proofs         2m41s   6GB
Apr 13 06:28:37 Starting examples/opentheory
Apr 13 06:39:39 Finished examples/opentheory                                  11m02s   3GB
Apr 13 06:39:39 Starting examples/opentheory
Apr 13 06:39:41 Finished examples/opentheory                                      1s  30MB
Apr 13 06:39:41 Starting examples/opentheory/compilation
Apr 13 07:17:09 Finished examples/opentheory/compilation                      37m28s  33GB
Apr 13 07:17:09 Starting examples/opentheory/compilation/proofs
Apr 13 07:18:12 Finished examples/opentheory/compilation/proofs                1m02s   5GB
Apr 13 07:18:12 Starting examples/opentheory/compilation/ag32
Apr 13 07:53:26 Finished examples/opentheory/compilation/ag32                 35m13s  33GB
Apr 13 07:53:26 Starting examples/opentheory/compilation/ag32/proofs
Apr 13 07:55:22 Finished examples/opentheory/compilation/ag32/proofs           1m55s   7GB
Apr 13 07:55:22 Starting examples/sat_encodings
Apr 13 07:57:25 Finished examples/sat_encodings                                2m02s 970MB
Apr 13 07:57:25 Starting examples/sat_encodings/case_studies
Apr 13 07:59:15 Finished examples/sat_encodings/case_studies                   1m50s   1GB
Apr 13 07:59:15 Starting examples/sat_encodings/translation
Apr 13 08:05:31 Finished examples/sat_encodings/translation                    6m15s   4GB
Apr 13 08:05:31 Starting examples/sat_encodings/translation/compilation
Apr 13 08:53:02 Finished examples/sat_encodings/translation/compilation       47m30s  21GB
Apr 13 08:53:02 Starting examples/deflate
Apr 13 08:54:04 Finished examples/deflate                                      1m01s 826MB
Apr 13 08:54:04 Starting examples/deflate/translation
Apr 13 08:55:47 Finished examples/deflate/translation                          1m42s   3GB
Apr 13 08:55:47 Starting examples/deflate/translation/compilation
Apr 13 09:16:12 Finished examples/deflate/translation/compilation             20m24s  12GB
Apr 13 09:16:12 Starting examples/vipr
Apr 13 09:20:25 Finished examples/vipr                                         4m12s   5GB
Apr 13 09:20:25 Starting examples/vipr/compilation
Apr 13 09:42:13 Finished examples/vipr/compilation                            21m47s  18GB
Apr 13 09:42:13 Starting translator/okasaki-examples
Apr 13 09:47:28 Finished translator/okasaki-examples                           5m14s   2GB
Apr 13 09:47:28 Starting translator/other-examples
Apr 13 09:50:45 Finished translator/other-examples                             3m17s   2GB
Apr 13 09:50:45 Starting compiler/parsing/tests
Apr 13 09:51:17 Finished compiler/parsing/tests                                  31s 761MB
Apr 13 09:51:17 Starting compiler/inference/tests
Apr 13 09:59:55 Finished compiler/inference/tests                              8m37s   6GB
Apr 13 09:59:55 Starting compiler/printing/test
Apr 13 10:03:53 Finished compiler/printing/test                                3m58s   3GB
Apr 13 10:03:53 Starting icing/flover
Apr 13 10:47:45 Finished icing/flover                                         43m51s   2GB
Apr 13 10:47:45 Starting icing/
Apr 13 11:42:27 Finished icing/                                               54m41s   7GB
Apr 13 11:42:27 Starting icing/examples
Apr 13 11:44:06 Finished icing/examples                                        1m39s   4GB
Apr 13 11:44:06 Starting compiler/repl
Apr 13 11:52:51 Finished compiler/repl                                         8m44s   5GB
Apr 13 11:52:51 Starting unverified/sexpr-bootstrap/x64/64
Apr 13 12:06:33 Finished unverified/sexpr-bootstrap/x64/64                    13m40s  17GB
Apr 13 12:06:33 Starting unverified/sexpr-bootstrap/x64/32
Apr 13 12:17:39 Finished unverified/sexpr-bootstrap/x64/32                    11m05s  14GB
Apr 13 12:17:39 Starting compiler/benchmarks
Apr 13 12:33:16 Finished compiler/benchmarks                                  15m37s   2GB
Apr 13 12:33:17 Starting compiler/bootstrap/compilation/x64/64
Apr 14 00:55:18 Finished compiler/bootstrap/compilation/x64/64             12h22m01s  64GB
Apr 14 00:55:18 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 14 01:17:07 Finished compiler/bootstrap/compilation/x64/64/proofs         21m48s  21GB
Apr 14 01:17:07 Starting compiler/bootstrap/compilation/x64/32
Apr 14 08:56:47 Finished compiler/bootstrap/compilation/x64/32              7h39m39s  64GB
Apr 14 08:56:47 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 14 09:00:06 Finished compiler/bootstrap/compilation/x64/32/proofs          3m19s  18GB
Apr 14 09:00:06 Starting compiler/bootstrap/compilation/ag32/32
Apr 14 16:23:46 Finished compiler/bootstrap/compilation/ag32/32             7h23m39s  64GB
Apr 14 16:23:46 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 14 16:30:53 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m06s  38GB
Apr 14 16:30:53 SUCCESS