Job 2623

CakeML:96d01162e0f3289ba50ca2f18d1c0298bd547958
  Remove remaining mlDefine usage manually [Sep 28 12:36:20]
#1060 (remove-mldefine)
Merging into:06d5cf707aca7e50703c7e8b43e3a02dc37253e2
  Merge pull request #1058 from CakeML/dafny-ir-update [Sep 28 06:33:16]
HOL:72a01e7935ee7175f22527332d54ac58085668ed
  Add more primitive proof rules [Sep 23 23:08:36]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Sep 29 05:11:14 Claimed job
Sep 29 05:11:16 Reusing HOL
Sep 29 05:12:02 Starting developers
Sep 29 05:12:07 Finished developers                                               5s 141MB
Sep 29 05:12:07 Starting developers/bin
Sep 29 05:12:13 Finished developers/bin                                           6s   1GB
Sep 29 05:12:14 Starting compiler/proofs
Sep 29 07:07:39 Finished compiler/proofs                                    1h55m25s  15GB
Sep 29 07:07:40 Starting compiler/bootstrap/translation
Sep 29 16:03:13 Finished compiler/bootstrap/translation                     8h55m33s  39GB
Sep 29 16:03:13 Starting semantics/ffi
Sep 29 16:03:19 Finished semantics/ffi                                            5s 414MB
Sep 29 16:03:19 Starting semantics
Sep 29 16:03:21 Finished semantics                                                1s  19MB
Sep 29 16:03:21 Starting semantics/proofs
Sep 29 16:03:46 Finished semantics/proofs                                        25s 446MB
Sep 29 16:03:46 Starting semantics/alt_semantics
Sep 29 16:04:12 Finished semantics/alt_semantics                                 25s 563MB
Sep 29 16:04:12 Starting semantics/alt_semantics/proofs
Sep 29 16:15:51 Finished semantics/alt_semantics/proofs                       11m38s   1GB
Sep 29 16:15:51 Starting basis/pure
Sep 29 16:15:52 Finished basis/pure                                               1s  26MB
Sep 29 16:15:52 Starting translator
Sep 29 16:17:33 Finished translator                                            1m39s   2GB
Sep 29 16:17:33 Starting compiler/parsing
Sep 29 16:17:34 Finished compiler/parsing                                         1s  17MB
Sep 29 16:17:34 Starting characteristic
Sep 29 16:17:36 Finished characteristic                                           1s  24MB
Sep 29 16:17:36 Starting translator/monadic
Sep 29 16:17:38 Finished translator/monadic                                       1s  21MB
Sep 29 16:17:38 Starting basis
Sep 29 16:20:13 Finished basis                                                 2m34s   2GB
Sep 29 16:20:13 Starting compiler/inference
Sep 29 16:20:15 Finished compiler/inference                                       1s  21MB
Sep 29 16:20:15 Starting compiler/backend/reg_alloc
Sep 29 16:20:16 Finished compiler/backend/reg_alloc                               1s  21MB
Sep 29 16:20:16 Starting compiler/backend/gc
Sep 29 16:20:19 Finished compiler/backend/gc                                      2s  25MB
Sep 29 16:20:19 Starting compiler/backend
Sep 29 16:20:24 Finished compiler/backend                                         5s 284MB
Sep 29 16:20:24 Starting compiler/encoders/asm
Sep 29 16:20:26 Finished compiler/encoders/asm                                    1s  21MB
Sep 29 16:20:26 Starting compiler/encoders/x64
Sep 29 16:20:28 Finished compiler/encoders/x64                                    1s  22MB
Sep 29 16:20:28 Starting compiler/encoders/arm7
Sep 29 16:20:30 Finished compiler/encoders/arm7                                   1s  20MB
Sep 29 16:20:30 Starting compiler/encoders/arm8
Sep 29 16:20:32 Finished compiler/encoders/arm8                                   1s  23MB
Sep 29 16:20:32 Starting compiler/encoders/arm8_asl
Sep 29 18:50:17 Finished compiler/encoders/arm8_asl                         2h29m44s  31GB
Sep 29 18:50:18 Starting compiler/encoders/mips
Sep 29 18:50:20 Finished compiler/encoders/mips                                   1s  20MB
Sep 29 18:50:20 Starting compiler/encoders/riscv
Sep 29 18:50:22 Finished compiler/encoders/riscv                                  1s  22MB
Sep 29 18:50:22 Starting compiler/encoders/ag32
Sep 29 18:50:24 Finished compiler/encoders/ag32                                   2s  24MB
Sep 29 18:50:24 Starting compiler/backend/x64
Sep 29 18:50:26 Finished compiler/backend/x64                                     2s  24MB
Sep 29 18:50:27 Starting compiler/backend/arm7
Sep 29 18:50:29 Finished compiler/backend/arm7                                    2s  22MB
Sep 29 18:50:29 Starting compiler/backend/arm8
Sep 29 18:50:31 Finished compiler/backend/arm8                                    2s  29MB
Sep 29 18:50:31 Starting compiler/backend/mips
Sep 29 18:50:34 Finished compiler/backend/mips                                    2s  27MB
Sep 29 18:50:34 Starting compiler/backend/riscv
Sep 29 18:50:36 Finished compiler/backend/riscv                                   2s  26MB
Sep 29 18:50:36 Starting compiler/backend/ag32
Sep 29 18:51:48 Finished compiler/backend/ag32                                 1m11s   1GB
Sep 29 18:51:48 Starting compiler/parsing/proofs
Sep 29 18:51:50 Finished compiler/parsing/proofs                                  1s  20MB
Sep 29 18:51:50 Starting compiler/inference/proofs
Sep 29 18:51:52 Finished compiler/inference/proofs                                1s  23MB
Sep 29 18:51:52 Starting compiler/backend/semantics
Sep 29 18:55:16 Finished compiler/backend/semantics                            3m24s   2GB
Sep 29 18:55:16 Starting compiler/backend/reg_alloc/proofs
Sep 29 18:55:18 Finished compiler/backend/reg_alloc/proofs                        1s  25MB
Sep 29 18:55:18 Starting compiler/backend/proofs
Sep 29 18:56:14 Finished compiler/backend/proofs                                 55s   2GB
Sep 29 18:56:14 Starting compiler/backend/serialiser
Sep 29 18:56:16 Finished compiler/backend/serialiser                              2s  29MB
Sep 29 18:56:16 Starting compiler/encoders/x64/proofs
Sep 29 19:06:54 Finished compiler/encoders/x64/proofs                         10m37s   6GB
Sep 29 19:06:54 Starting compiler/encoders/arm7/proofs
Sep 29 19:21:03 Finished compiler/encoders/arm7/proofs                        14m08s   3GB
Sep 29 19:21:03 Starting compiler/encoders/arm8/proofs
Sep 29 19:28:24 Finished compiler/encoders/arm8/proofs                         7m21s   1GB
Sep 29 19:28:25 Starting compiler/encoders/arm8_asl/proofs
Sep 29 20:25:09 Finished compiler/encoders/arm8_asl/proofs                    56m44s   7GB
Sep 29 20:25:09 Starting compiler/encoders/mips/proofs
Sep 29 20:36:05 Finished compiler/encoders/mips/proofs                        10m56s   2GB
Sep 29 20:36:05 Starting compiler/encoders/riscv/proofs
Sep 29 20:44:55 Finished compiler/encoders/riscv/proofs                        8m49s   2GB
Sep 29 20:44:55 Starting compiler/encoders/ag32/proofs
Sep 29 20:48:14 Finished compiler/encoders/ag32/proofs                         3m18s 990MB
Sep 29 20:48:14 Starting compiler/backend/x64/proofs
Sep 29 20:48:46 Finished compiler/backend/x64/proofs                             31s   1GB
Sep 29 20:48:46 Starting compiler/backend/arm7/proofs
Sep 29 20:49:19 Finished compiler/backend/arm7/proofs                            33s   1GB
Sep 29 20:49:19 Starting compiler/backend/arm8/proofs
Sep 29 20:49:52 Finished compiler/backend/arm8/proofs                            32s   1GB
Sep 29 20:49:52 Starting compiler/backend/arm8_asl
Sep 29 20:50:16 Finished compiler/backend/arm8_asl                               24s   1GB
Sep 29 20:50:16 Starting compiler/backend/mips/proofs
Sep 29 20:50:51 Finished compiler/backend/mips/proofs                            34s   1GB
Sep 29 20:50:51 Starting compiler/backend/riscv/proofs
Sep 29 20:51:29 Finished compiler/backend/riscv/proofs                           37s   2GB
Sep 29 20:51:29 Starting compiler/backend/ag32/proofs
Sep 29 21:06:11 Finished compiler/backend/ag32/proofs                         14m42s   3GB
Sep 29 21:06:11 Starting compiler/backend/cv_compute
Sep 29 21:07:30 Finished compiler/backend/cv_compute                           1m18s   2GB
Sep 29 21:07:30 Starting cv_translator
Sep 29 21:28:07 Finished cv_translator                                        20m36s   6GB
Sep 29 21:28:07 Starting candle/set-theory
Sep 29 21:28:44 Finished candle/set-theory                                       37s   1GB
Sep 29 21:28:44 Starting candle/syntax-lib
Sep 29 21:28:46 Finished candle/syntax-lib                                        1s  19MB
Sep 29 21:28:46 Starting candle/standard/syntax
Sep 29 21:28:59 Finished candle/standard/syntax                                  13s 861MB
Sep 29 21:28:59 Starting candle/standard/semantics
Sep 29 21:31:11 Finished candle/standard/semantics                             2m11s   1GB
Sep 29 21:31:12 Starting candle/standard/monadic
Sep 29 21:31:13 Finished candle/standard/monadic                                  1s  21MB
Sep 29 21:31:14 Starting candle/standard/ml_kernel
Sep 29 21:33:00 Finished candle/standard/ml_kernel                             1m46s   3GB
Sep 29 21:33:00 Starting candle/overloading/syntax
Sep 29 21:36:30 Finished candle/overloading/syntax                             3m29s   1GB
Sep 29 21:36:30 Starting candle/overloading/semantics
Sep 29 21:48:52 Finished candle/overloading/semantics                         12m21s   2GB
Sep 29 21:48:52 Starting candle/overloading/monadic
Sep 29 21:51:36 Finished candle/overloading/monadic                            2m44s   2GB
Sep 29 21:51:36 Starting candle/overloading/ml_kernel
Sep 29 21:59:51 Finished candle/overloading/ml_kernel                          8m14s   4GB
Sep 29 21:59:51 Starting candle/overloading/ml_checker
Sep 29 22:02:33 Finished candle/overloading/ml_checker                         2m42s   2GB
Sep 29 22:02:33 Starting candle/prover
Sep 29 22:12:59 Finished candle/prover                                        10m26s   3GB
Sep 29 22:13:00 Starting pancake
Sep 29 22:13:24 Finished pancake                                                 24s 821MB
Sep 29 22:13:24 Starting pancake/ffi
Sep 29 22:13:25 Finished pancake/ffi                                              0s  13MB
Sep 29 22:13:25 Starting pancake/semantics
Sep 29 22:15:51 Finished pancake/semantics                                     2m25s   1GB
Sep 29 22:15:51 Starting pancake/parser
Sep 29 22:16:17 Finished pancake/parser                                          26s 416MB
Sep 29 22:16:17 Starting pancake/proofs
Sep 29 22:34:33 Finished pancake/proofs                                       18m16s   4GB
Sep 29 22:34:34 Starting compiler/dafny
Sep 29 22:37:00 Finished compiler/dafny                                        2m26s   8GB
Sep 29 22:37:00 Starting compiler/dafny/translation
Sep 29 23:07:07 Finished compiler/dafny/translation                           30m06s  17GB
Sep 29 23:07:07 Starting compiler/dafny/compilation
Sep 29 23:10:29 Finished compiler/dafny/compilation                            3m22s  10GB
Sep 29 23:10:29 Starting compiler/dafny/semantics
Sep 29 23:11:07 Finished compiler/dafny/semantics                                37s 827MB
Sep 29 23:11:07 Starting characteristic/examples
Sep 29 23:12:38 Finished characteristic/examples                               1m30s   3GB
Sep 29 23:12:39 Starting tutorial/solutions
Sep 29 23:15:30 Finished tutorial/solutions                                    2m51s   3GB
Sep 29 23:15:30 Starting translator/monadic/examples
Sep 29 23:19:04 Finished translator/monadic/examples                           3m34s   3GB
Sep 29 23:19:04 Starting examples
Sep 29 23:33:33 Finished examples                                             14m28s   2GB
Sep 29 23:33:33 Starting examples/compilation/x64
Sep 29 23:42:40 Finished examples/compilation/x64                              9m06s   5GB
Sep 29 23:42:40 Starting examples/compilation/x64/proofs
Sep 29 23:45:36 Finished examples/compilation/x64/proofs                       2m56s   4GB
Sep 29 23:45:36 Starting examples/compilation/ag32
Sep 29 23:47:52 Finished examples/compilation/ag32                             2m15s   3GB
Sep 29 23:47:52 Starting examples/compilation/ag32/proofs
Sep 29 23:49:01 Finished examples/compilation/ag32/proofs                      1m09s   5GB
Sep 29 23:49:01 Starting examples/compilation/to_word
Sep 29 23:52:36 Finished examples/compilation/to_word                          3m34s   4GB
Sep 29 23:52:36 Starting examples/lpr_checker
Sep 29 23:53:07 Finished examples/lpr_checker                                    31s 842MB
Sep 29 23:53:07 Starting examples/lpr_checker/array
Sep 30 00:21:22 Finished examples/lpr_checker/array                           28m14s   4GB
Sep 30 00:21:22 Starting examples/lpr_checker/array/compilation
Sep 30 00:24:03 Finished examples/lpr_checker/array/compilation                2m41s   8GB
Sep 30 00:24:03 Starting examples/lpr_checker/array/compilation/proofs
Sep 30 00:25:21 Finished examples/lpr_checker/array/compilation/proofs         1m17s   5GB
Sep 30 00:25:21 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 30 00:26:35 Finished examples/lpr_checker/array/compilation/proofsARM8     1m13s   6GB
Sep 30 00:26:35 Starting examples/xlrup_checker
Sep 30 00:27:12 Finished examples/xlrup_checker                                  37s 611MB
Sep 30 00:27:13 Starting examples/xlrup_checker/array
Sep 30 00:41:37 Finished examples/xlrup_checker/array                         14m24s   2GB
Sep 30 00:41:38 Starting examples/xlrup_checker/array/compilation
Sep 30 00:43:03 Finished examples/xlrup_checker/array/compilation              1m24s   4GB
Sep 30 00:43:03 Starting examples/xlrup_checker/array/compilation/proofs
Sep 30 00:44:07 Finished examples/xlrup_checker/array/compilation/proofs       1m04s   4GB
Sep 30 00:44:07 Starting examples/pseudo_bool
Sep 30 00:45:39 Finished examples/pseudo_bool                                  1m31s   1GB
Sep 30 00:45:39 Starting examples/pseudo_bool/cnf_encoding
Sep 30 00:46:09 Finished examples/pseudo_bool/cnf_encoding                       29s 990MB
Sep 30 00:46:09 Starting examples/pseudo_bool/graph_encoding
Sep 30 00:46:56 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Sep 30 00:46:57 Starting examples/pseudo_bool/array
Sep 30 01:52:26 Finished examples/pseudo_bool/array                         1h05m28s   7GB
Sep 30 01:52:26 Starting examples/pseudo_bool/array/compilation
Sep 30 02:07:26 Finished examples/pseudo_bool/array/compilation               14m59s  27GB
Sep 30 02:07:26 Starting examples/pseudo_bool/array/compilation/proofs
Sep 30 02:10:17 Finished examples/pseudo_bool/array/compilation/proofs         2m51s   6GB
Sep 30 02:10:17 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 30 02:11:37 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m19s   7GB
Sep 30 02:11:37 Starting examples/opentheory
Sep 30 02:20:48 Finished examples/opentheory                                   9m11s   3GB
Sep 30 02:20:48 Starting examples/opentheory
Sep 30 02:20:50 Finished examples/opentheory                                      1s  34MB
Sep 30 02:20:50 Starting examples/opentheory/compilation
Sep 30 02:22:55 Finished examples/opentheory/compilation                       2m04s   5GB
Sep 30 02:22:55 Starting examples/opentheory/compilation/proofs
Sep 30 02:24:01 Finished examples/opentheory/compilation/proofs                1m05s   4GB
Sep 30 02:24:01 Starting examples/opentheory/compilation/ag32
Sep 30 02:26:04 Finished examples/opentheory/compilation/ag32                  2m03s   5GB
Sep 30 02:26:04 Starting examples/opentheory/compilation/ag32/proofs
Sep 30 02:27:46 Finished examples/opentheory/compilation/ag32/proofs           1m42s   7GB
Sep 30 02:27:46 Starting examples/sat_encodings
Sep 30 02:28:54 Finished examples/sat_encodings                                1m07s 443MB
Sep 30 02:28:54 Starting examples/sat_encodings/case_studies
Sep 30 02:30:50 Finished examples/sat_encodings/case_studies                   1m55s   1GB
Sep 30 02:30:50 Starting examples/sat_encodings/translation
Sep 30 02:34:54 Finished examples/sat_encodings/translation                    4m03s   1GB
Sep 30 02:34:54 Starting examples/sat_encodings/translation/compilation
Sep 30 02:37:24 Finished examples/sat_encodings/translation/compilation        2m29s   5GB
Sep 30 02:37:24 Starting examples/deflate
Sep 30 02:37:56 Finished examples/deflate                                        31s 506MB
Sep 30 02:37:56 Starting examples/deflate/translation
Sep 30 02:39:06 Finished examples/deflate/translation                          1m10s   1GB
Sep 30 02:39:06 Starting examples/deflate/translation/compilation
Sep 30 02:40:15 Finished examples/deflate/translation/compilation              1m09s   4GB
Sep 30 02:40:15 Starting examples/vipr
Sep 30 02:44:06 Finished examples/vipr                                         3m50s   5GB
Sep 30 02:44:06 Starting examples/vipr/compilation
Sep 30 02:45:23 Finished examples/vipr/compilation                             1m17s   3GB
Sep 30 02:45:23 Starting translator/okasaki-examples
Sep 30 02:49:56 Finished translator/okasaki-examples                           4m33s   1GB
Sep 30 02:49:56 Starting translator/other-examples
Sep 30 02:53:51 Finished translator/other-examples                             3m54s   1GB
Sep 30 02:53:51 Starting compiler/parsing/tests
Sep 30 02:54:28 Finished compiler/parsing/tests                                  36s   1GB
Sep 30 02:54:28 Starting compiler/inference/tests
Sep 30 02:55:02 Finished compiler/inference/tests                                33s   2GB
Sep 30 02:55:02 Starting compiler/printing/test
Sep 30 02:56:37 Finished compiler/printing/test                                1m35s   2GB
Sep 30 02:56:37 Starting icing/flover
Sep 30 03:42:09 Finished icing/flover                                         45m31s   2GB
Sep 30 03:42:09 Starting icing/
Sep 30 04:12:32 Finished icing/                                               30m22s   3GB
Sep 30 04:12:32 Starting icing/examples
Sep 30 04:14:14 Finished icing/examples                                        1m41s   4GB
Sep 30 04:14:14 Starting compiler/repl
Sep 30 04:23:17 Finished compiler/repl                                         9m03s   6GB
Sep 30 04:23:17 Starting unverified/sexpr-bootstrap/x64/64
Sep 30 04:39:49 Finished unverified/sexpr-bootstrap/x64/64                    16m31s  17GB
Sep 30 04:39:49 Starting unverified/sexpr-bootstrap/x64/32
Sep 30 04:52:57 Finished unverified/sexpr-bootstrap/x64/32                    13m07s  15GB
Sep 30 04:52:57 Starting compiler/benchmarks
Sep 30 05:08:34 Finished compiler/benchmarks                                  15m37s   2GB
Sep 30 05:08:34 Starting compiler/bootstrap/compilation/x64/64
Sep 30 05:48:57 Finished compiler/bootstrap/compilation/x64/64                40m22s  63GB
Sep 30 05:48:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 30 06:12:29 Finished compiler/bootstrap/compilation/x64/64/proofs         23m32s  54GB
Sep 30 06:12:30 Starting compiler/bootstrap/compilation/x64/32
Sep 30 06:51:46 Finished compiler/bootstrap/compilation/x64/32                39m16s  64GB
Sep 30 06:51:47 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 30 06:57:54 Finished compiler/bootstrap/compilation/x64/32/proofs          6m07s  19GB
Sep 30 06:57:54 Starting compiler/bootstrap/compilation/arm8/64
Sep 30 07:49:08 Finished compiler/bootstrap/compilation/arm8/64               51m13s  64GB
Sep 30 07:49:08 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 30 07:53:57 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m48s  27GB
Sep 30 07:53:57 Starting compiler/bootstrap/compilation/ag32/32
Sep 30 08:30:18 Finished compiler/bootstrap/compilation/ag32/32               36m20s  63GB
Sep 30 08:30:18 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 30 08:37:04 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m45s  20GB
Sep 30 08:37:04 SUCCESS