Job 2599

CakeML:7b614da7b56c9d04e55ecc20f0c22bdd8d7866e7
  Fix a broken proof [Sep 11 11:01:55]
HOL:7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361
  Fix bug in reduceLib.NOT_CONV [Sep 09 04:53:02]
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-arm8-64.tar.gz
cake-x64-32.tar.gz

Sep 11 11:13:52 Claimed job
Sep 11 11:13:56 Reusing HOL
Sep 11 11:14:41 Starting developers
Sep 11 11:14:47 Finished developers                                               5s 108MB
Sep 11 11:14:47 Starting developers/bin
Sep 11 11:14:53 Finished developers/bin                                           5s   1GB
Sep 11 11:14:53 Starting compiler/proofs
Sep 11 13:12:59 Finished compiler/proofs                                    1h58m05s  16GB
Sep 11 13:12:59 Starting compiler/bootstrap/translation
Sep 11 22:05:39 Finished compiler/bootstrap/translation                     8h52m40s  51GB
Sep 11 22:05:39 Starting semantics/ffi
Sep 11 22:05:45 Finished semantics/ffi                                            5s 410MB
Sep 11 22:05:45 Starting semantics
Sep 11 22:05:47 Finished semantics                                                1s  19MB
Sep 11 22:05:47 Starting semantics/proofs
Sep 11 22:06:12 Finished semantics/proofs                                        25s 436MB
Sep 11 22:06:13 Starting semantics/alt_semantics
Sep 11 22:06:38 Finished semantics/alt_semantics                                 25s 578MB
Sep 11 22:06:39 Starting semantics/alt_semantics/proofs
Sep 11 22:18:08 Finished semantics/alt_semantics/proofs                       11m29s   1GB
Sep 11 22:18:08 Starting basis/pure
Sep 11 22:18:10 Finished basis/pure                                               1s  18MB
Sep 11 22:18:10 Starting translator
Sep 11 22:19:53 Finished translator                                            1m42s   1GB
Sep 11 22:19:53 Starting compiler/parsing
Sep 11 22:19:55 Finished compiler/parsing                                         1s  20MB
Sep 11 22:19:55 Starting characteristic
Sep 11 22:19:57 Finished characteristic                                           1s  22MB
Sep 11 22:19:57 Starting translator/monadic
Sep 11 22:19:59 Finished translator/monadic                                       1s  21MB
Sep 11 22:19:59 Starting basis
Sep 11 22:22:35 Finished basis                                                 2m36s   2GB
Sep 11 22:22:35 Starting compiler/inference
Sep 11 22:22:37 Finished compiler/inference                                       1s  20MB
Sep 11 22:22:37 Starting compiler/backend/reg_alloc
Sep 11 22:22:39 Finished compiler/backend/reg_alloc                               1s  18MB
Sep 11 22:22:39 Starting compiler/backend/gc
Sep 11 22:22:41 Finished compiler/backend/gc                                      2s  28MB
Sep 11 22:22:41 Starting compiler/backend
Sep 11 22:22:47 Finished compiler/backend                                         5s 295MB
Sep 11 22:22:47 Starting compiler/encoders/asm
Sep 11 22:22:49 Finished compiler/encoders/asm                                    1s  27MB
Sep 11 22:22:49 Starting compiler/encoders/x64
Sep 11 22:22:51 Finished compiler/encoders/x64                                    1s  23MB
Sep 11 22:22:51 Starting compiler/encoders/arm7
Sep 11 22:22:53 Finished compiler/encoders/arm7                                   1s  26MB
Sep 11 22:22:53 Starting compiler/encoders/arm8
Sep 11 22:22:55 Finished compiler/encoders/arm8                                   1s  25MB
Sep 11 22:22:55 Starting compiler/encoders/arm8_asl
Sep 11 22:26:00 Finished compiler/encoders/arm8_asl                            3m05s   1GB
Sep 11 22:26:00 Starting compiler/encoders/mips
Sep 11 22:26:02 Finished compiler/encoders/mips                                   1s  20MB
Sep 11 22:26:02 Starting compiler/encoders/riscv
Sep 11 22:26:04 Finished compiler/encoders/riscv                                  1s  24MB
Sep 11 22:26:04 Starting compiler/encoders/ag32
Sep 11 22:26:06 Finished compiler/encoders/ag32                                   1s  26MB
Sep 11 22:26:06 Starting compiler/backend/x64
Sep 11 22:26:09 Finished compiler/backend/x64                                     2s  33MB
Sep 11 22:26:09 Starting compiler/backend/arm7
Sep 11 22:26:11 Finished compiler/backend/arm7                                    2s  25MB
Sep 11 22:26:11 Starting compiler/backend/arm8
Sep 11 22:26:14 Finished compiler/backend/arm8                                    2s  23MB
Sep 11 22:26:14 Starting compiler/backend/mips
Sep 11 22:26:16 Finished compiler/backend/mips                                    2s  26MB
Sep 11 22:26:16 Starting compiler/backend/riscv
Sep 11 22:26:18 Finished compiler/backend/riscv                                   2s  27MB
Sep 11 22:26:18 Starting compiler/backend/ag32
Sep 11 22:27:47 Finished compiler/backend/ag32                                 1m29s   1GB
Sep 11 22:27:48 Starting compiler/parsing/proofs
Sep 11 22:27:49 Finished compiler/parsing/proofs                                  1s  19MB
Sep 11 22:27:49 Starting compiler/inference/proofs
Sep 11 22:27:51 Finished compiler/inference/proofs                                1s  21MB
Sep 11 22:27:51 Starting compiler/backend/semantics
Sep 11 22:31:20 Finished compiler/backend/semantics                            3m28s   1GB
Sep 11 22:31:20 Starting compiler/backend/reg_alloc/proofs
Sep 11 22:31:22 Finished compiler/backend/reg_alloc/proofs                        1s  26MB
Sep 11 22:31:22 Starting compiler/backend/proofs
Sep 11 22:32:14 Finished compiler/backend/proofs                                 52s   2GB
Sep 11 22:32:14 Starting compiler/backend/serialiser
Sep 11 22:32:16 Finished compiler/backend/serialiser                              2s  23MB
Sep 11 22:32:16 Starting compiler/encoders/x64/proofs
Sep 11 22:42:56 Finished compiler/encoders/x64/proofs                         10m39s   5GB
Sep 11 22:42:56 Starting compiler/encoders/arm7/proofs
Sep 11 22:57:05 Finished compiler/encoders/arm7/proofs                        14m09s   3GB
Sep 11 22:57:05 Starting compiler/encoders/arm8/proofs
Sep 11 23:04:26 Finished compiler/encoders/arm8/proofs                         7m20s   1GB
Sep 11 23:04:26 Starting compiler/encoders/arm8_asl/proofs
Sep 11 23:22:02 Finished compiler/encoders/arm8_asl/proofs                    17m35s   2GB
Sep 11 23:22:02 Starting compiler/encoders/mips/proofs
Sep 11 23:32:45 Finished compiler/encoders/mips/proofs                        10m42s   3GB
Sep 11 23:32:45 Starting compiler/encoders/riscv/proofs
Sep 11 23:41:53 Finished compiler/encoders/riscv/proofs                        9m08s   1GB
Sep 11 23:41:53 Starting compiler/encoders/ag32/proofs
Sep 11 23:45:10 Finished compiler/encoders/ag32/proofs                         3m17s   1GB
Sep 11 23:45:10 Starting compiler/backend/x64/proofs
Sep 11 23:45:42 Finished compiler/backend/x64/proofs                             31s   1GB
Sep 11 23:45:42 Starting compiler/backend/arm7/proofs
Sep 11 23:46:16 Finished compiler/backend/arm7/proofs                            33s   1GB
Sep 11 23:46:16 Starting compiler/backend/arm8/proofs
Sep 11 23:46:50 Finished compiler/backend/arm8/proofs                            34s   2GB
Sep 11 23:46:50 Starting compiler/backend/arm8_asl
Sep 11 23:47:15 Finished compiler/backend/arm8_asl                               24s   1GB
Sep 11 23:47:15 Starting compiler/backend/mips/proofs
Sep 11 23:47:48 Finished compiler/backend/mips/proofs                            33s   1GB
Sep 11 23:47:49 Starting compiler/backend/riscv/proofs
Sep 11 23:48:26 Finished compiler/backend/riscv/proofs                           37s   2GB
Sep 11 23:48:26 Starting compiler/backend/ag32/proofs
Sep 12 00:03:19 Finished compiler/backend/ag32/proofs                         14m53s   3GB
Sep 12 00:03:19 Starting compiler/backend/cv_compute
Sep 12 00:04:37 Finished compiler/backend/cv_compute                           1m17s   2GB
Sep 12 00:04:37 Starting cv_translator
Sep 12 00:25:39 Finished cv_translator                                        21m01s   7GB
Sep 12 00:25:39 Starting candle/set-theory
Sep 12 00:26:24 Finished candle/set-theory                                       44s   1GB
Sep 12 00:26:24 Starting candle/syntax-lib
Sep 12 00:26:25 Finished candle/syntax-lib                                        1s  20MB
Sep 12 00:26:26 Starting candle/standard/syntax
Sep 12 00:26:38 Finished candle/standard/syntax                                  12s 918MB
Sep 12 00:26:38 Starting candle/standard/semantics
Sep 12 00:28:52 Finished candle/standard/semantics                             2m13s   1GB
Sep 12 00:28:52 Starting candle/standard/monadic
Sep 12 00:28:54 Finished candle/standard/monadic                                  1s  22MB
Sep 12 00:28:54 Starting candle/standard/ml_kernel
Sep 12 00:30:38 Finished candle/standard/ml_kernel                             1m43s   2GB
Sep 12 00:30:38 Starting candle/overloading/syntax
Sep 12 00:34:15 Finished candle/overloading/syntax                             3m36s   1GB
Sep 12 00:34:15 Starting candle/overloading/semantics
Sep 12 00:46:44 Finished candle/overloading/semantics                         12m29s   3GB
Sep 12 00:46:44 Starting candle/overloading/monadic
Sep 12 00:49:28 Finished candle/overloading/monadic                            2m43s   2GB
Sep 12 00:49:28 Starting candle/overloading/ml_kernel
Sep 12 00:57:48 Finished candle/overloading/ml_kernel                          8m20s   4GB
Sep 12 00:57:48 Starting candle/overloading/ml_checker
Sep 12 01:00:29 Finished candle/overloading/ml_checker                         2m40s   3GB
Sep 12 01:00:29 Starting candle/prover
Sep 12 01:10:49 Finished candle/prover                                        10m20s   4GB
Sep 12 01:10:49 Starting pancake
Sep 12 01:11:13 Finished pancake                                                 23s 701MB
Sep 12 01:11:13 Starting pancake/ffi
Sep 12 01:11:13 Finished pancake/ffi                                              0s  13MB
Sep 12 01:11:13 Starting pancake/semantics
Sep 12 01:13:39 Finished pancake/semantics                                     2m25s   1GB
Sep 12 01:13:39 Starting pancake/parser
Sep 12 01:14:04 Finished pancake/parser                                          24s 503MB
Sep 12 01:14:04 Starting pancake/proofs
Sep 12 01:32:23 Finished pancake/proofs                                       18m18s   5GB
Sep 12 01:32:23 Starting characteristic/examples
Sep 12 01:33:53 Finished characteristic/examples                               1m30s   3GB
Sep 12 01:33:53 Starting tutorial/solutions
Sep 12 01:36:48 Finished tutorial/solutions                                    2m54s   3GB
Sep 12 01:36:48 Starting translator/monadic/examples
Sep 12 01:40:38 Finished translator/monadic/examples                           3m50s   2GB
Sep 12 01:40:38 Starting examples
Sep 12 01:55:33 Finished examples                                             14m54s   3GB
Sep 12 01:55:33 Starting examples/compilation/x64
Sep 12 02:04:37 Finished examples/compilation/x64                              9m04s   5GB
Sep 12 02:04:37 Starting examples/compilation/x64/proofs
Sep 12 02:07:34 Finished examples/compilation/x64/proofs                       2m56s   4GB
Sep 12 02:07:34 Starting examples/compilation/ag32
Sep 12 02:09:49 Finished examples/compilation/ag32                             2m15s   3GB
Sep 12 02:09:49 Starting examples/compilation/ag32/proofs
Sep 12 02:10:59 Finished examples/compilation/ag32/proofs                      1m09s   5GB
Sep 12 02:10:59 Starting examples/compilation/to_word
Sep 12 02:14:33 Finished examples/compilation/to_word                          3m34s   7GB
Sep 12 02:14:34 Starting examples/lpr_checker
Sep 12 02:15:14 Finished examples/lpr_checker                                    40s 639MB
Sep 12 02:15:14 Starting examples/lpr_checker/array
Sep 12 08:27:31 Resuming examples/lpr_checker/array
Sep 12 08:54:22 Finished examples/lpr_checker/array                           26m51s   4GB
Sep 12 08:54:22 Starting examples/lpr_checker/array/compilation
Sep 12 08:57:07 Finished examples/lpr_checker/array/compilation                2m45s   7GB
Sep 12 08:57:07 Starting examples/lpr_checker/array/compilation/proofs
Sep 12 08:58:26 Finished examples/lpr_checker/array/compilation/proofs         1m18s   6GB
Sep 12 08:58:26 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 12 08:59:42 Finished examples/lpr_checker/array/compilation/proofsARM8     1m15s   6GB
Sep 12 08:59:42 Starting examples/xlrup_checker
Sep 12 09:00:21 Finished examples/xlrup_checker                                  38s   1GB
Sep 12 09:00:21 Starting examples/xlrup_checker/array
Sep 12 09:14:56 Finished examples/xlrup_checker/array                         14m35s   3GB
Sep 12 09:14:56 Starting examples/xlrup_checker/array/compilation
Sep 12 09:16:20 Finished examples/xlrup_checker/array/compilation              1m23s   4GB
Sep 12 09:16:20 Starting examples/xlrup_checker/array/compilation/proofs
Sep 12 09:17:26 Finished examples/xlrup_checker/array/compilation/proofs       1m05s   5GB
Sep 12 09:17:26 Starting examples/pseudo_bool
Sep 12 09:18:57 Finished examples/pseudo_bool                                  1m31s 959MB
Sep 12 09:18:57 Starting examples/pseudo_bool/cnf_encoding
Sep 12 09:19:27 Finished examples/pseudo_bool/cnf_encoding                       30s 761MB
Sep 12 09:19:27 Starting examples/pseudo_bool/graph_encoding
Sep 12 09:20:14 Finished examples/pseudo_bool/graph_encoding                     46s   1GB
Sep 12 09:20:14 Starting examples/pseudo_bool/array
Sep 12 10:26:37 Finished examples/pseudo_bool/array                         1h06m23s   6GB
Sep 12 10:26:37 Starting examples/pseudo_bool/array/compilation
Sep 12 10:41:01 Finished examples/pseudo_bool/array/compilation               14m24s  25GB
Sep 12 10:41:02 Starting examples/pseudo_bool/array/compilation/proofs
Sep 12 10:44:01 Finished examples/pseudo_bool/array/compilation/proofs         2m59s   7GB
Sep 12 10:44:02 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 12 10:45:21 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m19s   7GB
Sep 12 10:45:21 Starting examples/opentheory
Sep 12 10:54:37 Finished examples/opentheory                                   9m15s   2GB
Sep 12 10:54:37 Starting examples/opentheory
Sep 12 10:54:39 Finished examples/opentheory                                      1s  30MB
Sep 12 10:54:39 Starting examples/opentheory/compilation
Sep 12 10:56:45 Finished examples/opentheory/compilation                       2m05s   7GB
Sep 12 10:56:45 Starting examples/opentheory/compilation/proofs
Sep 12 10:57:51 Finished examples/opentheory/compilation/proofs                1m06s   5GB
Sep 12 10:57:51 Starting examples/opentheory/compilation/ag32
Sep 12 10:59:54 Finished examples/opentheory/compilation/ag32                  2m03s   5GB
Sep 12 10:59:54 Starting examples/opentheory/compilation/ag32/proofs
Sep 12 11:01:36 Finished examples/opentheory/compilation/ag32/proofs           1m42s   6GB
Sep 12 11:01:36 Starting examples/sat_encodings
Sep 12 11:02:44 Finished examples/sat_encodings                                1m07s 636MB
Sep 12 11:02:44 Starting examples/sat_encodings/case_studies
Sep 12 11:04:37 Finished examples/sat_encodings/case_studies                   1m53s   1GB
Sep 12 11:04:38 Starting examples/sat_encodings/translation
Sep 12 11:08:40 Finished examples/sat_encodings/translation                    4m02s   1GB
Sep 12 11:08:40 Starting examples/sat_encodings/translation/compilation
Sep 12 11:11:09 Finished examples/sat_encodings/translation/compilation        2m28s   5GB
Sep 12 11:11:09 Starting examples/deflate
Sep 12 11:11:41 Finished examples/deflate                                        31s 478MB
Sep 12 11:11:41 Starting examples/deflate/translation
Sep 12 11:12:51 Finished examples/deflate/translation                          1m10s   1GB
Sep 12 11:12:51 Starting examples/deflate/translation/compilation
Sep 12 11:14:00 Finished examples/deflate/translation/compilation              1m08s   3GB
Sep 12 11:14:00 Starting examples/vipr
Sep 12 11:17:56 Finished examples/vipr                                         3m55s   5GB
Sep 12 11:17:56 Starting examples/vipr/compilation
Sep 12 11:19:12 Finished examples/vipr/compilation                             1m15s   4GB
Sep 12 11:19:12 Starting translator/okasaki-examples
Sep 12 11:23:52 Finished translator/okasaki-examples                           4m40s   2GB
Sep 12 11:23:53 Starting translator/other-examples
Sep 12 11:27:44 Finished translator/other-examples                             3m51s   1GB
Sep 12 11:27:44 Starting compiler/parsing/tests
Sep 12 11:28:20 Finished compiler/parsing/tests                                  36s   1GB
Sep 12 11:28:20 Starting compiler/inference/tests
Sep 12 11:28:53 Finished compiler/inference/tests                                33s   2GB
Sep 12 11:28:54 Starting compiler/printing/test
Sep 12 11:30:26 Finished compiler/printing/test                                1m32s   2GB
Sep 12 11:30:26 Starting icing/flover
Sep 12 12:16:32 Finished icing/flover                                         46m05s   2GB
Sep 12 12:16:32 Starting icing/
Sep 12 12:45:52 Finished icing/                                               29m19s   3GB
Sep 12 12:45:52 Starting icing/examples
Sep 12 12:47:33 Finished icing/examples                                        1m40s   4GB
Sep 12 12:47:33 Starting compiler/repl
Sep 12 12:56:31 Finished compiler/repl                                         8m58s   5GB
Sep 12 12:56:31 Starting unverified/sexpr-bootstrap/x64/64
Sep 12 13:12:56 Finished unverified/sexpr-bootstrap/x64/64                    16m24s  19GB
Sep 12 13:12:56 Starting unverified/sexpr-bootstrap/x64/32
Sep 12 13:25:48 Finished unverified/sexpr-bootstrap/x64/32                    12m51s  14GB
Sep 12 13:25:48 Starting compiler/benchmarks
Sep 12 13:41:27 Finished compiler/benchmarks                                  15m38s   2GB
Sep 12 13:41:27 Starting compiler/bootstrap/compilation/x64/64
Sep 12 14:22:19 Finished compiler/bootstrap/compilation/x64/64                40m51s  63GB
Sep 12 14:22:19 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 12 14:45:38 Finished compiler/bootstrap/compilation/x64/64/proofs         23m19s  34GB
Sep 12 14:45:39 Starting compiler/bootstrap/compilation/x64/32
Sep 12 15:24:56 Finished compiler/bootstrap/compilation/x64/32                39m17s  63GB
Sep 12 15:24:56 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 12 15:31:01 Finished compiler/bootstrap/compilation/x64/32/proofs          6m04s  18GB
Sep 12 15:31:01 Starting compiler/bootstrap/compilation/arm8/64
Sep 12 16:29:51 Finished compiler/bootstrap/compilation/arm8/64               58m49s  64GB
Sep 12 16:29:51 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 12 16:34:43 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m52s  28GB
Sep 12 16:34:43 Starting compiler/bootstrap/compilation/ag32/32
Sep 12 17:14:22 Finished compiler/bootstrap/compilation/ag32/32               39m38s  64GB
Sep 12 17:14:22 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 12 17:21:35 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m13s  18GB
Sep 12 17:21:35 SUCCESS