Job 2618

CakeML:6f4b58f756c7f6f298c463aab1f5009b798c00ca
  Update to account for changed Dafny IR [Sep 26 17:56:43]
#1058 (dafny-ir-update)
Merging into:49f0d44be26ff907ef52240f3818a4c3caa10598
  Merge pull request #1055 from CakeML/pan_news [Sep 18 13:05:16]
HOL:72a01e7935ee7175f22527332d54ac58085668ed
  Add more primitive proof rules [Sep 23 23:08:36]
Machine:pavlova

Sep 26 20:41:24 Claimed job
Sep 26 20:41:31 Reusing HOL
Sep 26 20:41:43 Starting developers
Sep 26 20:41:47 Finished developers                                               2s 200MB
Sep 26 20:41:48 Starting developers/bin
Sep 26 20:42:09 Finished developers/bin                                          20s   1GB
Sep 26 20:42:10 Starting compiler/proofs
Sep 26 22:27:13 Finished compiler/proofs                                    1h45m02s  45GB
Sep 26 22:27:14 Starting compiler/bootstrap/translation
Sep 27 07:27:29 Finished compiler/bootstrap/translation                     9h00m13s  94GB
Sep 27 07:27:30 Starting semantics/ffi
Sep 27 07:27:39 Finished semantics/ffi                                            8s 635MB
Sep 27 07:27:40 Starting semantics
Sep 27 07:27:41 Finished semantics                                                0s  64MB
Sep 27 07:27:42 Starting semantics/proofs
Sep 27 07:28:07 Finished semantics/proofs                                        23s 771MB
Sep 27 07:28:08 Starting semantics/alt_semantics
Sep 27 07:28:35 Finished semantics/alt_semantics                                 26s 663MB
Sep 27 07:28:36 Starting semantics/alt_semantics/proofs
Sep 27 07:39:06 Finished semantics/alt_semantics/proofs                       10m29s   2GB
Sep 27 07:39:07 Starting basis/pure
Sep 27 07:39:09 Finished basis/pure                                               0s  70MB
Sep 27 07:39:10 Starting translator
Sep 27 07:40:48 Finished translator                                            1m37s   4GB
Sep 27 07:40:49 Starting compiler/parsing
Sep 27 07:40:50 Finished compiler/parsing                                         0s  72MB
Sep 27 07:40:51 Starting characteristic
Sep 27 07:40:53 Finished characteristic                                           0s  90MB
Sep 27 07:40:54 Starting translator/monadic
Sep 27 07:40:56 Finished translator/monadic                                       0s  99MB
Sep 27 07:40:57 Starting basis
Sep 27 07:43:22 Finished basis                                                 2m24s   3GB
Sep 27 07:43:23 Starting compiler/inference
Sep 27 07:43:24 Finished compiler/inference                                       0s  99MB
Sep 27 07:43:25 Starting compiler/backend/reg_alloc
Sep 27 07:43:27 Finished compiler/backend/reg_alloc                               0s  67MB
Sep 27 07:43:28 Starting compiler/backend/gc
Sep 27 07:43:30 Finished compiler/backend/gc                                      1s 141MB
Sep 27 07:43:31 Starting compiler/backend
Sep 27 07:43:36 Finished compiler/backend                                         4s 342MB
Sep 27 07:43:37 Starting compiler/encoders/asm
Sep 27 07:43:39 Finished compiler/encoders/asm                                    0s  89MB
Sep 27 07:43:39 Starting compiler/encoders/x64
Sep 27 07:43:41 Finished compiler/encoders/x64                                    0s  99MB
Sep 27 07:43:42 Starting compiler/encoders/arm7
Sep 27 07:43:44 Finished compiler/encoders/arm7                                   0s 103MB
Sep 27 07:43:45 Starting compiler/encoders/arm8
Sep 27 07:43:46 Finished compiler/encoders/arm8                                   0s  98MB
Sep 27 07:43:47 Starting compiler/encoders/arm8_asl
Sep 27 07:45:58 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Sep 27 07:45:59 Starting compiler/encoders/mips
Sep 27 07:46:01 Finished compiler/encoders/mips                                   0s  94MB
Sep 27 07:46:01 Starting compiler/encoders/riscv
Sep 27 07:46:03 Finished compiler/encoders/riscv                                  0s  99MB
Sep 27 07:46:04 Starting compiler/encoders/ag32
Sep 27 07:46:06 Finished compiler/encoders/ag32                                   0s  91MB
Sep 27 07:46:07 Starting compiler/backend/x64
Sep 27 07:46:09 Finished compiler/backend/x64                                     1s 140MB
Sep 27 07:46:10 Starting compiler/backend/arm7
Sep 27 07:46:12 Finished compiler/backend/arm7                                    1s 139MB
Sep 27 07:46:12 Starting compiler/backend/arm8
Sep 27 07:46:15 Finished compiler/backend/arm8                                    1s 139MB
Sep 27 07:46:15 Starting compiler/backend/mips
Sep 27 07:46:17 Finished compiler/backend/mips                                    1s 139MB
Sep 27 07:46:18 Starting compiler/backend/riscv
Sep 27 07:46:20 Finished compiler/backend/riscv                                   1s 139MB
Sep 27 07:46:21 Starting compiler/backend/ag32
Sep 27 07:47:48 Finished compiler/backend/ag32                                 1m25s   3GB
Sep 27 07:47:49 Starting compiler/parsing/proofs
Sep 27 07:47:50 Finished compiler/parsing/proofs                                  0s  72MB
Sep 27 07:47:51 Starting compiler/inference/proofs
Sep 27 07:47:53 Finished compiler/inference/proofs                                0s  92MB
Sep 27 07:47:54 Starting compiler/backend/semantics
Sep 27 07:51:09 Finished compiler/backend/semantics                            3m14s   3GB
Sep 27 07:51:10 Starting compiler/backend/reg_alloc/proofs
Sep 27 07:51:12 Finished compiler/backend/reg_alloc/proofs                        0s  96MB
Sep 27 07:51:13 Starting compiler/backend/proofs
Sep 27 07:52:07 Finished compiler/backend/proofs                                 53s   3GB
Sep 27 07:52:08 Starting compiler/backend/serialiser
Sep 27 07:52:10 Finished compiler/backend/serialiser                              1s 140MB
Sep 27 07:52:11 Starting compiler/encoders/x64/proofs
Sep 27 08:02:31 Finished compiler/encoders/x64/proofs                         10m18s   5GB
Sep 27 08:02:32 Starting compiler/encoders/arm7/proofs
Sep 27 08:15:35 Finished compiler/encoders/arm7/proofs                        13m01s   9GB
Sep 27 08:15:36 Starting compiler/encoders/arm8/proofs
Sep 27 08:22:30 Finished compiler/encoders/arm8/proofs                         6m52s   5GB
Sep 27 08:22:30 Starting compiler/encoders/arm8_asl/proofs
Sep 27 08:37:59 Finished compiler/encoders/arm8_asl/proofs                    15m27s   4GB
Sep 27 08:38:00 Starting compiler/encoders/mips/proofs
Sep 27 08:48:09 Finished compiler/encoders/mips/proofs                        10m08s  10GB
Sep 27 08:48:10 Starting compiler/encoders/riscv/proofs
Sep 27 08:56:38 Finished compiler/encoders/riscv/proofs                        8m26s   4GB
Sep 27 08:56:39 Starting compiler/encoders/ag32/proofs
Sep 27 08:59:36 Finished compiler/encoders/ag32/proofs                         2m56s   3GB
Sep 27 08:59:37 Starting compiler/backend/x64/proofs
Sep 27 09:00:24 Finished compiler/backend/x64/proofs                             46s   3GB
Sep 27 09:00:25 Starting compiler/backend/arm7/proofs
Sep 27 09:01:13 Finished compiler/backend/arm7/proofs                            46s   3GB
Sep 27 09:01:14 Starting compiler/backend/arm8/proofs
Sep 27 09:01:59 Finished compiler/backend/arm8/proofs                            44s   3GB
Sep 27 09:02:00 Starting compiler/backend/arm8_asl
Sep 27 09:02:31 Finished compiler/backend/arm8_asl                               29s   2GB
Sep 27 09:02:32 Starting compiler/backend/mips/proofs
Sep 27 09:03:22 Finished compiler/backend/mips/proofs                            49s   3GB
Sep 27 09:03:23 Starting compiler/backend/riscv/proofs
Sep 27 09:04:20 Finished compiler/backend/riscv/proofs                           56s   4GB
Sep 27 09:04:21 Starting compiler/backend/ag32/proofs
Sep 27 09:18:49 Finished compiler/backend/ag32/proofs                         14m26s   6GB
Sep 27 09:18:50 Starting compiler/backend/cv_compute
Sep 27 09:20:44 Finished compiler/backend/cv_compute                           1m52s   3GB
Sep 27 09:20:45 Starting cv_translator
Sep 27 09:40:35 Finished cv_translator                                        19m48s  14GB
Sep 27 09:40:35 Starting candle/set-theory
Sep 27 09:41:29 Finished candle/set-theory                                       52s   2GB
Sep 27 09:41:29 Starting candle/syntax-lib
Sep 27 09:41:31 Finished candle/syntax-lib                                        0s  73MB
Sep 27 09:41:32 Starting candle/standard/syntax
Sep 27 09:41:52 Finished candle/standard/syntax                                  18s   1GB
Sep 27 09:41:52 Starting candle/standard/semantics
Sep 27 09:44:40 Finished candle/standard/semantics                             2m46s   2GB
Sep 27 09:44:41 Starting candle/standard/monadic
Sep 27 09:44:43 Finished candle/standard/monadic                                  0s 102MB
Sep 27 09:44:44 Starting candle/standard/ml_kernel
Sep 27 09:46:52 Finished candle/standard/ml_kernel                             2m07s   5GB
Sep 27 09:46:53 Starting candle/overloading/syntax
Sep 27 09:50:36 Finished candle/overloading/syntax                             3m42s   2GB
Sep 27 09:50:37 Starting candle/overloading/semantics
Sep 27 10:02:23 Finished candle/overloading/semantics                         11m44s   5GB
Sep 27 10:02:24 Starting candle/overloading/monadic
Sep 27 10:05:04 Finished candle/overloading/monadic                            2m38s   3GB
Sep 27 10:05:05 Starting candle/overloading/ml_kernel
Sep 27 10:13:04 Finished candle/overloading/ml_kernel                          7m57s   6GB
Sep 27 10:13:05 Starting candle/overloading/ml_checker
Sep 27 10:15:50 Finished candle/overloading/ml_checker                         2m44s   7GB
Sep 27 10:15:51 Starting candle/prover
Sep 27 10:26:28 Finished candle/prover                                        10m36s   5GB
Sep 27 10:26:29 Starting pancake
Sep 27 10:26:56 Finished pancake                                                 26s 994MB
Sep 27 10:26:57 Starting pancake/ffi
Sep 27 10:26:58 Finished pancake/ffi                                              0s  22MB
Sep 27 10:26:59 Starting pancake/semantics
Sep 27 10:29:11 Finished pancake/semantics                                     2m10s   3GB
Sep 27 10:29:12 Starting pancake/parser
Sep 27 10:29:35 Finished pancake/parser                                          22s 792MB
Sep 27 10:29:36 Starting pancake/proofs
Sep 27 10:45:35 Finished pancake/proofs                                       15m56s   7GB
Sep 27 10:45:35 Starting compiler/dafny
Sep 27 10:48:15 Finished compiler/dafny                                        2m38s  11GB
Sep 27 10:48:15 Starting compiler/dafny/translation
Sep 27 11:16:53 Finished compiler/dafny/translation                           28m36s  13GB
Sep 27 11:16:54 Starting compiler/dafny/compilation
Sep 27 11:20:35 Finished compiler/dafny/compilation                            3m39s  14GB
Sep 27 11:20:35 Starting compiler/dafny/semantics
Sep 27 11:21:13 Finished compiler/dafny/semantics                                36s   1GB
Sep 27 11:21:14 Starting characteristic/examples
Sep 27 11:22:46 Finished characteristic/examples                               1m31s   5GB
Sep 27 11:22:47 Starting tutorial/solutions
Sep 27 11:25:37 Finished tutorial/solutions                                    2m49s   5GB
Sep 27 11:25:37 Starting translator/monadic/examples
Sep 27 11:28:55 Finished translator/monadic/examples                           3m16s   4GB
Sep 27 11:28:56 Starting examples
Sep 27 11:41:20 Finished examples                                             12m23s   4GB
Sep 27 11:41:21 Starting examples/compilation/x64
Sep 27 11:51:15 Finished examples/compilation/x64                              9m52s   7GB
Sep 27 11:51:16 Starting examples/compilation/x64/proofs
Sep 27 11:56:24 Finished examples/compilation/x64/proofs                       5m07s   8GB
Sep 27 11:56:25 Starting examples/compilation/ag32
Sep 27 11:59:13 Finished examples/compilation/ag32                             2m47s   5GB
Sep 27 11:59:14 Starting examples/compilation/ag32/proofs
Sep 27 12:01:14 Finished examples/compilation/ag32/proofs                      1m58s   8GB
Sep 27 12:01:15 Starting examples/compilation/to_word
Sep 27 12:05:31 Finished examples/compilation/to_word                          4m14s  13GB
Sep 27 12:05:32 Starting examples/lpr_checker
Sep 27 12:06:11 Finished examples/lpr_checker                                    38s   1GB
Sep 27 12:06:12 Starting examples/lpr_checker/array
Sep 27 12:32:40 Finished examples/lpr_checker/array                           26m27s  22GB
Sep 27 12:32:41 Starting examples/lpr_checker/array/compilation
Sep 27 12:35:23 Finished examples/lpr_checker/array/compilation                2m41s  10GB
Sep 27 12:35:24 Starting examples/lpr_checker/array/compilation/proofs
Sep 27 12:37:25 Finished examples/lpr_checker/array/compilation/proofs         1m59s   8GB
Sep 27 12:37:26 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 27 12:39:25 Finished examples/lpr_checker/array/compilation/proofsARM8     1m58s   8GB
Sep 27 12:39:26 Starting examples/xlrup_checker
Sep 27 12:40:02 Finished examples/xlrup_checker                                  35s   1GB
Sep 27 12:40:03 Starting examples/xlrup_checker/array
Sep 27 12:53:15 Finished examples/xlrup_checker/array                         13m10s  10GB
Sep 27 12:53:16 Starting examples/xlrup_checker/array/compilation
Sep 27 12:54:43 Finished examples/xlrup_checker/array/compilation              1m26s   6GB
Sep 27 12:54:44 Starting examples/xlrup_checker/array/compilation/proofs
Sep 27 12:56:35 Finished examples/xlrup_checker/array/compilation/proofs       1m49s   7GB
Sep 27 12:56:36 Starting examples/pseudo_bool
Sep 27 12:58:02 Finished examples/pseudo_bool                                  1m25s   2GB
Sep 27 12:58:03 Starting examples/pseudo_bool/cnf_encoding
Sep 27 12:58:45 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Sep 27 12:58:46 Starting examples/pseudo_bool/graph_encoding
Sep 27 12:59:44 Finished examples/pseudo_bool/graph_encoding                     57s   2GB
Sep 27 12:59:45 Starting examples/pseudo_bool/array
Sep 27 14:03:31 Finished examples/pseudo_bool/array                         1h03m45s  38GB
Sep 27 14:03:32 Starting examples/pseudo_bool/array/compilation
Sep 27 14:17:29 Finished examples/pseudo_bool/array/compilation               13m56s  30GB
Sep 27 14:17:30 Starting examples/pseudo_bool/array/compilation/proofs
Sep 27 14:21:46 Finished examples/pseudo_bool/array/compilation/proofs         4m15s  10GB
Sep 27 14:21:47 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 27 14:23:45 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m57s   9GB
Sep 27 14:23:46 Starting examples/opentheory
Sep 27 14:32:34 Finished examples/opentheory                                   8m47s   6GB
Sep 27 14:32:35 Starting examples/opentheory
Sep 27 14:32:37 Finished examples/opentheory                                      1s 134MB
Sep 27 14:32:38 Starting examples/opentheory/compilation
Sep 27 14:34:46 Finished examples/opentheory/compilation                       2m06s   9GB
Sep 27 14:34:47 Starting examples/opentheory/compilation/proofs
Sep 27 14:36:41 Finished examples/opentheory/compilation/proofs                1m52s   7GB
Sep 27 14:36:42 Starting examples/opentheory/compilation/ag32
Sep 27 14:38:55 Finished examples/opentheory/compilation/ag32                  2m12s   9GB
Sep 27 14:38:56 Starting examples/opentheory/compilation/ag32/proofs
Sep 27 14:41:32 Finished examples/opentheory/compilation/ag32/proofs           2m35s  12GB
Sep 27 14:41:33 Starting examples/sat_encodings
Sep 27 14:42:36 Finished examples/sat_encodings                                1m02s 894MB
Sep 27 14:42:37 Starting examples/sat_encodings/case_studies
Sep 27 14:44:53 Finished examples/sat_encodings/case_studies                   2m15s   2GB
Sep 27 14:44:53 Starting examples/sat_encodings/translation
Sep 27 14:48:35 Finished examples/sat_encodings/translation                    3m40s   3GB
Sep 27 14:48:36 Starting examples/sat_encodings/translation/compilation
Sep 27 14:51:09 Finished examples/sat_encodings/translation/compilation        2m31s   7GB
Sep 27 14:51:09 Starting examples/deflate
Sep 27 14:51:38 Finished examples/deflate                                        27s 757MB
Sep 27 14:51:38 Starting examples/deflate/translation
Sep 27 14:52:39 Finished examples/deflate/translation                          1m00s   2GB
Sep 27 14:52:40 Starting examples/deflate/translation/compilation
Sep 27 14:53:49 Finished examples/deflate/translation/compilation              1m08s   6GB
Sep 27 14:53:50 Starting examples/vipr
Sep 27 14:57:29 Finished examples/vipr                                         3m37s   4GB
Sep 27 14:57:30 Starting examples/vipr/compilation
Sep 27 14:58:50 Finished examples/vipr/compilation                             1m18s   6GB
Sep 27 14:58:51 Starting translator/okasaki-examples
Sep 27 15:03:12 Finished translator/okasaki-examples                           4m20s   3GB
Sep 27 15:03:13 Starting translator/other-examples
Sep 27 15:08:15 Finished translator/other-examples                             5m01s   3GB
Sep 27 15:08:16 Starting compiler/parsing/tests
Sep 27 15:08:55 Finished compiler/parsing/tests                                  37s   2GB
Sep 27 15:08:56 Starting compiler/inference/tests
Sep 27 15:09:43 Finished compiler/inference/tests                                46s   3GB
Sep 27 15:09:44 Starting compiler/printing/test
Sep 27 15:11:27 Finished compiler/printing/test                                1m41s   6GB
Sep 27 15:11:27 Starting icing/flover
Sep 27 15:48:17 Finished icing/flover                                         36m48s   4GB
Sep 27 15:48:18 Starting icing/
Sep 27 16:16:19 Finished icing/                                               28m00s  10GB
Sep 27 16:16:20 Starting icing/examples
Sep 27 16:18:11 Finished icing/examples                                        1m50s   9GB
Sep 27 16:18:12 Starting compiler/repl
Sep 27 16:27:30 Finished compiler/repl                                         9m17s  10GB
Sep 27 16:27:31 Starting unverified/sexpr-bootstrap/x64/64
Sep 27 16:41:30 Finished unverified/sexpr-bootstrap/x64/64                    13m57s  18GB
Sep 27 16:41:31 Starting unverified/sexpr-bootstrap/x64/32
Sep 27 16:52:51 Finished unverified/sexpr-bootstrap/x64/32                    11m19s  14GB
Sep 27 16:52:52 Starting compiler/benchmarks
Sep 27 16:53:38 Finished compiler/benchmarks                                     44s 712MB
Sep 27 16:53:39 Starting compiler/bootstrap/compilation/x64/64
Sep 27 17:38:31 Finished compiler/bootstrap/compilation/x64/64                44m51s 125GB
Sep 27 17:38:32 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 27 18:03:46 Finished compiler/bootstrap/compilation/x64/64/proofs         25m13s  47GB
Sep 27 18:03:47 Starting compiler/bootstrap/compilation/x64/32
Sep 27 18:47:01 Finished compiler/bootstrap/compilation/x64/32                43m12s 110GB
Sep 27 18:47:02 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 27 18:52:11 Finished compiler/bootstrap/compilation/x64/32/proofs          5m08s  26GB
Sep 27 18:52:12 Starting compiler/bootstrap/compilation/arm8/64
Sep 27 19:50:13 Finished compiler/bootstrap/compilation/arm8/64               57m59s 120GB
Sep 27 19:50:14 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 27 19:55:55 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m40s  29GB
Sep 27 19:55:56 Starting compiler/bootstrap/compilation/ag32/32
Sep 27 20:38:38 Finished compiler/bootstrap/compilation/ag32/32               42m40s 100GB
Sep 27 20:38:39 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 27 20:44:27 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m47s  32GB
Sep 27 20:44:28 SUCCESS