Job 2621

CakeML:a980371eee72aa50eeb232cacffa98b277ead4d7
  Remove problematic use of new Quote syntax [Sep 28 07:06:33]
#1056 (new-quotes)
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:pavlova

Sep 28 07:25:08 Claimed job
Sep 28 07:25:15 Reusing HOL
Sep 28 07:25:27 Starting developers
Sep 28 07:25:31 Finished developers                                               3s 208MB
Sep 28 07:25:32 Starting developers/bin
Sep 28 07:25:52 Finished developers/bin                                          18s   1GB
Sep 28 07:25:53 Starting compiler/proofs
Sep 28 09:09:53 Finished compiler/proofs                                    1h43m58s  36GB
Sep 28 09:09:54 Starting compiler/bootstrap/translation
Sep 28 18:01:31 Finished compiler/bootstrap/translation                     8h51m36s  59GB
Sep 28 18:01:32 Starting semantics/ffi
Sep 28 18:01:41 Finished semantics/ffi                                            8s 634MB
Sep 28 18:01:42 Starting semantics
Sep 28 18:01:44 Finished semantics                                                0s  62MB
Sep 28 18:01:45 Starting semantics/proofs
Sep 28 18:02:09 Finished semantics/proofs                                        23s   1GB
Sep 28 18:02:10 Starting semantics/alt_semantics
Sep 28 18:02:37 Finished semantics/alt_semantics                                 26s 776MB
Sep 28 18:02:38 Starting semantics/alt_semantics/proofs
Sep 28 18:12:49 Finished semantics/alt_semantics/proofs                       10m09s   3GB
Sep 28 18:12:49 Starting basis/pure
Sep 28 18:12:51 Finished basis/pure                                               0s  69MB
Sep 28 18:12:52 Starting translator
Sep 28 18:14:34 Finished translator                                            1m41s   3GB
Sep 28 18:14:35 Starting compiler/parsing
Sep 28 18:14:36 Finished compiler/parsing                                         0s  72MB
Sep 28 18:14:37 Starting characteristic
Sep 28 18:14:39 Finished characteristic                                           0s  90MB
Sep 28 18:14:40 Starting translator/monadic
Sep 28 18:14:42 Finished translator/monadic                                       0s 101MB
Sep 28 18:14:42 Starting basis
Sep 28 18:17:11 Finished basis                                                 2m28s   5GB
Sep 28 18:17:12 Starting compiler/inference
Sep 28 18:17:14 Finished compiler/inference                                       0s  93MB
Sep 28 18:17:15 Starting compiler/backend/reg_alloc
Sep 28 18:17:16 Finished compiler/backend/reg_alloc                               0s  65MB
Sep 28 18:17:17 Starting compiler/backend/gc
Sep 28 18:17:19 Finished compiler/backend/gc                                      1s 140MB
Sep 28 18:17:20 Starting compiler/backend
Sep 28 18:17:26 Finished compiler/backend                                         4s 363MB
Sep 28 18:17:26 Starting compiler/encoders/asm
Sep 28 18:17:28 Finished compiler/encoders/asm                                    0s  89MB
Sep 28 18:17:29 Starting compiler/encoders/x64
Sep 28 18:17:31 Finished compiler/encoders/x64                                    0s  98MB
Sep 28 18:17:32 Starting compiler/encoders/arm7
Sep 28 18:17:33 Finished compiler/encoders/arm7                                   0s 103MB
Sep 28 18:17:34 Starting compiler/encoders/arm8
Sep 28 18:17:36 Finished compiler/encoders/arm8                                   0s  99MB
Sep 28 18:17:37 Starting compiler/encoders/arm8_asl
Sep 28 18:19:48 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Sep 28 18:19:49 Starting compiler/encoders/mips
Sep 28 18:19:51 Finished compiler/encoders/mips                                   0s  94MB
Sep 28 18:19:52 Starting compiler/encoders/riscv
Sep 28 18:19:53 Finished compiler/encoders/riscv                                  0s  98MB
Sep 28 18:19:54 Starting compiler/encoders/ag32
Sep 28 18:19:56 Finished compiler/encoders/ag32                                   0s  90MB
Sep 28 18:19:57 Starting compiler/backend/x64
Sep 28 18:19:59 Finished compiler/backend/x64                                     1s 137MB
Sep 28 18:20:00 Starting compiler/backend/arm7
Sep 28 18:20:02 Finished compiler/backend/arm7                                    1s 137MB
Sep 28 18:20:03 Starting compiler/backend/arm8
Sep 28 18:20:05 Finished compiler/backend/arm8                                    1s 137MB
Sep 28 18:20:06 Starting compiler/backend/mips
Sep 28 18:20:08 Finished compiler/backend/mips                                    1s 137MB
Sep 28 18:20:08 Starting compiler/backend/riscv
Sep 28 18:20:11 Finished compiler/backend/riscv                                   1s 137MB
Sep 28 18:20:11 Starting compiler/backend/ag32
Sep 28 18:21:26 Finished compiler/backend/ag32                                 1m13s   3GB
Sep 28 18:21:27 Starting compiler/parsing/proofs
Sep 28 18:21:29 Finished compiler/parsing/proofs                                  0s  71MB
Sep 28 18:21:30 Starting compiler/inference/proofs
Sep 28 18:21:31 Finished compiler/inference/proofs                                0s  99MB
Sep 28 18:21:32 Starting compiler/backend/semantics
Sep 28 18:24:56 Finished compiler/backend/semantics                            3m22s   3GB
Sep 28 18:24:57 Starting compiler/backend/reg_alloc/proofs
Sep 28 18:24:59 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Sep 28 18:25:00 Starting compiler/backend/proofs
Sep 28 18:25:55 Finished compiler/backend/proofs                                 54s   3GB
Sep 28 18:25:56 Starting compiler/backend/serialiser
Sep 28 18:25:58 Finished compiler/backend/serialiser                              1s 148MB
Sep 28 18:25:59 Starting compiler/encoders/x64/proofs
Sep 28 18:36:15 Finished compiler/encoders/x64/proofs                         10m14s   5GB
Sep 28 18:36:16 Starting compiler/encoders/arm7/proofs
Sep 28 18:49:20 Finished compiler/encoders/arm7/proofs                        13m03s   9GB
Sep 28 18:49:21 Starting compiler/encoders/arm8/proofs
Sep 28 18:56:22 Finished compiler/encoders/arm8/proofs                         7m00s   5GB
Sep 28 18:56:23 Starting compiler/encoders/arm8_asl/proofs
Sep 28 19:11:39 Finished compiler/encoders/arm8_asl/proofs                    15m14s   4GB
Sep 28 19:11:40 Starting compiler/encoders/mips/proofs
Sep 28 19:22:06 Finished compiler/encoders/mips/proofs                        10m24s   6GB
Sep 28 19:22:07 Starting compiler/encoders/riscv/proofs
Sep 28 19:30:50 Finished compiler/encoders/riscv/proofs                        8m41s   3GB
Sep 28 19:30:51 Starting compiler/encoders/ag32/proofs
Sep 28 19:33:48 Finished compiler/encoders/ag32/proofs                         2m56s   2GB
Sep 28 19:33:49 Starting compiler/backend/x64/proofs
Sep 28 19:34:36 Finished compiler/backend/x64/proofs                             46s   3GB
Sep 28 19:34:37 Starting compiler/backend/arm7/proofs
Sep 28 19:35:25 Finished compiler/backend/arm7/proofs                            46s   2GB
Sep 28 19:35:26 Starting compiler/backend/arm8/proofs
Sep 28 19:36:14 Finished compiler/backend/arm8/proofs                            47s   3GB
Sep 28 19:36:14 Starting compiler/backend/arm8_asl
Sep 28 19:36:48 Finished compiler/backend/arm8_asl                               32s   2GB
Sep 28 19:36:49 Starting compiler/backend/mips/proofs
Sep 28 19:37:40 Finished compiler/backend/mips/proofs                            50s   3GB
Sep 28 19:37:41 Starting compiler/backend/riscv/proofs
Sep 28 19:38:38 Finished compiler/backend/riscv/proofs                           56s   4GB
Sep 28 19:38:39 Starting compiler/backend/ag32/proofs
Sep 28 19:53:00 Finished compiler/backend/ag32/proofs                         14m20s   6GB
Sep 28 19:53:01 Starting compiler/backend/cv_compute
Sep 28 19:54:56 Finished compiler/backend/cv_compute                           1m53s   3GB
Sep 28 19:54:57 Starting cv_translator
Sep 28 20:14:57 Finished cv_translator                                        19m59s  10GB
Sep 28 20:14:58 Starting candle/set-theory
Sep 28 20:15:47 Finished candle/set-theory                                       48s   1GB
Sep 28 20:15:48 Starting candle/syntax-lib
Sep 28 20:15:49 Finished candle/syntax-lib                                        0s  72MB
Sep 28 20:15:50 Starting candle/standard/syntax
Sep 28 20:16:10 Finished candle/standard/syntax                                  18s   1GB
Sep 28 20:16:11 Starting candle/standard/semantics
Sep 28 20:18:55 Finished candle/standard/semantics                             2m43s   2GB
Sep 28 20:18:56 Starting candle/standard/monadic
Sep 28 20:18:57 Finished candle/standard/monadic                                  0s 108MB
Sep 28 20:18:58 Starting candle/standard/ml_kernel
Sep 28 20:21:06 Finished candle/standard/ml_kernel                             2m07s   5GB
Sep 28 20:21:07 Starting candle/overloading/syntax
Sep 28 20:24:47 Finished candle/overloading/syntax                             3m39s   2GB
Sep 28 20:24:48 Starting candle/overloading/semantics
Sep 28 20:36:31 Finished candle/overloading/semantics                         11m41s   8GB
Sep 28 20:36:32 Starting candle/overloading/monadic
Sep 28 20:39:10 Finished candle/overloading/monadic                            2m36s   2GB
Sep 28 20:39:11 Starting candle/overloading/ml_kernel
Sep 28 20:47:23 Finished candle/overloading/ml_kernel                          8m11s   7GB
Sep 28 20:47:24 Starting candle/overloading/ml_checker
Sep 28 20:50:11 Finished candle/overloading/ml_checker                         2m45s   7GB
Sep 28 20:50:12 Starting candle/prover
Sep 28 21:00:54 Finished candle/prover                                        10m41s   5GB
Sep 28 21:00:55 Starting pancake
Sep 28 21:01:22 Finished pancake                                                 26s 993MB
Sep 28 21:01:23 Starting pancake/ffi
Sep 28 21:01:24 Finished pancake/ffi                                              0s  22MB
Sep 28 21:01:25 Starting pancake/semantics
Sep 28 21:03:36 Finished pancake/semantics                                     2m10s   2GB
Sep 28 21:03:37 Starting pancake/parser
Sep 28 21:04:00 Finished pancake/parser                                          22s 836MB
Sep 28 21:04:01 Starting pancake/proofs
Sep 28 21:20:06 Finished pancake/proofs                                       16m04s   7GB
Sep 28 21:20:07 Starting compiler/dafny
Sep 28 21:22:52 Finished compiler/dafny                                        2m44s  10GB
Sep 28 21:22:53 Starting compiler/dafny/translation
Sep 28 21:51:48 Finished compiler/dafny/translation                           28m53s  20GB
Sep 28 21:51:49 Starting compiler/dafny/compilation
Sep 28 21:55:26 Finished compiler/dafny/compilation                            3m36s  15GB
Sep 28 21:55:27 Starting compiler/dafny/semantics
Sep 28 21:56:06 Finished compiler/dafny/semantics                                37s   1GB
Sep 28 21:56:07 Starting characteristic/examples
Sep 28 21:57:39 Finished characteristic/examples                               1m31s   5GB
Sep 28 21:57:40 Starting tutorial/solutions
Sep 28 22:00:26 Finished tutorial/solutions                                    2m44s   4GB
Sep 28 22:00:27 Starting translator/monadic/examples
Sep 28 22:03:38 Finished translator/monadic/examples                           3m10s   3GB
Sep 28 22:03:39 Starting examples
Sep 28 22:15:51 Finished examples                                             12m10s   4GB
Sep 28 22:15:52 Starting examples/compilation/x64
Sep 28 22:25:49 Finished examples/compilation/x64                              9m56s   7GB
Sep 28 22:25:50 Starting examples/compilation/x64/proofs
Sep 28 22:30:57 Finished examples/compilation/x64/proofs                       5m05s   7GB
Sep 28 22:30:58 Starting examples/compilation/ag32
Sep 28 22:33:48 Finished examples/compilation/ag32                             2m49s   5GB
Sep 28 22:33:49 Starting examples/compilation/ag32/proofs
Sep 28 22:35:44 Finished examples/compilation/ag32/proofs                      1m54s   8GB
Sep 28 22:35:45 Starting examples/compilation/to_word
Sep 28 22:40:01 Finished examples/compilation/to_word                          4m15s  13GB
Sep 28 22:40:02 Starting examples/lpr_checker
Sep 28 22:40:33 Finished examples/lpr_checker                                    30s   1GB
Sep 28 22:40:34 Starting examples/lpr_checker/array
Sep 28 23:06:45 Finished examples/lpr_checker/array                           26m09s  25GB
Sep 28 23:06:46 Starting examples/lpr_checker/array/compilation
Sep 28 23:09:26 Finished examples/lpr_checker/array/compilation                2m39s  10GB
Sep 28 23:09:27 Starting examples/lpr_checker/array/compilation/proofs
Sep 28 23:11:26 Finished examples/lpr_checker/array/compilation/proofs         1m58s   8GB
Sep 28 23:11:27 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 28 23:13:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m50s   9GB
Sep 28 23:13:19 Starting examples/xlrup_checker
Sep 28 23:13:55 Finished examples/xlrup_checker                                  34s   1GB
Sep 28 23:13:56 Starting examples/xlrup_checker/array
Sep 28 23:27:07 Finished examples/xlrup_checker/array                         13m10s  11GB
Sep 28 23:27:08 Starting examples/xlrup_checker/array/compilation
Sep 28 23:28:35 Finished examples/xlrup_checker/array/compilation              1m26s   6GB
Sep 28 23:28:36 Starting examples/xlrup_checker/array/compilation/proofs
Sep 28 23:30:37 Finished examples/xlrup_checker/array/compilation/proofs       2m00s   6GB
Sep 28 23:30:38 Starting examples/pseudo_bool
Sep 28 23:32:05 Finished examples/pseudo_bool                                  1m26s   1GB
Sep 28 23:32:06 Starting examples/pseudo_bool/cnf_encoding
Sep 28 23:32:50 Finished examples/pseudo_bool/cnf_encoding                       42s   1GB
Sep 28 23:32:51 Starting examples/pseudo_bool/graph_encoding
Sep 28 23:33:50 Finished examples/pseudo_bool/graph_encoding                     57s   2GB
Sep 28 23:33:50 Starting examples/pseudo_bool/array
Sep 29 00:37:22 Finished examples/pseudo_bool/array                         1h03m31s  28GB
Sep 29 00:37:23 Starting examples/pseudo_bool/array/compilation
Sep 29 00:51:18 Finished examples/pseudo_bool/array/compilation               13m53s  31GB
Sep 29 00:51:19 Starting examples/pseudo_bool/array/compilation/proofs
Sep 29 00:55:43 Finished examples/pseudo_bool/array/compilation/proofs         4m23s   9GB
Sep 29 00:55:44 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 29 00:57:39 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m53s   9GB
Sep 29 00:57:40 Starting examples/opentheory
Sep 29 01:06:32 Finished examples/opentheory                                   8m50s   5GB
Sep 29 01:06:33 Starting examples/opentheory
Sep 29 01:06:34 Finished examples/opentheory                                      1s 134MB
Sep 29 01:06:35 Starting examples/opentheory/compilation
Sep 29 01:08:44 Finished examples/opentheory/compilation                       2m07s   9GB
Sep 29 01:08:45 Starting examples/opentheory/compilation/proofs
Sep 29 01:10:40 Finished examples/opentheory/compilation/proofs                1m54s  10GB
Sep 29 01:10:41 Starting examples/opentheory/compilation/ag32
Sep 29 01:12:51 Finished examples/opentheory/compilation/ag32                  2m09s   8GB
Sep 29 01:12:52 Starting examples/opentheory/compilation/ag32/proofs
Sep 29 01:15:24 Finished examples/opentheory/compilation/ag32/proofs           2m30s  13GB
Sep 29 01:15:25 Starting examples/sat_encodings
Sep 29 01:16:27 Finished examples/sat_encodings                                1m01s 929MB
Sep 29 01:16:28 Starting examples/sat_encodings/case_studies
Sep 29 01:18:45 Finished examples/sat_encodings/case_studies                   2m15s   2GB
Sep 29 01:18:45 Starting examples/sat_encodings/translation
Sep 29 01:22:30 Finished examples/sat_encodings/translation                    3m43s   3GB
Sep 29 01:22:31 Starting examples/sat_encodings/translation/compilation
Sep 29 01:25:02 Finished examples/sat_encodings/translation/compilation        2m30s   7GB
Sep 29 01:25:03 Starting examples/deflate
Sep 29 01:25:31 Finished examples/deflate                                        27s 764MB
Sep 29 01:25:32 Starting examples/deflate/translation
Sep 29 01:26:33 Finished examples/deflate/translation                          1m00s   2GB
Sep 29 01:26:34 Starting examples/deflate/translation/compilation
Sep 29 01:27:44 Finished examples/deflate/translation/compilation              1m08s   6GB
Sep 29 01:27:45 Starting examples/vipr
Sep 29 01:31:25 Finished examples/vipr                                         3m39s   4GB
Sep 29 01:31:26 Starting examples/vipr/compilation
Sep 29 01:32:46 Finished examples/vipr/compilation                             1m19s   6GB
Sep 29 01:32:47 Starting translator/okasaki-examples
Sep 29 01:37:06 Finished translator/okasaki-examples                           4m18s   4GB
Sep 29 01:37:07 Starting translator/other-examples
Sep 29 01:38:25 Finished translator/other-examples                             1m16s   3GB
Sep 29 01:38:26 Starting compiler/parsing/tests
Sep 29 01:39:05 Finished compiler/parsing/tests                                  38s   2GB
Sep 29 01:39:06 Starting compiler/inference/tests
Sep 29 01:39:53 Finished compiler/inference/tests                                46s   3GB
Sep 29 01:39:54 Starting compiler/printing/test
Sep 29 01:41:34 Finished compiler/printing/test                                1m39s   6GB
Sep 29 01:41:35 Starting icing/flover
Sep 29 02:18:48 Finished icing/flover                                         37m11s   3GB
Sep 29 02:18:49 Starting icing/
Sep 29 02:46:52 Finished icing/                                               28m01s   5GB
Sep 29 02:46:53 Starting icing/examples
Sep 29 02:48:53 Finished icing/examples                                        1m58s   9GB
Sep 29 02:48:54 Starting compiler/repl
Sep 29 02:58:12 Finished compiler/repl                                         9m17s  12GB
Sep 29 02:58:13 Starting unverified/sexpr-bootstrap/x64/64
Sep 29 03:12:22 Finished unverified/sexpr-bootstrap/x64/64                    14m07s  18GB
Sep 29 03:12:23 Starting unverified/sexpr-bootstrap/x64/32
Sep 29 03:23:15 Finished unverified/sexpr-bootstrap/x64/32                    10m50s  14GB
Sep 29 03:23:16 Starting compiler/benchmarks
Sep 29 03:24:01 Finished compiler/benchmarks                                     44s 712MB
Sep 29 03:24:02 Starting compiler/bootstrap/compilation/x64/64
Sep 29 04:09:43 Finished compiler/bootstrap/compilation/x64/64                45m39s 125GB
Sep 29 04:09:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 29 04:34:36 Finished compiler/bootstrap/compilation/x64/64/proofs         24m51s  56GB
Sep 29 04:34:37 Starting compiler/bootstrap/compilation/x64/32
Sep 29 05:15:07 Finished compiler/bootstrap/compilation/x64/32                40m28s  91GB
Sep 29 05:15:07 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 29 05:20:17 Finished compiler/bootstrap/compilation/x64/32/proofs          5m08s  25GB
Sep 29 05:20:18 Starting compiler/bootstrap/compilation/arm8/64
Sep 29 06:18:32 Finished compiler/bootstrap/compilation/arm8/64               58m13s 121GB
Sep 29 06:18:33 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 29 06:24:22 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m47s  30GB
Sep 29 06:24:22 Starting compiler/bootstrap/compilation/ag32/32
Sep 29 07:06:10 Finished compiler/bootstrap/compilation/ag32/32               41m46s 112GB
Sep 29 07:06:11 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 29 07:11:50 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m38s  30GB
Sep 29 07:11:51 SUCCESS