Job 2625

CakeML:283d3066096e12168a754375b0711d33518c5938
  Merge pull request #1056 from CakeML/new-quotes [Sep 29 07:23:28]
HOL:72a01e7935ee7175f22527332d54ac58085668ed
  Add more primitive proof rules [Sep 23 23:08:36]
Machine:lammmington
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 29 07:37:13 Claimed job
Sep 29 07:37:17 Reusing HOL
Sep 29 07:37:29 Starting developers
Sep 29 07:37:33 Finished developers                                               3s 215MB
Sep 29 07:37:34 Starting developers/bin
Sep 29 07:38:00 Finished developers/bin                                          25s   1GB
Sep 29 07:38:01 Starting compiler/proofs
Sep 29 09:23:11 Finished compiler/proofs                                    1h45m09s  46GB
Sep 29 09:23:12 Starting compiler/bootstrap/translation
Sep 29 18:30:46 Finished compiler/bootstrap/translation                     9h07m31s  81GB
Sep 29 18:30:47 Starting semantics/ffi
Sep 29 18:30:56 Finished semantics/ffi                                            8s 635MB
Sep 29 18:30:57 Starting semantics
Sep 29 18:30:59 Finished semantics                                                0s  68MB
Sep 29 18:31:00 Starting semantics/proofs
Sep 29 18:31:24 Finished semantics/proofs                                        23s 794MB
Sep 29 18:31:25 Starting semantics/alt_semantics
Sep 29 18:31:52 Finished semantics/alt_semantics                                 26s 777MB
Sep 29 18:31:53 Starting semantics/alt_semantics/proofs
Sep 29 18:42:15 Finished semantics/alt_semantics/proofs                       10m20s   3GB
Sep 29 18:42:16 Starting basis/pure
Sep 29 18:42:17 Finished basis/pure                                               0s  74MB
Sep 29 18:42:18 Starting translator
Sep 29 18:43:56 Finished translator                                            1m37s   4GB
Sep 29 18:43:57 Starting compiler/parsing
Sep 29 18:43:59 Finished compiler/parsing                                         0s  72MB
Sep 29 18:44:00 Starting characteristic
Sep 29 18:44:01 Finished characteristic                                           0s  95MB
Sep 29 18:44:02 Starting translator/monadic
Sep 29 18:44:04 Finished translator/monadic                                       0s  92MB
Sep 29 18:44:05 Starting basis
Sep 29 18:46:27 Finished basis                                                 2m21s   4GB
Sep 29 18:46:28 Starting compiler/inference
Sep 29 18:46:29 Finished compiler/inference                                       0s  93MB
Sep 29 18:46:30 Starting compiler/backend/reg_alloc
Sep 29 18:46:32 Finished compiler/backend/reg_alloc                               0s  67MB
Sep 29 18:46:33 Starting compiler/backend/gc
Sep 29 18:46:35 Finished compiler/backend/gc                                      1s 139MB
Sep 29 18:46:36 Starting compiler/backend
Sep 29 18:46:41 Finished compiler/backend                                         4s 318MB
Sep 29 18:46:42 Starting compiler/encoders/asm
Sep 29 18:46:43 Finished compiler/encoders/asm                                    0s  89MB
Sep 29 18:46:44 Starting compiler/encoders/x64
Sep 29 18:46:46 Finished compiler/encoders/x64                                    0s 101MB
Sep 29 18:46:47 Starting compiler/encoders/arm7
Sep 29 18:46:49 Finished compiler/encoders/arm7                                   0s 102MB
Sep 29 18:46:50 Starting compiler/encoders/arm8
Sep 29 18:46:51 Finished compiler/encoders/arm8                                   0s 104MB
Sep 29 18:46:52 Starting compiler/encoders/arm8_asl
Sep 29 18:49:05 Finished compiler/encoders/arm8_asl                            2m11s   1GB
Sep 29 18:49:05 Starting compiler/encoders/mips
Sep 29 18:49:07 Finished compiler/encoders/mips                                   0s  93MB
Sep 29 18:49:08 Starting compiler/encoders/riscv
Sep 29 18:49:10 Finished compiler/encoders/riscv                                  0s 103MB
Sep 29 18:49:11 Starting compiler/encoders/ag32
Sep 29 18:49:12 Finished compiler/encoders/ag32                                   0s  97MB
Sep 29 18:49:13 Starting compiler/backend/x64
Sep 29 18:49:15 Finished compiler/backend/x64                                     1s 137MB
Sep 29 18:49:16 Starting compiler/backend/arm7
Sep 29 18:49:18 Finished compiler/backend/arm7                                    1s 144MB
Sep 29 18:49:19 Starting compiler/backend/arm8
Sep 29 18:49:21 Finished compiler/backend/arm8                                    1s 143MB
Sep 29 18:49:22 Starting compiler/backend/mips
Sep 29 18:49:24 Finished compiler/backend/mips                                    1s 139MB
Sep 29 18:49:25 Starting compiler/backend/riscv
Sep 29 18:49:27 Finished compiler/backend/riscv                                   1s 138MB
Sep 29 18:49:28 Starting compiler/backend/ag32
Sep 29 18:50:40 Finished compiler/backend/ag32                                 1m10s   2GB
Sep 29 18:50:40 Starting compiler/parsing/proofs
Sep 29 18:50:42 Finished compiler/parsing/proofs                                  0s  74MB
Sep 29 18:50:43 Starting compiler/inference/proofs
Sep 29 18:50:45 Finished compiler/inference/proofs                                0s  90MB
Sep 29 18:50:45 Starting compiler/backend/semantics
Sep 29 18:53:56 Finished compiler/backend/semantics                            3m09s   3GB
Sep 29 18:53:57 Starting compiler/backend/reg_alloc/proofs
Sep 29 18:53:59 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Sep 29 18:54:00 Starting compiler/backend/proofs
Sep 29 18:54:59 Finished compiler/backend/proofs                                 58s   5GB
Sep 29 18:55:00 Starting compiler/backend/serialiser
Sep 29 18:55:02 Finished compiler/backend/serialiser                              1s 147MB
Sep 29 18:55:03 Starting compiler/encoders/x64/proofs
Sep 29 19:05:16 Finished compiler/encoders/x64/proofs                         10m12s   5GB
Sep 29 19:05:17 Starting compiler/encoders/arm7/proofs
Sep 29 19:18:22 Finished compiler/encoders/arm7/proofs                        13m03s   8GB
Sep 29 19:18:23 Starting compiler/encoders/arm8/proofs
Sep 29 19:25:11 Finished compiler/encoders/arm8/proofs                         6m47s   6GB
Sep 29 19:25:12 Starting compiler/encoders/arm8_asl/proofs
Sep 29 19:40:31 Finished compiler/encoders/arm8_asl/proofs                    15m17s   4GB
Sep 29 19:40:32 Starting compiler/encoders/mips/proofs
Sep 29 19:50:46 Finished compiler/encoders/mips/proofs                        10m12s   5GB
Sep 29 19:50:47 Starting compiler/encoders/riscv/proofs
Sep 29 19:59:18 Finished compiler/encoders/riscv/proofs                        8m29s   4GB
Sep 29 19:59:19 Starting compiler/encoders/ag32/proofs
Sep 29 20:02:16 Finished compiler/encoders/ag32/proofs                         2m56s   2GB
Sep 29 20:02:16 Starting compiler/backend/x64/proofs
Sep 29 20:03:03 Finished compiler/backend/x64/proofs                             45s   3GB
Sep 29 20:03:04 Starting compiler/backend/arm7/proofs
Sep 29 20:03:52 Finished compiler/backend/arm7/proofs                            46s   2GB
Sep 29 20:03:52 Starting compiler/backend/arm8/proofs
Sep 29 20:04:43 Finished compiler/backend/arm8/proofs                            49s   3GB
Sep 29 20:04:43 Starting compiler/backend/arm8_asl
Sep 29 20:05:15 Finished compiler/backend/arm8_asl                               30s   2GB
Sep 29 20:05:16 Starting compiler/backend/mips/proofs
Sep 29 20:06:07 Finished compiler/backend/mips/proofs                            49s   3GB
Sep 29 20:06:08 Starting compiler/backend/riscv/proofs
Sep 29 20:07:04 Finished compiler/backend/riscv/proofs                           55s   4GB
Sep 29 20:07:05 Starting compiler/backend/ag32/proofs
Sep 29 20:23:08 Finished compiler/backend/ag32/proofs                         16m01s   6GB
Sep 29 20:23:09 Starting compiler/backend/cv_compute
Sep 29 20:24:59 Finished compiler/backend/cv_compute                           1m49s   3GB
Sep 29 20:25:00 Starting cv_translator
Sep 29 20:44:59 Finished cv_translator                                        19m58s  10GB
Sep 29 20:45:00 Starting candle/set-theory
Sep 29 20:45:48 Finished candle/set-theory                                       46s   1GB
Sep 29 20:45:49 Starting candle/syntax-lib
Sep 29 20:45:50 Finished candle/syntax-lib                                        0s  72MB
Sep 29 20:45:51 Starting candle/standard/syntax
Sep 29 20:46:11 Finished candle/standard/syntax                                  19s   1GB
Sep 29 20:46:12 Starting candle/standard/semantics
Sep 29 20:49:06 Finished candle/standard/semantics                             2m52s   3GB
Sep 29 20:49:07 Starting candle/standard/monadic
Sep 29 20:49:08 Finished candle/standard/monadic                                  0s 108MB
Sep 29 20:49:09 Starting candle/standard/ml_kernel
Sep 29 20:51:22 Finished candle/standard/ml_kernel                             2m12s   4GB
Sep 29 20:51:23 Starting candle/overloading/syntax
Sep 29 20:55:03 Finished candle/overloading/syntax                             3m39s   3GB
Sep 29 20:55:04 Starting candle/overloading/semantics
Sep 29 21:06:47 Finished candle/overloading/semantics                         11m41s   6GB
Sep 29 21:06:48 Starting candle/overloading/monadic
Sep 29 21:09:31 Finished candle/overloading/monadic                            2m42s   3GB
Sep 29 21:09:32 Starting candle/overloading/ml_kernel
Sep 29 21:17:38 Finished candle/overloading/ml_kernel                          8m04s   7GB
Sep 29 21:17:39 Starting candle/overloading/ml_checker
Sep 29 21:20:27 Finished candle/overloading/ml_checker                         2m47s   7GB
Sep 29 21:20:28 Starting candle/prover
Sep 29 21:31:16 Finished candle/prover                                        10m46s   6GB
Sep 29 21:31:17 Starting pancake
Sep 29 21:31:44 Finished pancake                                                 26s 994MB
Sep 29 21:31:45 Starting pancake/ffi
Sep 29 21:31:46 Finished pancake/ffi                                              0s  22MB
Sep 29 21:31:47 Starting pancake/semantics
Sep 29 21:33:56 Finished pancake/semantics                                     2m08s   2GB
Sep 29 21:33:57 Starting pancake/parser
Sep 29 21:34:20 Finished pancake/parser                                          22s 791MB
Sep 29 21:34:21 Starting pancake/proofs
Sep 29 21:50:31 Finished pancake/proofs                                       16m09s   6GB
Sep 29 21:50:32 Starting compiler/dafny
Sep 29 21:53:15 Finished compiler/dafny                                        2m41s  10GB
Sep 29 21:53:16 Starting compiler/dafny/translation
Sep 29 22:22:21 Finished compiler/dafny/translation                           29m04s  32GB
Sep 29 22:22:22 Starting compiler/dafny/compilation
Sep 29 22:26:00 Finished compiler/dafny/compilation                            3m37s  14GB
Sep 29 22:26:01 Starting compiler/dafny/semantics
Sep 29 22:26:39 Finished compiler/dafny/semantics                                36s   1GB
Sep 29 22:26:40 Starting characteristic/examples
Sep 29 22:28:13 Finished characteristic/examples                               1m32s   5GB
Sep 29 22:28:14 Starting tutorial/solutions
Sep 29 22:31:03 Finished tutorial/solutions                                    2m47s   4GB
Sep 29 22:31:04 Starting translator/monadic/examples
Sep 29 22:34:14 Finished translator/monadic/examples                           3m09s   4GB
Sep 29 22:34:15 Starting examples
Sep 29 22:46:33 Finished examples                                             12m17s   6GB
Sep 29 22:46:34 Starting examples/compilation/x64
Sep 29 22:56:42 Finished examples/compilation/x64                             10m07s   7GB
Sep 29 22:56:43 Starting examples/compilation/x64/proofs
Sep 29 23:01:52 Finished examples/compilation/x64/proofs                       5m08s   8GB
Sep 29 23:01:53 Starting examples/compilation/ag32
Sep 29 23:04:38 Finished examples/compilation/ag32                             2m43s   5GB
Sep 29 23:04:39 Starting examples/compilation/ag32/proofs
Sep 29 23:06:36 Finished examples/compilation/ag32/proofs                      1m56s   7GB
Sep 29 23:06:37 Starting examples/compilation/to_word
Sep 29 23:10:51 Finished examples/compilation/to_word                          4m13s  12GB
Sep 29 23:10:52 Starting examples/lpr_checker
Sep 29 23:11:23 Finished examples/lpr_checker                                    30s   1GB
Sep 29 23:11:24 Starting examples/lpr_checker/array
Sep 29 23:38:02 Finished examples/lpr_checker/array                           26m37s  25GB
Sep 29 23:38:03 Starting examples/lpr_checker/array/compilation
Sep 29 23:40:45 Finished examples/lpr_checker/array/compilation                2m40s  10GB
Sep 29 23:40:46 Starting examples/lpr_checker/array/compilation/proofs
Sep 29 23:42:49 Finished examples/lpr_checker/array/compilation/proofs         2m02s   9GB
Sep 29 23:42:50 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 29 23:44:47 Finished examples/lpr_checker/array/compilation/proofsARM8     1m56s   9GB
Sep 29 23:44:47 Starting examples/xlrup_checker
Sep 29 23:45:23 Finished examples/xlrup_checker                                  34s   1GB
Sep 29 23:45:24 Starting examples/xlrup_checker/array
Sep 29 23:58:46 Finished examples/xlrup_checker/array                         13m20s  10GB
Sep 29 23:58:46 Starting examples/xlrup_checker/array/compilation
Sep 30 00:00:17 Finished examples/xlrup_checker/array/compilation              1m29s   7GB
Sep 30 00:00:18 Starting examples/xlrup_checker/array/compilation/proofs
Sep 30 00:02:04 Finished examples/xlrup_checker/array/compilation/proofs       1m44s   8GB
Sep 30 00:02:05 Starting examples/pseudo_bool
Sep 30 00:03:32 Finished examples/pseudo_bool                                  1m25s   1GB
Sep 30 00:03:32 Starting examples/pseudo_bool/cnf_encoding
Sep 30 00:04:15 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Sep 30 00:04:16 Starting examples/pseudo_bool/graph_encoding
Sep 30 00:05:15 Finished examples/pseudo_bool/graph_encoding                     58s   2GB
Sep 30 00:05:16 Starting examples/pseudo_bool/array
Sep 30 01:09:38 Finished examples/pseudo_bool/array                         1h04m20s  45GB
Sep 30 01:09:38 Starting examples/pseudo_bool/array/compilation
Sep 30 01:23:40 Finished examples/pseudo_bool/array/compilation               14m00s  31GB
Sep 30 01:23:41 Starting examples/pseudo_bool/array/compilation/proofs
Sep 30 01:27:59 Finished examples/pseudo_bool/array/compilation/proofs         4m16s  10GB
Sep 30 01:28:00 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 30 01:29:57 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m56s   8GB
Sep 30 01:29:58 Starting examples/opentheory
Sep 30 01:38:42 Finished examples/opentheory                                   8m42s   5GB
Sep 30 01:38:42 Starting examples/opentheory
Sep 30 01:38:44 Finished examples/opentheory                                      1s 134MB
Sep 30 01:38:45 Starting examples/opentheory/compilation
Sep 30 01:40:54 Finished examples/opentheory/compilation                       2m07s   9GB
Sep 30 01:40:55 Starting examples/opentheory/compilation/proofs
Sep 30 01:42:50 Finished examples/opentheory/compilation/proofs                1m54s   7GB
Sep 30 01:42:51 Starting examples/opentheory/compilation/ag32
Sep 30 01:45:04 Finished examples/opentheory/compilation/ag32                  2m11s   9GB
Sep 30 01:45:05 Starting examples/opentheory/compilation/ag32/proofs
Sep 30 01:47:41 Finished examples/opentheory/compilation/ag32/proofs           2m35s  12GB
Sep 30 01:47:42 Starting examples/sat_encodings
Sep 30 01:48:45 Finished examples/sat_encodings                                1m02s 946MB
Sep 30 01:48:46 Starting examples/sat_encodings/case_studies
Sep 30 01:51:01 Finished examples/sat_encodings/case_studies                   2m13s   2GB
Sep 30 01:51:02 Starting examples/sat_encodings/translation
Sep 30 01:54:40 Finished examples/sat_encodings/translation                    3m37s   2GB
Sep 30 01:54:41 Starting examples/sat_encodings/translation/compilation
Sep 30 01:57:15 Finished examples/sat_encodings/translation/compilation        2m33s   7GB
Sep 30 01:57:16 Starting examples/deflate
Sep 30 01:57:44 Finished examples/deflate                                        27s 743MB
Sep 30 01:57:45 Starting examples/deflate/translation
Sep 30 01:58:45 Finished examples/deflate/translation                            58s   2GB
Sep 30 01:58:46 Starting examples/deflate/translation/compilation
Sep 30 01:59:55 Finished examples/deflate/translation/compilation              1m08s   6GB
Sep 30 01:59:56 Starting examples/vipr
Sep 30 02:03:30 Finished examples/vipr                                         3m33s   4GB
Sep 30 02:03:31 Starting examples/vipr/compilation
Sep 30 02:04:52 Finished examples/vipr/compilation                             1m20s   6GB
Sep 30 02:04:53 Starting translator/okasaki-examples
Sep 30 02:09:19 Finished translator/okasaki-examples                           4m25s   3GB
Sep 30 02:09:20 Starting translator/other-examples
Sep 30 02:10:35 Finished translator/other-examples                             1m14s   3GB
Sep 30 02:10:36 Starting compiler/parsing/tests
Sep 30 02:11:15 Finished compiler/parsing/tests                                  38s   2GB
Sep 30 02:11:16 Starting compiler/inference/tests
Sep 30 02:12:04 Finished compiler/inference/tests                                46s   3GB
Sep 30 02:12:05 Starting compiler/printing/test
Sep 30 02:13:46 Finished compiler/printing/test                                1m40s   7GB
Sep 30 02:13:47 Starting icing/flover
Sep 30 02:51:16 Finished icing/flover                                         37m28s   4GB
Sep 30 02:51:17 Starting icing/
Sep 30 03:19:06 Finished icing/                                               27m47s   6GB
Sep 30 03:19:07 Starting icing/examples
Sep 30 03:21:04 Finished icing/examples                                        1m56s   9GB
Sep 30 03:21:05 Starting compiler/repl
Sep 30 03:30:28 Finished compiler/repl                                         9m22s  10GB
Sep 30 03:30:29 Starting unverified/sexpr-bootstrap/x64/64
Sep 30 03:44:57 Finished unverified/sexpr-bootstrap/x64/64                    13m58s  18GB
Sep 30 03:44:57 Starting unverified/sexpr-bootstrap/x64/32
Sep 30 03:56:28 Finished unverified/sexpr-bootstrap/x64/32                    11m08s  15GB
Sep 30 03:56:29 Starting compiler/benchmarks
Sep 30 03:57:15 Finished compiler/benchmarks                                     45s 712MB
Sep 30 03:57:16 Starting compiler/bootstrap/compilation/x64/64
Sep 30 04:43:02 Finished compiler/bootstrap/compilation/x64/64                45m32s 125GB
Sep 30 04:43:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 30 05:07:56 Finished compiler/bootstrap/compilation/x64/64/proofs         24m51s  49GB
Sep 30 05:07:57 Starting compiler/bootstrap/compilation/x64/32
Sep 30 05:52:03 Finished compiler/bootstrap/compilation/x64/32                43m57s 114GB
Sep 30 05:52:04 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 30 05:57:24 Finished compiler/bootstrap/compilation/x64/32/proofs          5m19s  24GB
Sep 30 05:57:25 Starting compiler/bootstrap/compilation/arm8/64
Sep 30 06:57:05 Finished compiler/bootstrap/compilation/arm8/64               59m30s 138GB
Sep 30 06:57:05 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 30 07:03:20 Finished compiler/bootstrap/compilation/arm8/64/proofs         6m13s  34GB
Sep 30 07:03:21 Starting compiler/bootstrap/compilation/ag32/32
Sep 30 07:45:18 Finished compiler/bootstrap/compilation/ag32/32               41m56s 101GB
Sep 30 07:45:19 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 30 07:50:50 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m29s  31GB
Sep 30 07:50:51 SUCCESS