Job 2610

CakeML:47620c885bf54aac8598ee831c0c02aa1763d98e
  Merge pull request #1053 from CakeML/dafny [Sep 16 16:47:56]
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 16 17:00:22 Claimed job
Sep 16 17:00:24 Reusing HOL
Sep 16 17:01:09 Starting developers
Sep 16 17:01:14 Finished developers                                               5s 177MB
Sep 16 17:01:15 Starting developers/bin
Sep 16 17:01:21 Finished developers/bin                                           5s   1GB
Sep 16 17:01:21 Starting compiler/proofs
Sep 16 18:59:13 Finished compiler/proofs                                    1h57m51s  15GB
Sep 16 18:59:13 Starting compiler/bootstrap/translation
Sep 17 03:54:53 Finished compiler/bootstrap/translation                     8h55m40s  53GB
Sep 17 03:54:53 Starting semantics/ffi
Sep 17 03:54:59 Finished semantics/ffi                                            5s 410MB
Sep 17 03:54:59 Starting semantics
Sep 17 03:55:01 Finished semantics                                                1s  19MB
Sep 17 03:55:01 Starting semantics/proofs
Sep 17 03:55:26 Finished semantics/proofs                                        25s 445MB
Sep 17 03:55:26 Starting semantics/alt_semantics
Sep 17 03:55:52 Finished semantics/alt_semantics                                 25s 578MB
Sep 17 03:55:52 Starting semantics/alt_semantics/proofs
Sep 17 04:07:30 Finished semantics/alt_semantics/proofs                       11m38s   2GB
Sep 17 04:07:30 Starting basis/pure
Sep 17 04:07:32 Finished basis/pure                                               1s  17MB
Sep 17 04:07:32 Starting translator
Sep 17 04:09:14 Finished translator                                            1m41s   2GB
Sep 17 04:09:14 Starting compiler/parsing
Sep 17 04:09:15 Finished compiler/parsing                                         1s  21MB
Sep 17 04:09:15 Starting characteristic
Sep 17 04:09:17 Finished characteristic                                           1s  21MB
Sep 17 04:09:17 Starting translator/monadic
Sep 17 04:09:19 Finished translator/monadic                                       1s  23MB
Sep 17 04:09:19 Starting basis
Sep 17 04:11:58 Finished basis                                                 2m38s   3GB
Sep 17 04:11:58 Starting compiler/inference
Sep 17 04:12:00 Finished compiler/inference                                       1s  20MB
Sep 17 04:12:00 Starting compiler/backend/reg_alloc
Sep 17 04:12:02 Finished compiler/backend/reg_alloc                               1s  22MB
Sep 17 04:12:02 Starting compiler/backend/gc
Sep 17 04:12:04 Finished compiler/backend/gc                                      2s  29MB
Sep 17 04:12:04 Starting compiler/backend
Sep 17 04:12:10 Finished compiler/backend                                         5s 295MB
Sep 17 04:12:10 Starting compiler/encoders/asm
Sep 17 04:12:12 Finished compiler/encoders/asm                                    1s  21MB
Sep 17 04:12:12 Starting compiler/encoders/x64
Sep 17 04:12:14 Finished compiler/encoders/x64                                    1s  21MB
Sep 17 04:12:14 Starting compiler/encoders/arm7
Sep 17 04:12:16 Finished compiler/encoders/arm7                                   1s  19MB
Sep 17 04:12:16 Starting compiler/encoders/arm8
Sep 17 04:12:18 Finished compiler/encoders/arm8                                   1s  21MB
Sep 17 04:12:18 Starting compiler/encoders/arm8_asl
Sep 17 04:15:24 Finished compiler/encoders/arm8_asl                            3m05s   1GB
Sep 17 04:15:24 Starting compiler/encoders/mips
Sep 17 04:15:26 Finished compiler/encoders/mips                                   1s  25MB
Sep 17 04:15:26 Starting compiler/encoders/riscv
Sep 17 04:15:28 Finished compiler/encoders/riscv                                  1s  20MB
Sep 17 04:15:28 Starting compiler/encoders/ag32
Sep 17 04:15:30 Finished compiler/encoders/ag32                                   1s  21MB
Sep 17 04:15:30 Starting compiler/backend/x64
Sep 17 04:15:32 Finished compiler/backend/x64                                     2s  23MB
Sep 17 04:15:32 Starting compiler/backend/arm7
Sep 17 04:15:35 Finished compiler/backend/arm7                                    2s  28MB
Sep 17 04:15:35 Starting compiler/backend/arm8
Sep 17 04:15:37 Finished compiler/backend/arm8                                    2s  29MB
Sep 17 04:15:37 Starting compiler/backend/mips
Sep 17 04:15:40 Finished compiler/backend/mips                                    2s  27MB
Sep 17 04:15:40 Starting compiler/backend/riscv
Sep 17 04:15:42 Finished compiler/backend/riscv                                   2s  24MB
Sep 17 04:15:42 Starting compiler/backend/ag32
Sep 17 04:17:10 Finished compiler/backend/ag32                                 1m28s   1GB
Sep 17 04:17:10 Starting compiler/parsing/proofs
Sep 17 04:17:12 Finished compiler/parsing/proofs                                  1s  21MB
Sep 17 04:17:12 Starting compiler/inference/proofs
Sep 17 04:17:14 Finished compiler/inference/proofs                                1s  20MB
Sep 17 04:17:14 Starting compiler/backend/semantics
Sep 17 04:20:45 Finished compiler/backend/semantics                            3m31s   1GB
Sep 17 04:20:45 Starting compiler/backend/reg_alloc/proofs
Sep 17 04:20:47 Finished compiler/backend/reg_alloc/proofs                        1s  20MB
Sep 17 04:20:47 Starting compiler/backend/proofs
Sep 17 04:21:42 Finished compiler/backend/proofs                                 54s   2GB
Sep 17 04:21:42 Starting compiler/backend/serialiser
Sep 17 04:21:45 Finished compiler/backend/serialiser                              2s  28MB
Sep 17 04:21:45 Starting compiler/encoders/x64/proofs
Sep 17 04:32:32 Finished compiler/encoders/x64/proofs                         10m47s   4GB
Sep 17 04:32:32 Starting compiler/encoders/arm7/proofs
Sep 17 04:46:43 Finished compiler/encoders/arm7/proofs                        14m10s   3GB
Sep 17 04:46:43 Starting compiler/encoders/arm8/proofs
Sep 17 04:54:10 Finished compiler/encoders/arm8/proofs                         7m27s   1GB
Sep 17 04:54:10 Starting compiler/encoders/arm8_asl/proofs
Sep 17 05:11:57 Finished compiler/encoders/arm8_asl/proofs                    17m46s   2GB
Sep 17 05:11:57 Starting compiler/encoders/mips/proofs
Sep 17 05:22:52 Finished compiler/encoders/mips/proofs                        10m54s   1GB
Sep 17 05:22:52 Starting compiler/encoders/riscv/proofs
Sep 17 05:31:47 Finished compiler/encoders/riscv/proofs                        8m54s   2GB
Sep 17 05:31:47 Starting compiler/encoders/ag32/proofs
Sep 17 05:35:05 Finished compiler/encoders/ag32/proofs                         3m18s   1GB
Sep 17 05:35:05 Starting compiler/backend/x64/proofs
Sep 17 05:35:37 Finished compiler/backend/x64/proofs                             32s   1GB
Sep 17 05:35:37 Starting compiler/backend/arm7/proofs
Sep 17 05:36:11 Finished compiler/backend/arm7/proofs                            33s   1GB
Sep 17 05:36:11 Starting compiler/backend/arm8/proofs
Sep 17 05:36:45 Finished compiler/backend/arm8/proofs                            33s   2GB
Sep 17 05:36:45 Starting compiler/backend/arm8_asl
Sep 17 05:37:10 Finished compiler/backend/arm8_asl                               24s   1GB
Sep 17 05:37:10 Starting compiler/backend/mips/proofs
Sep 17 05:37:45 Finished compiler/backend/mips/proofs                            34s   2GB
Sep 17 05:37:45 Starting compiler/backend/riscv/proofs
Sep 17 05:38:22 Finished compiler/backend/riscv/proofs                           37s   2GB
Sep 17 05:38:22 Starting compiler/backend/ag32/proofs
Sep 17 05:53:13 Finished compiler/backend/ag32/proofs                         14m51s   2GB
Sep 17 05:53:13 Starting compiler/backend/cv_compute
Sep 17 05:54:33 Finished compiler/backend/cv_compute                           1m19s   2GB
Sep 17 05:54:33 Starting cv_translator
Sep 17 06:15:36 Finished cv_translator                                        21m03s   7GB
Sep 17 06:15:37 Starting candle/set-theory
Sep 17 06:16:20 Finished candle/set-theory                                       43s   1GB
Sep 17 06:16:20 Starting candle/syntax-lib
Sep 17 06:16:22 Finished candle/syntax-lib                                        1s  21MB
Sep 17 06:16:22 Starting candle/standard/syntax
Sep 17 06:16:35 Finished candle/standard/syntax                                  13s 868MB
Sep 17 06:16:35 Starting candle/standard/semantics
Sep 17 06:18:48 Finished candle/standard/semantics                             2m13s   1GB
Sep 17 06:18:49 Starting candle/standard/monadic
Sep 17 06:18:50 Finished candle/standard/monadic                                  1s  21MB
Sep 17 06:18:51 Starting candle/standard/ml_kernel
Sep 17 06:20:46 Finished candle/standard/ml_kernel                             1m55s   3GB
Sep 17 06:20:46 Starting candle/overloading/syntax
Sep 17 06:24:21 Finished candle/overloading/syntax                             3m34s   1GB
Sep 17 06:24:21 Starting candle/overloading/semantics
Sep 17 06:36:49 Finished candle/overloading/semantics                         12m28s   2GB
Sep 17 06:36:49 Starting candle/overloading/monadic
Sep 17 06:39:34 Finished candle/overloading/monadic                            2m44s   1GB
Sep 17 06:39:34 Starting candle/overloading/ml_kernel
Sep 17 06:47:52 Finished candle/overloading/ml_kernel                          8m17s   4GB
Sep 17 06:47:52 Starting candle/overloading/ml_checker
Sep 17 06:50:34 Finished candle/overloading/ml_checker                         2m42s   2GB
Sep 17 06:50:34 Starting candle/prover
Sep 17 07:01:01 Finished candle/prover                                        10m26s   3GB
Sep 17 07:01:02 Starting pancake
Sep 17 07:01:26 Finished pancake                                                 24s 793MB
Sep 17 07:01:26 Starting pancake/ffi
Sep 17 07:01:27 Finished pancake/ffi                                              0s  13MB
Sep 17 07:01:27 Starting pancake/semantics
Sep 17 07:03:51 Finished pancake/semantics                                     2m24s   1GB
Sep 17 07:03:51 Starting pancake/parser
Sep 17 07:04:15 Finished pancake/parser                                          24s 502MB
Sep 17 07:04:15 Starting pancake/proofs
Sep 17 07:22:37 Finished pancake/proofs                                       18m22s   3GB
Sep 17 07:22:37 Starting compiler/dafny
Sep 17 07:25:02 Finished compiler/dafny                                        2m24s   8GB
Sep 17 07:25:02 Starting compiler/dafny/translation
Sep 17 07:54:41 Finished compiler/dafny/translation                           29m38s  16GB
Sep 17 07:54:41 Starting compiler/dafny/compilation
Sep 17 07:58:04 Finished compiler/dafny/compilation                            3m23s  10GB
Sep 17 07:58:04 Starting compiler/dafny/semantics
Sep 17 07:58:43 Finished compiler/dafny/semantics                                38s 973MB
Sep 17 07:58:43 Starting characteristic/examples
Sep 17 08:00:15 Finished characteristic/examples                               1m31s   2GB
Sep 17 08:00:15 Starting tutorial/solutions
Sep 17 08:03:06 Finished tutorial/solutions                                    2m51s   5GB
Sep 17 08:03:06 Starting translator/monadic/examples
Sep 17 08:06:58 Finished translator/monadic/examples                           3m51s   2GB
Sep 17 08:06:58 Starting examples
Sep 17 08:21:44 Finished examples                                             14m45s   2GB
Sep 17 08:21:44 Starting examples/compilation/x64
Sep 17 08:30:48 Finished examples/compilation/x64                              9m03s   5GB
Sep 17 08:30:48 Starting examples/compilation/x64/proofs
Sep 17 08:33:48 Finished examples/compilation/x64/proofs                       3m00s   5GB
Sep 17 08:33:48 Starting examples/compilation/ag32
Sep 17 08:36:02 Finished examples/compilation/ag32                             2m14s   2GB
Sep 17 08:36:03 Starting examples/compilation/ag32/proofs
Sep 17 08:37:12 Finished examples/compilation/ag32/proofs                      1m09s   5GB
Sep 17 08:37:12 Starting examples/compilation/to_word
Sep 17 08:40:43 Finished examples/compilation/to_word                          3m30s   8GB
Sep 17 08:40:43 Starting examples/lpr_checker
Sep 17 08:41:23 Finished examples/lpr_checker                                    39s 638MB
Sep 17 08:41:23 Starting examples/lpr_checker/array
Sep 17 09:09:34 Finished examples/lpr_checker/array                           28m11s   5GB
Sep 17 09:09:34 Starting examples/lpr_checker/array/compilation
Sep 17 09:12:15 Finished examples/lpr_checker/array/compilation                2m40s   7GB
Sep 17 09:12:15 Starting examples/lpr_checker/array/compilation/proofs
Sep 17 09:13:33 Finished examples/lpr_checker/array/compilation/proofs         1m18s   6GB
Sep 17 09:13:34 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 17 09:14:55 Finished examples/lpr_checker/array/compilation/proofsARM8     1m21s   7GB
Sep 17 09:14:55 Starting examples/xlrup_checker
Sep 17 09:15:33 Finished examples/xlrup_checker                                  37s 849MB
Sep 17 09:15:33 Starting examples/xlrup_checker/array
Sep 17 09:30:05 Finished examples/xlrup_checker/array                         14m32s   2GB
Sep 17 09:30:05 Starting examples/xlrup_checker/array/compilation
Sep 17 09:31:31 Finished examples/xlrup_checker/array/compilation              1m26s   4GB
Sep 17 09:31:31 Starting examples/xlrup_checker/array/compilation/proofs
Sep 17 09:32:42 Finished examples/xlrup_checker/array/compilation/proofs       1m10s   5GB
Sep 17 09:32:42 Starting examples/pseudo_bool
Sep 17 09:34:12 Finished examples/pseudo_bool                                  1m30s   1GB
Sep 17 09:34:12 Starting examples/pseudo_bool/cnf_encoding
Sep 17 09:34:43 Finished examples/pseudo_bool/cnf_encoding                       30s 761MB
Sep 17 09:34:43 Starting examples/pseudo_bool/graph_encoding
Sep 17 09:35:30 Finished examples/pseudo_bool/graph_encoding                     47s 997MB
Sep 17 09:35:30 Starting examples/pseudo_bool/array
Sep 17 10:41:15 Finished examples/pseudo_bool/array                         1h05m44s   6GB
Sep 17 10:41:15 Starting examples/pseudo_bool/array/compilation
Sep 17 10:55:58 Finished examples/pseudo_bool/array/compilation               14m42s  27GB
Sep 17 10:55:58 Starting examples/pseudo_bool/array/compilation/proofs
Sep 17 10:58:57 Finished examples/pseudo_bool/array/compilation/proofs         2m59s   7GB
Sep 17 10:58:57 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 17 11:00:18 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m20s   6GB
Sep 17 11:00:18 Starting examples/opentheory
Sep 17 11:09:32 Finished examples/opentheory                                   9m14s   2GB
Sep 17 11:09:32 Starting examples/opentheory
Sep 17 11:09:34 Finished examples/opentheory                                      1s  32MB
Sep 17 11:09:34 Starting examples/opentheory/compilation
Sep 17 11:11:36 Finished examples/opentheory/compilation                       2m01s   5GB
Sep 17 11:11:36 Starting examples/opentheory/compilation/proofs
Sep 17 11:12:42 Finished examples/opentheory/compilation/proofs                1m05s   4GB
Sep 17 11:12:42 Starting examples/opentheory/compilation/ag32
Sep 17 11:14:46 Finished examples/opentheory/compilation/ag32                  2m03s   5GB
Sep 17 11:14:46 Starting examples/opentheory/compilation/ag32/proofs
Sep 17 11:16:29 Finished examples/opentheory/compilation/ag32/proofs           1m42s   6GB
Sep 17 11:16:29 Starting examples/sat_encodings
Sep 17 11:17:37 Finished examples/sat_encodings                                1m07s 444MB
Sep 17 11:17:37 Starting examples/sat_encodings/case_studies
Sep 17 11:19:31 Finished examples/sat_encodings/case_studies                   1m54s   1GB
Sep 17 11:19:31 Starting examples/sat_encodings/translation
Sep 17 11:23:35 Finished examples/sat_encodings/translation                    4m03s   1GB
Sep 17 11:23:35 Starting examples/sat_encodings/translation/compilation
Sep 17 11:26:02 Finished examples/sat_encodings/translation/compilation        2m27s   5GB
Sep 17 11:26:02 Starting examples/deflate
Sep 17 11:26:34 Finished examples/deflate                                        31s 497MB
Sep 17 11:26:34 Starting examples/deflate/translation
Sep 17 11:27:43 Finished examples/deflate/translation                          1m08s   1GB
Sep 17 11:27:43 Starting examples/deflate/translation/compilation
Sep 17 11:28:53 Finished examples/deflate/translation/compilation              1m10s   4GB
Sep 17 11:28:53 Starting examples/vipr
Sep 17 11:32:50 Finished examples/vipr                                         3m57s   5GB
Sep 17 11:32:50 Starting examples/vipr/compilation
Sep 17 11:34:05 Finished examples/vipr/compilation                             1m14s   4GB
Sep 17 11:34:05 Starting translator/okasaki-examples
Sep 17 11:38:53 Finished translator/okasaki-examples                           4m47s   1GB
Sep 17 11:38:53 Starting translator/other-examples
Sep 17 11:39:55 Finished translator/other-examples                             1m02s   2GB
Sep 17 11:39:55 Starting compiler/parsing/tests
Sep 17 11:40:35 Finished compiler/parsing/tests                                  39s   1GB
Sep 17 11:40:35 Starting compiler/inference/tests
Sep 17 11:41:07 Finished compiler/inference/tests                                32s   2GB
Sep 17 11:41:08 Starting compiler/printing/test
Sep 17 11:42:40 Finished compiler/printing/test                                1m32s   2GB
Sep 17 11:42:40 Starting icing/flover
Sep 17 12:28:26 Finished icing/flover                                         45m46s   2GB
Sep 17 12:28:26 Starting icing/
Sep 17 12:58:37 Finished icing/                                               30m10s   6GB
Sep 17 12:58:37 Starting icing/examples
Sep 17 13:00:13 Finished icing/examples                                        1m36s   3GB
Sep 17 13:00:13 Starting compiler/repl
Sep 17 13:09:04 Finished compiler/repl                                         8m50s   6GB
Sep 17 13:09:04 Starting unverified/sexpr-bootstrap/x64/64
Sep 17 13:25:25 Finished unverified/sexpr-bootstrap/x64/64                    16m20s  18GB
Sep 17 13:25:25 Starting unverified/sexpr-bootstrap/x64/32
Sep 17 13:38:19 Finished unverified/sexpr-bootstrap/x64/32                    12m53s  16GB
Sep 17 13:38:19 Starting compiler/benchmarks
Sep 17 13:54:17 Finished compiler/benchmarks                                  15m57s   2GB
Sep 17 13:54:18 Starting compiler/bootstrap/compilation/x64/64
Sep 17 14:31:40 Finished compiler/bootstrap/compilation/x64/64                37m22s  63GB
Sep 17 14:31:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 17 14:55:05 Finished compiler/bootstrap/compilation/x64/64/proofs         23m24s  42GB
Sep 17 14:55:05 Starting compiler/bootstrap/compilation/x64/32
Sep 17 15:34:05 Finished compiler/bootstrap/compilation/x64/32                38m59s  64GB
Sep 17 15:34:05 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 17 15:40:12 Finished compiler/bootstrap/compilation/x64/32/proofs          6m07s  19GB
Sep 17 15:40:12 Starting compiler/bootstrap/compilation/arm8/64
Sep 17 16:33:19 Finished compiler/bootstrap/compilation/arm8/64               53m06s  64GB
Sep 17 16:33:19 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 17 16:40:52 Finished compiler/bootstrap/compilation/arm8/64/proofs         7m33s  23GB
Sep 17 16:40:52 Starting compiler/bootstrap/compilation/ag32/32
Sep 17 17:19:46 Finished compiler/bootstrap/compilation/ag32/32               38m53s  64GB
Sep 17 17:19:46 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 17 17:26:27 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m40s  19GB
Sep 17 17:26:27 SUCCESS