Job 2617

CakeML: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: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 25 19:07:22 Claimed job
Sep 25 19:07:29 Building HOL
Sep 25 19:22:45 Starting developers
Sep 25 19:22:49 Finished developers                                               2s 224MB
Sep 25 19:22:49 Starting developers/bin
Sep 25 19:23:09 Finished developers/bin                                          18s   1GB
Sep 25 19:23:10 Starting compiler/proofs
Sep 25 21:12:40 Finished compiler/proofs                                    1h49m28s  38GB
Sep 25 21:12:41 Starting compiler/bootstrap/translation
Sep 26 06:12:14 Finished compiler/bootstrap/translation                     8h59m31s  88GB
Sep 26 06:12:14 Starting semantics/ffi
Sep 26 06:12:24 Finished semantics/ffi                                            8s 655MB
Sep 26 06:12:25 Starting semantics
Sep 26 06:12:27 Finished semantics                                                0s  68MB
Sep 26 06:12:27 Starting semantics/proofs
Sep 26 06:12:53 Finished semantics/proofs                                        24s 964MB
Sep 26 06:12:53 Starting semantics/alt_semantics
Sep 26 06:13:20 Finished semantics/alt_semantics                                 25s 776MB
Sep 26 06:13:21 Starting semantics/alt_semantics/proofs
Sep 26 06:23:40 Finished semantics/alt_semantics/proofs                       10m17s   4GB
Sep 26 06:23:40 Starting basis/pure
Sep 26 06:23:42 Finished basis/pure                                               0s  75MB
Sep 26 06:23:43 Starting translator
Sep 26 06:25:25 Finished translator                                            1m40s   5GB
Sep 26 06:25:25 Starting compiler/parsing
Sep 26 06:25:27 Finished compiler/parsing                                         0s  67MB
Sep 26 06:25:28 Starting characteristic
Sep 26 06:25:30 Finished characteristic                                           0s  96MB
Sep 26 06:25:30 Starting translator/monadic
Sep 26 06:25:32 Finished translator/monadic                                       0s  93MB
Sep 26 06:25:33 Starting basis
Sep 26 06:28:04 Finished basis                                                 2m29s   5GB
Sep 26 06:28:04 Starting compiler/inference
Sep 26 06:28:06 Finished compiler/inference                                       0s  93MB
Sep 26 06:28:07 Starting compiler/backend/reg_alloc
Sep 26 06:28:08 Finished compiler/backend/reg_alloc                               0s  67MB
Sep 26 06:28:09 Starting compiler/backend/gc
Sep 26 06:28:11 Finished compiler/backend/gc                                      1s 149MB
Sep 26 06:28:12 Starting compiler/backend
Sep 26 06:28:18 Finished compiler/backend                                         4s 347MB
Sep 26 06:28:19 Starting compiler/encoders/asm
Sep 26 06:28:20 Finished compiler/encoders/asm                                    0s  90MB
Sep 26 06:28:21 Starting compiler/encoders/x64
Sep 26 06:28:23 Finished compiler/encoders/x64                                    0s 103MB
Sep 26 06:28:24 Starting compiler/encoders/arm7
Sep 26 06:28:26 Finished compiler/encoders/arm7                                   0s 103MB
Sep 26 06:28:27 Starting compiler/encoders/arm8
Sep 26 06:28:28 Finished compiler/encoders/arm8                                   0s 103MB
Sep 26 06:28:29 Starting compiler/encoders/arm8_asl
Sep 26 08:46:43 Finished compiler/encoders/arm8_asl                         2h18m11s  40GB
Sep 26 08:46:43 Starting compiler/encoders/mips
Sep 26 08:46:45 Finished compiler/encoders/mips                                   0s 101MB
Sep 26 08:46:46 Starting compiler/encoders/riscv
Sep 26 08:46:48 Finished compiler/encoders/riscv                                  0s  99MB
Sep 26 08:46:49 Starting compiler/encoders/ag32
Sep 26 08:46:50 Finished compiler/encoders/ag32                                   0s  97MB
Sep 26 08:46:51 Starting compiler/backend/x64
Sep 26 08:46:53 Finished compiler/backend/x64                                     1s 138MB
Sep 26 08:46:54 Starting compiler/backend/arm7
Sep 26 08:46:56 Finished compiler/backend/arm7                                    1s 139MB
Sep 26 08:46:57 Starting compiler/backend/arm8
Sep 26 08:46:59 Finished compiler/backend/arm8                                    1s 139MB
Sep 26 08:47:00 Starting compiler/backend/mips
Sep 26 08:47:02 Finished compiler/backend/mips                                    1s 140MB
Sep 26 08:47:03 Starting compiler/backend/riscv
Sep 26 08:47:05 Finished compiler/backend/riscv                                   1s 140MB
Sep 26 08:47:06 Starting compiler/backend/ag32
Sep 26 08:48:34 Finished compiler/backend/ag32                                 1m26s   2GB
Sep 26 08:48:35 Starting compiler/parsing/proofs
Sep 26 08:48:36 Finished compiler/parsing/proofs                                  0s  75MB
Sep 26 08:48:37 Starting compiler/inference/proofs
Sep 26 08:48:39 Finished compiler/inference/proofs                                0s  94MB
Sep 26 08:48:40 Starting compiler/backend/semantics
Sep 26 08:51:53 Finished compiler/backend/semantics                            3m12s   3GB
Sep 26 08:51:54 Starting compiler/backend/reg_alloc/proofs
Sep 26 08:51:56 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Sep 26 08:51:57 Starting compiler/backend/proofs
Sep 26 08:52:55 Finished compiler/backend/proofs                                 57s   5GB
Sep 26 08:52:56 Starting compiler/backend/serialiser
Sep 26 08:52:58 Finished compiler/backend/serialiser                              1s 149MB
Sep 26 08:52:59 Starting compiler/encoders/x64/proofs
Sep 26 09:02:52 Finished compiler/encoders/x64/proofs                          9m51s   5GB
Sep 26 09:02:53 Starting compiler/encoders/arm7/proofs
Sep 26 09:16:06 Finished compiler/encoders/arm7/proofs                        13m12s  11GB
Sep 26 09:16:07 Starting compiler/encoders/arm8/proofs
Sep 26 09:22:58 Finished compiler/encoders/arm8/proofs                         6m50s   6GB
Sep 26 09:22:59 Starting compiler/encoders/arm8_asl/proofs
Sep 26 10:13:23 Finished compiler/encoders/arm8_asl/proofs                    50m23s   9GB
Sep 26 10:13:24 Starting compiler/encoders/mips/proofs
Sep 26 10:23:21 Finished compiler/encoders/mips/proofs                         9m55s  10GB
Sep 26 10:23:22 Starting compiler/encoders/riscv/proofs
Sep 26 10:31:55 Finished compiler/encoders/riscv/proofs                        8m32s   6GB
Sep 26 10:31:56 Starting compiler/encoders/ag32/proofs
Sep 26 10:34:52 Finished compiler/encoders/ag32/proofs                         2m55s   2GB
Sep 26 10:34:53 Starting compiler/backend/x64/proofs
Sep 26 10:35:43 Finished compiler/backend/x64/proofs                             48s   3GB
Sep 26 10:35:44 Starting compiler/backend/arm7/proofs
Sep 26 10:36:34 Finished compiler/backend/arm7/proofs                            49s   2GB
Sep 26 10:36:35 Starting compiler/backend/arm8/proofs
Sep 26 10:37:20 Finished compiler/backend/arm8/proofs                            44s   3GB
Sep 26 10:37:21 Starting compiler/backend/arm8_asl
Sep 26 10:37:53 Finished compiler/backend/arm8_asl                               30s   2GB
Sep 26 10:37:54 Starting compiler/backend/mips/proofs
Sep 26 10:38:45 Finished compiler/backend/mips/proofs                            49s   3GB
Sep 26 10:38:46 Starting compiler/backend/riscv/proofs
Sep 26 10:39:42 Finished compiler/backend/riscv/proofs                           55s   4GB
Sep 26 10:39:43 Starting compiler/backend/ag32/proofs
Sep 26 10:54:36 Finished compiler/backend/ag32/proofs                         14m51s   6GB
Sep 26 10:54:36 Starting compiler/backend/cv_compute
Sep 26 10:56:28 Finished compiler/backend/cv_compute                           1m50s   3GB
Sep 26 10:56:29 Starting cv_translator
Sep 26 11:16:09 Finished cv_translator                                        19m38s  10GB
Sep 26 11:16:10 Starting candle/set-theory
Sep 26 11:17:01 Finished candle/set-theory                                       50s   1GB
Sep 26 11:17:01 Starting candle/syntax-lib
Sep 26 11:17:03 Finished candle/syntax-lib                                        0s  73MB
Sep 26 11:17:04 Starting candle/standard/syntax
Sep 26 11:17:23 Finished candle/standard/syntax                                  18s   1GB
Sep 26 11:17:24 Starting candle/standard/semantics
Sep 26 11:20:17 Finished candle/standard/semantics                             2m52s   4GB
Sep 26 11:20:18 Starting candle/standard/monadic
Sep 26 11:20:20 Finished candle/standard/monadic                                  0s 102MB
Sep 26 11:20:21 Starting candle/standard/ml_kernel
Sep 26 11:22:31 Finished candle/standard/ml_kernel                             2m09s   5GB
Sep 26 11:22:32 Starting candle/overloading/syntax
Sep 26 11:26:10 Finished candle/overloading/syntax                             3m36s   2GB
Sep 26 11:26:11 Starting candle/overloading/semantics
Sep 26 11:38:10 Finished candle/overloading/semantics                         11m58s  10GB
Sep 26 11:38:10 Starting candle/overloading/monadic
Sep 26 11:40:51 Finished candle/overloading/monadic                            2m39s   3GB
Sep 26 11:40:52 Starting candle/overloading/ml_kernel
Sep 26 11:49:03 Finished candle/overloading/ml_kernel                          8m10s   7GB
Sep 26 11:49:04 Starting candle/overloading/ml_checker
Sep 26 11:51:54 Finished candle/overloading/ml_checker                         2m49s   7GB
Sep 26 11:51:55 Starting candle/prover
Sep 26 12:02:39 Finished candle/prover                                        10m42s   5GB
Sep 26 12:02:40 Starting pancake
Sep 26 12:03:07 Finished pancake                                                 26s 986MB
Sep 26 12:03:08 Starting pancake/ffi
Sep 26 12:03:09 Finished pancake/ffi                                              0s  22MB
Sep 26 12:03:10 Starting pancake/semantics
Sep 26 12:05:22 Finished pancake/semantics                                     2m11s   2GB
Sep 26 12:05:23 Starting pancake/parser
Sep 26 12:05:46 Finished pancake/parser                                          22s 805MB
Sep 26 12:05:47 Starting pancake/proofs
Sep 26 12:22:01 Finished pancake/proofs                                       16m12s   7GB
Sep 26 12:22:01 Starting compiler/dafny
Sep 26 12:24:42 Finished compiler/dafny                                        2m39s  10GB
Sep 26 12:24:43 Starting compiler/dafny/translation
Sep 26 12:53:10 Finished compiler/dafny/translation                           28m26s  21GB
Sep 26 12:53:11 Starting compiler/dafny/compilation
Sep 26 12:56:39 Finished compiler/dafny/compilation                            3m27s  13GB
Sep 26 12:56:40 Starting compiler/dafny/semantics
Sep 26 12:57:17 Finished compiler/dafny/semantics                                35s   1GB
Sep 26 12:57:18 Starting characteristic/examples
Sep 26 12:58:49 Finished characteristic/examples                               1m29s   5GB
Sep 26 12:58:50 Starting tutorial/solutions
Sep 26 13:01:44 Finished tutorial/solutions                                    2m53s   6GB
Sep 26 13:01:45 Starting translator/monadic/examples
Sep 26 13:05:02 Finished translator/monadic/examples                           3m15s   3GB
Sep 26 13:05:03 Starting examples
Sep 26 13:17:17 Finished examples                                             12m13s   6GB
Sep 26 13:17:18 Starting examples/compilation/x64
Sep 26 13:27:19 Finished examples/compilation/x64                             10m00s   7GB
Sep 26 13:27:20 Starting examples/compilation/x64/proofs
Sep 26 13:32:15 Finished examples/compilation/x64/proofs                       4m53s   8GB
Sep 26 13:32:16 Starting examples/compilation/ag32
Sep 26 13:35:01 Finished examples/compilation/ag32                             2m44s   5GB
Sep 26 13:35:02 Starting examples/compilation/ag32/proofs
Sep 26 13:37:08 Finished examples/compilation/ag32/proofs                      2m04s   8GB
Sep 26 13:37:09 Starting examples/compilation/to_word
Sep 26 13:41:26 Finished examples/compilation/to_word                          4m16s  13GB
Sep 26 13:41:27 Starting examples/lpr_checker
Sep 26 13:42:06 Finished examples/lpr_checker                                    38s   1GB
Sep 26 13:42:07 Starting examples/lpr_checker/array
Sep 26 14:08:33 Finished examples/lpr_checker/array                           26m25s  25GB
Sep 26 14:08:34 Starting examples/lpr_checker/array/compilation
Sep 26 14:11:14 Finished examples/lpr_checker/array/compilation                2m38s  10GB
Sep 26 14:11:15 Starting examples/lpr_checker/array/compilation/proofs
Sep 26 14:13:20 Finished examples/lpr_checker/array/compilation/proofs         2m04s   9GB
Sep 26 14:13:21 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 26 14:15:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m55s   8GB
Sep 26 14:15:18 Starting examples/xlrup_checker
Sep 26 14:15:55 Finished examples/xlrup_checker                                  35s   1GB
Sep 26 14:15:56 Starting examples/xlrup_checker/array
Sep 26 14:29:04 Finished examples/xlrup_checker/array                         13m06s  11GB
Sep 26 14:29:05 Starting examples/xlrup_checker/array/compilation
Sep 26 14:30:35 Finished examples/xlrup_checker/array/compilation              1m29s   6GB
Sep 26 14:30:36 Starting examples/xlrup_checker/array/compilation/proofs
Sep 26 14:32:23 Finished examples/xlrup_checker/array/compilation/proofs       1m46s   9GB
Sep 26 14:32:24 Starting examples/pseudo_bool
Sep 26 14:33:51 Finished examples/pseudo_bool                                  1m26s   1GB
Sep 26 14:33:52 Starting examples/pseudo_bool/cnf_encoding
Sep 26 14:34:34 Finished examples/pseudo_bool/cnf_encoding                       40s   1GB
Sep 26 14:34:35 Starting examples/pseudo_bool/graph_encoding
Sep 26 14:35:34 Finished examples/pseudo_bool/graph_encoding                     58s   2GB
Sep 26 14:35:35 Starting examples/pseudo_bool/array
Sep 26 15:38:51 Finished examples/pseudo_bool/array                         1h03m15s  37GB
Sep 26 15:38:52 Starting examples/pseudo_bool/array/compilation
Sep 26 15:52:43 Finished examples/pseudo_bool/array/compilation               13m49s  29GB
Sep 26 15:52:44 Starting examples/pseudo_bool/array/compilation/proofs
Sep 26 15:57:01 Finished examples/pseudo_bool/array/compilation/proofs         4m16s  11GB
Sep 26 15:57:02 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 26 15:58:55 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m52s  10GB
Sep 26 15:58:56 Starting examples/opentheory
Sep 26 16:07:40 Finished examples/opentheory                                   8m43s   5GB
Sep 26 16:07:41 Starting examples/opentheory
Sep 26 16:07:43 Finished examples/opentheory                                      1s 133MB
Sep 26 16:07:44 Starting examples/opentheory/compilation
Sep 26 16:09:54 Finished examples/opentheory/compilation                       2m09s  10GB
Sep 26 16:09:55 Starting examples/opentheory/compilation/proofs
Sep 26 16:11:50 Finished examples/opentheory/compilation/proofs                1m53s   6GB
Sep 26 16:11:50 Starting examples/opentheory/compilation/ag32
Sep 26 16:14:07 Finished examples/opentheory/compilation/ag32                  2m16s   9GB
Sep 26 16:14:08 Starting examples/opentheory/compilation/ag32/proofs
Sep 26 16:16:42 Finished examples/opentheory/compilation/ag32/proofs           2m32s  12GB
Sep 26 16:16:43 Starting examples/sat_encodings
Sep 26 16:17:46 Finished examples/sat_encodings                                1m02s 935MB
Sep 26 16:17:47 Starting examples/sat_encodings/case_studies
Sep 26 16:20:02 Finished examples/sat_encodings/case_studies                   2m14s   2GB
Sep 26 16:20:02 Starting examples/sat_encodings/translation
Sep 26 16:23:45 Finished examples/sat_encodings/translation                    3m41s   3GB
Sep 26 16:23:46 Starting examples/sat_encodings/translation/compilation
Sep 26 16:26:19 Finished examples/sat_encodings/translation/compilation        2m32s   7GB
Sep 26 16:26:20 Starting examples/deflate
Sep 26 16:26:48 Finished examples/deflate                                        27s 764MB
Sep 26 16:26:49 Starting examples/deflate/translation
Sep 26 16:27:51 Finished examples/deflate/translation                          1m00s   2GB
Sep 26 16:27:52 Starting examples/deflate/translation/compilation
Sep 26 16:29:01 Finished examples/deflate/translation/compilation              1m08s   6GB
Sep 26 16:29:02 Starting examples/vipr
Sep 26 16:32:38 Finished examples/vipr                                         3m34s   4GB
Sep 26 16:32:39 Starting examples/vipr/compilation
Sep 26 16:33:59 Finished examples/vipr/compilation                             1m18s   6GB
Sep 26 16:34:00 Starting translator/okasaki-examples
Sep 26 16:38:20 Finished translator/okasaki-examples                           4m19s   4GB
Sep 26 16:38:21 Starting translator/other-examples
Sep 26 16:43:31 Finished translator/other-examples                             5m08s   3GB
Sep 26 16:43:32 Starting compiler/parsing/tests
Sep 26 16:44:11 Finished compiler/parsing/tests                                  38s   2GB
Sep 26 16:44:12 Starting compiler/inference/tests
Sep 26 16:44:59 Finished compiler/inference/tests                                46s   3GB
Sep 26 16:45:00 Starting compiler/printing/test
Sep 26 16:46:41 Finished compiler/printing/test                                1m39s   7GB
Sep 26 16:46:42 Starting icing/flover
Sep 26 17:23:35 Finished icing/flover                                         36m52s   4GB
Sep 26 17:23:36 Starting icing/
Sep 26 17:51:25 Finished icing/                                               27m48s   7GB
Sep 26 17:51:26 Starting icing/examples
Sep 26 17:53:20 Finished icing/examples                                        1m52s   9GB
Sep 26 17:53:21 Starting compiler/repl
Sep 26 18:02:34 Finished compiler/repl                                         9m12s  11GB
Sep 26 18:02:35 Starting unverified/sexpr-bootstrap/x64/64
Sep 26 18:16:41 Finished unverified/sexpr-bootstrap/x64/64                    13m39s  17GB
Sep 26 18:16:42 Starting unverified/sexpr-bootstrap/x64/32
Sep 26 18:28:16 Finished unverified/sexpr-bootstrap/x64/32                    11m14s  16GB
Sep 26 18:28:17 Starting compiler/benchmarks
Sep 26 18:29:03 Finished compiler/benchmarks                                     44s 711MB
Sep 26 18:29:03 Starting compiler/bootstrap/compilation/x64/64
Sep 26 19:15:18 Finished compiler/bootstrap/compilation/x64/64                46m01s 129GB
Sep 26 19:15:19 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 26 19:40:48 Finished compiler/bootstrap/compilation/x64/64/proofs         25m27s  53GB
Sep 26 19:40:49 Starting compiler/bootstrap/compilation/x64/32
Sep 26 20:22:33 Finished compiler/bootstrap/compilation/x64/32                41m35s 105GB
Sep 26 20:22:33 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 26 20:27:50 Finished compiler/bootstrap/compilation/x64/32/proofs          5m15s  26GB
Sep 26 20:27:51 Starting compiler/bootstrap/compilation/arm8/64
Sep 26 21:27:50 Finished compiler/bootstrap/compilation/arm8/64               59m50s 130GB
Sep 26 21:27:51 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 26 21:33:50 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m58s  30GB
Sep 26 21:33:51 Starting compiler/bootstrap/compilation/ag32/32
Sep 26 22:15:48 Finished compiler/bootstrap/compilation/ag32/32               41m55s 104GB
Sep 26 22:15:49 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 26 22:21:42 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m52s  32GB
Sep 26 22:21:42 SUCCESS