Job 2801

CakeML:7aca9c9e635320f45bb5f2cd5f70f071c39d7310
  Merge pull request #1155 from CakeML/upstream_MD5 [Apr 07 20:22:52]
HOL:aa266667af464b9d3a22e8be1415d8f3af014c82
  Implement EQ_MP_TAC, which reverses primitive rule EQ_MP [Apr 01 04:57:21]
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

Apr 08 09:46:45 Claimed job
Apr 08 09:46:51 Reusing HOL
Apr 08 09:47:02 Starting developers
Apr 08 09:47:05 Finished developers                                               3s 218MB
Apr 08 09:47:06 Starting developers/bin
Apr 08 09:47:12 Finished developers/bin                                           4s 745MB
Apr 08 09:47:13 Starting misc
Apr 08 09:47:58 Finished misc                                                    43s   2GB
Apr 08 09:47:59 Starting compiler/proofs
Apr 08 11:33:51 Finished compiler/proofs                                    1h45m51s  27GB
Apr 08 11:33:52 Starting compiler/bootstrap/translation
Apr 08 17:26:14 Finished compiler/bootstrap/translation                     5h52m21s  94GB
Apr 08 17:26:15 Starting semantics/ffi
Apr 08 17:26:25 Finished semantics/ffi                                            9s 576MB
Apr 08 17:26:26 Starting semantics
Apr 08 17:26:28 Finished semantics                                                0s  53MB
Apr 08 17:26:28 Starting semantics/proofs
Apr 08 17:26:52 Finished semantics/proofs                                        22s 882MB
Apr 08 17:26:53 Starting semantics/alt_semantics
Apr 08 17:27:14 Finished semantics/alt_semantics                                 20s 892MB
Apr 08 17:27:15 Starting semantics/alt_semantics/proofs
Apr 08 17:37:28 Finished semantics/alt_semantics/proofs                       10m13s   2GB
Apr 08 17:37:29 Starting basis/pure
Apr 08 17:37:31 Finished basis/pure                                               0s  98MB
Apr 08 17:37:32 Starting translator
Apr 08 17:39:07 Finished translator                                            1m33s   3GB
Apr 08 17:39:08 Starting compiler/parsing
Apr 08 17:39:09 Finished compiler/parsing                                         0s  60MB
Apr 08 17:39:10 Starting characteristic
Apr 08 17:39:12 Finished characteristic                                           1s 118MB
Apr 08 17:39:13 Starting translator/monadic
Apr 08 17:39:15 Finished translator/monadic                                       1s 118MB
Apr 08 17:39:16 Starting translator/monadic/monad_base
Apr 08 17:39:17 Finished translator/monadic/monad_base                            0s  57MB
Apr 08 17:39:18 Starting basis
Apr 08 17:41:44 Finished basis                                                 2m24s   4GB
Apr 08 17:41:45 Starting compiler
Apr 08 17:41:47 Finished compiler                                                 1s 216MB
Apr 08 17:41:48 Starting compiler/inference
Apr 08 17:41:50 Finished compiler/inference                                       1s 118MB
Apr 08 17:41:51 Starting compiler/backend/reg_alloc
Apr 08 17:41:53 Finished compiler/backend/reg_alloc                               0s  58MB
Apr 08 17:41:53 Starting compiler/backend/gc
Apr 08 17:41:56 Finished compiler/backend/gc                                      1s 146MB
Apr 08 17:41:57 Starting compiler/backend
Apr 08 17:42:02 Finished compiler/backend                                         4s 254MB
Apr 08 17:42:02 Starting compiler/encoders/asm
Apr 08 17:42:04 Finished compiler/encoders/asm                                    0s  85MB
Apr 08 17:42:05 Starting compiler/encoders/x64
Apr 08 17:42:07 Finished compiler/encoders/x64                                    0s  89MB
Apr 08 17:42:08 Starting compiler/encoders/arm7
Apr 08 17:42:09 Finished compiler/encoders/arm7                                   0s  88MB
Apr 08 17:42:10 Starting compiler/encoders/arm8
Apr 08 17:42:12 Finished compiler/encoders/arm8                                   0s  87MB
Apr 08 17:42:13 Starting compiler/encoders/arm8_asl
Apr 08 17:43:11 Finished compiler/encoders/arm8_asl                              56s  20GB
Apr 08 17:43:12 Starting compiler/encoders/mips
Apr 08 17:43:13 Finished compiler/encoders/mips                                   0s  91MB
Apr 08 17:43:14 Starting compiler/encoders/riscv
Apr 08 17:43:16 Finished compiler/encoders/riscv                                  0s  86MB
Apr 08 17:43:17 Starting compiler/encoders/ag32
Apr 08 17:43:18 Finished compiler/encoders/ag32                                   0s  84MB
Apr 08 17:43:19 Starting compiler/encoders/tests
Apr 08 17:43:21 Finished compiler/encoders/tests                                  1s 111MB
Apr 08 17:43:22 Starting compiler/encoders/monadic_enc
Apr 08 17:43:24 Finished compiler/encoders/monadic_enc                            1s 144MB
Apr 08 17:43:25 Starting compiler/backend/x64
Apr 08 17:43:27 Finished compiler/backend/x64                                     1s 135MB
Apr 08 17:43:28 Starting compiler/backend/arm7
Apr 08 17:43:30 Finished compiler/backend/arm7                                    1s 134MB
Apr 08 17:43:31 Starting compiler/backend/arm8
Apr 08 17:43:33 Finished compiler/backend/arm8                                    1s 135MB
Apr 08 17:43:34 Starting compiler/backend/mips
Apr 08 17:43:37 Finished compiler/backend/mips                                    1s 135MB
Apr 08 17:43:37 Starting compiler/backend/riscv
Apr 08 17:43:40 Finished compiler/backend/riscv                                   1s 135MB
Apr 08 17:43:40 Starting compiler/backend/ag32
Apr 08 17:44:46 Finished compiler/backend/ag32                                 1m05s   2GB
Apr 08 17:44:47 Starting compiler/backend/pattern_matching
Apr 08 17:44:49 Finished compiler/backend/pattern_matching                        0s  52MB
Apr 08 17:44:50 Starting compiler/parsing/ocaml
Apr 08 17:46:32 Finished compiler/parsing/ocaml                                1m41s   1GB
Apr 08 17:46:33 Starting compiler/printing
Apr 08 17:46:35 Finished compiler/printing                                        1s 124MB
Apr 08 17:46:36 Starting compiler/parsing/proofs
Apr 08 17:46:37 Finished compiler/parsing/proofs                                  0s  66MB
Apr 08 17:46:38 Starting compiler/inference/proofs
Apr 08 17:46:40 Finished compiler/inference/proofs                                1s 122MB
Apr 08 17:46:41 Starting compiler/backend/semantics
Apr 08 17:49:46 Finished compiler/backend/semantics                            3m03s   2GB
Apr 08 17:49:47 Starting compiler/backend/reg_alloc/proofs
Apr 08 17:49:49 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Apr 08 17:49:50 Starting compiler/backend/proofs
Apr 08 17:50:37 Finished compiler/backend/proofs                                 46s   3GB
Apr 08 17:50:38 Starting compiler/backend/serialiser
Apr 08 17:50:41 Finished compiler/backend/serialiser                              1s 149MB
Apr 08 17:50:41 Starting compiler/encoders/x64/proofs
Apr 08 18:01:01 Finished compiler/encoders/x64/proofs                         10m18s   4GB
Apr 08 18:01:02 Starting compiler/encoders/arm7/proofs
Apr 08 18:14:12 Finished compiler/encoders/arm7/proofs                        13m09s  11GB
Apr 08 18:14:13 Starting compiler/encoders/arm8/proofs
Apr 08 18:21:24 Finished compiler/encoders/arm8/proofs                         7m10s   4GB
Apr 08 18:21:25 Starting compiler/encoders/arm8_asl/proofs
Apr 08 18:36:54 Finished compiler/encoders/arm8_asl/proofs                    15m28s   3GB
Apr 08 18:36:55 Starting compiler/encoders/mips/proofs
Apr 08 18:47:14 Finished compiler/encoders/mips/proofs                        10m18s   8GB
Apr 08 18:47:15 Starting compiler/encoders/riscv/proofs
Apr 08 18:55:32 Finished compiler/encoders/riscv/proofs                        8m15s   4GB
Apr 08 18:55:33 Starting compiler/encoders/ag32/proofs
Apr 08 18:58:25 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Apr 08 18:58:26 Starting compiler/backend/x64/proofs
Apr 08 18:58:58 Finished compiler/backend/x64/proofs                             31s   2GB
Apr 08 18:58:59 Starting compiler/backend/arm7/proofs
Apr 08 18:59:32 Finished compiler/backend/arm7/proofs                            32s   2GB
Apr 08 18:59:33 Starting compiler/backend/arm8/proofs
Apr 08 19:00:06 Finished compiler/backend/arm8/proofs                            32s   2GB
Apr 08 19:00:07 Starting compiler/backend/arm8_asl
Apr 08 19:00:28 Finished compiler/backend/arm8_asl                               20s   1GB
Apr 08 19:00:29 Starting compiler/backend/mips/proofs
Apr 08 19:01:00 Finished compiler/backend/mips/proofs                            29s   2GB
Apr 08 19:01:01 Starting compiler/backend/riscv/proofs
Apr 08 19:01:32 Finished compiler/backend/riscv/proofs                           30s   2GB
Apr 08 19:01:33 Starting compiler/backend/ag32/proofs
Apr 08 19:15:30 Finished compiler/backend/ag32/proofs                         13m55s   5GB
Apr 08 19:15:31 Starting compiler/backend/cv_compute
Apr 08 19:16:41 Finished compiler/backend/cv_compute                           1m09s   2GB
Apr 08 19:16:42 Starting cv_translator
Apr 08 19:37:22 Finished cv_translator                                        20m38s  10GB
Apr 08 19:37:23 Starting candle
Apr 08 19:37:24 Finished candle                                                   0s  11MB
Apr 08 19:37:25 Starting candle/set-theory
Apr 08 19:37:59 Finished candle/set-theory                                       33s   1GB
Apr 08 19:38:00 Starting candle/syntax-lib
Apr 08 19:38:02 Finished candle/syntax-lib                                        0s  89MB
Apr 08 19:38:03 Starting candle/standard
Apr 08 19:38:04 Finished candle/standard                                          0s  11MB
Apr 08 19:38:05 Starting candle/standard/syntax
Apr 08 19:38:17 Finished candle/standard/syntax                                  11s 784MB
Apr 08 19:38:18 Starting candle/standard/semantics
Apr 08 19:40:20 Finished candle/standard/semantics                             2m01s   2GB
Apr 08 19:40:21 Starting candle/standard/monadic
Apr 08 19:40:23 Finished candle/standard/monadic                                  1s 125MB
Apr 08 19:40:24 Starting candle/standard/ml_kernel
Apr 08 19:42:08 Finished candle/standard/ml_kernel                             1m42s   4GB
Apr 08 19:42:09 Starting candle/standard/ml_kernel/lisp
Apr 08 19:42:10 Finished candle/standard/ml_kernel/lisp                           0s  48MB
Apr 08 19:42:11 Starting candle/overloading
Apr 08 19:42:12 Finished candle/overloading                                       0s  12MB
Apr 08 19:42:13 Starting candle/overloading/syntax
Apr 08 19:45:25 Finished candle/overloading/syntax                             3m10s   2GB
Apr 08 19:45:26 Starting candle/overloading/semantics
Apr 08 19:56:21 Finished candle/overloading/semantics                         10m55s   7GB
Apr 08 19:56:22 Starting candle/overloading/monadic
Apr 08 19:58:42 Finished candle/overloading/monadic                            2m18s   2GB
Apr 08 19:58:43 Starting candle/overloading/ml_kernel
Apr 08 20:05:58 Finished candle/overloading/ml_kernel                          7m13s   6GB
Apr 08 20:05:59 Starting candle/overloading/ml_checker
Apr 08 20:08:07 Finished candle/overloading/ml_checker                         2m07s   4GB
Apr 08 20:08:08 Starting candle/prover
Apr 08 20:17:49 Finished candle/prover                                         9m40s   5GB
Apr 08 20:17:50 Starting candle/prover/compute
Apr 08 20:17:52 Finished candle/prover/compute                                    1s 145MB
Apr 08 20:17:53 Starting pancake
Apr 08 20:18:16 Finished pancake                                                 22s 809MB
Apr 08 20:18:17 Starting pancake/semantics
Apr 08 20:20:26 Finished pancake/semantics                                     2m08s   2GB
Apr 08 20:20:27 Starting pancake/parser
Apr 08 20:20:51 Finished pancake/parser                                          22s 490MB
Apr 08 20:20:52 Starting pancake/static_checker
Apr 08 20:21:30 Finished pancake/static_checker                                  37s   1GB
Apr 08 20:21:31 Starting pancake/proofs
Apr 08 20:37:50 Finished pancake/proofs                                       16m18s   7GB
Apr 08 20:37:51 Starting pancake/ta_progs
Apr 08 20:37:52 Finished pancake/ta_progs                                         0s  12MB
Apr 08 20:37:53 Starting compiler/dafny
Apr 08 20:40:38 Finished compiler/dafny                                        2m43s  11GB
Apr 08 20:40:39 Starting compiler/dafny/translation
Apr 08 20:59:56 Finished compiler/dafny/translation                           19m16s  21GB
Apr 08 20:59:57 Starting compiler/dafny/compilation
Apr 08 21:02:58 Finished compiler/dafny/compilation                            2m59s  12GB
Apr 08 21:02:59 Starting compiler/dafny/semantics
Apr 08 21:03:34 Finished compiler/dafny/semantics                                34s   1GB
Apr 08 21:03:35 Starting characteristic/examples
Apr 08 21:04:59 Finished characteristic/examples                               1m22s   4GB
Apr 08 21:04:59 Starting tutorial/solutions
Apr 08 21:07:26 Finished tutorial/solutions                                    2m26s   3GB
Apr 08 21:07:27 Starting translator/monadic/examples
Apr 08 21:10:23 Finished translator/monadic/examples                           2m55s   3GB
Apr 08 21:10:24 Starting examples
Apr 08 21:16:26 Finished examples                                              6m00s   4GB
Apr 08 21:16:27 Starting examples/compilation
Apr 08 21:16:28 Finished examples/compilation                                     0s  11MB
Apr 08 21:16:29 Starting examples/compilation/x64
Apr 08 21:23:28 Finished examples/compilation/x64                              6m57s   4GB
Apr 08 21:23:29 Starting examples/compilation/x64/proofs
Apr 08 21:25:55 Finished examples/compilation/x64/proofs                       2m25s   4GB
Apr 08 21:25:56 Starting examples/compilation/ag32
Apr 08 21:27:51 Finished examples/compilation/ag32                             1m54s   3GB
Apr 08 21:27:52 Starting examples/compilation/ag32/proofs
Apr 08 21:28:55 Finished examples/compilation/ag32/proofs                      1m01s   5GB
Apr 08 21:28:55 Starting examples/lpr_checker
Apr 08 21:29:25 Finished examples/lpr_checker                                    28s   1GB
Apr 08 21:29:26 Starting examples/lpr_checker/array
Apr 08 21:55:41 Finished examples/lpr_checker/array                           26m13s  24GB
Apr 08 21:55:42 Starting examples/lpr_checker/array/compilation
Apr 08 21:58:01 Finished examples/lpr_checker/array/compilation                2m18s   7GB
Apr 08 21:58:02 Starting examples/lpr_checker/array/compilation/proofs
Apr 08 21:59:13 Finished examples/lpr_checker/array/compilation/proofs         1m10s   6GB
Apr 08 21:59:14 Starting examples/lpr_checker/array/compilation/proofsARM8
Apr 08 22:00:21 Finished examples/lpr_checker/array/compilation/proofsARM8     1m06s   6GB
Apr 08 22:00:22 Starting .
Apr 08 22:00:26 Finished .                                                        2s 318MB
Apr 08 22:00:27 Starting examples/xlrup_checker
Apr 08 22:01:01 Finished examples/xlrup_checker                                  33s   1GB
Apr 08 22:01:02 Starting examples/xlrup_checker/array
Apr 08 22:13:55 Finished examples/xlrup_checker/array                         12m51s   8GB
Apr 08 22:13:55 Starting examples/xlrup_checker/array/compilation
Apr 08 22:14:58 Finished examples/xlrup_checker/array/compilation              1m02s   4GB
Apr 08 22:14:59 Starting examples/xlrup_checker/array/compilation/proofs
Apr 08 22:15:59 Finished examples/xlrup_checker/array/compilation/proofs         58s   4GB
Apr 08 22:16:00 Starting examples/pseudo_bool
Apr 08 22:17:32 Finished examples/pseudo_bool                                  1m30s   2GB
Apr 08 22:17:33 Starting examples/pseudo_bool/cnf_encoding
Apr 08 22:18:02 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Apr 08 22:18:03 Starting examples/pseudo_bool/graph_encoding
Apr 08 22:18:47 Finished examples/pseudo_bool/graph_encoding                     43s   1GB
Apr 08 22:18:48 Starting examples/pseudo_bool/array
Apr 08 23:27:34 Finished examples/pseudo_bool/array                         1h08m45s  28GB
Apr 08 23:27:35 Starting examples/pseudo_bool/array/compilation
Apr 08 23:37:38 Finished examples/pseudo_bool/array/compilation               10m01s  19GB
Apr 08 23:37:39 Starting examples/pseudo_bool/array/compilation/proofs
Apr 08 23:40:41 Finished examples/pseudo_bool/array/compilation/proofs         3m00s   6GB
Apr 08 23:40:41 Starting examples/pseudo_bool/array/compilation/proofsARM8
Apr 08 23:41:53 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m10s   6GB
Apr 08 23:41:54 Starting examples/opentheory
Apr 08 23:50:24 Finished examples/opentheory                                   8m29s   5GB
Apr 08 23:50:25 Starting examples/opentheory/compilation
Apr 08 23:51:58 Finished examples/opentheory/compilation                       1m32s   6GB
Apr 08 23:51:59 Starting examples/opentheory/compilation/proofs
Apr 08 23:52:57 Finished examples/opentheory/compilation/proofs                  56s   4GB
Apr 08 23:52:58 Starting examples/opentheory/compilation/ag32
Apr 08 23:54:36 Finished examples/opentheory/compilation/ag32                  1m37s   7GB
Apr 08 23:54:37 Starting examples/opentheory/compilation/ag32/proofs
Apr 08 23:56:14 Finished examples/opentheory/compilation/ag32/proofs           1m35s   8GB
Apr 08 23:56:15 Starting examples/sat_encodings
Apr 08 23:57:14 Finished examples/sat_encodings                                  58s 768MB
Apr 08 23:57:15 Starting examples/sat_encodings/demo
Apr 08 23:57:16 Finished examples/sat_encodings/demo                              0s  12MB
Apr 08 23:57:17 Starting examples/sat_encodings/case_studies
Apr 08 23:59:03 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Apr 08 23:59:04 Starting examples/sat_encodings/translation
Apr 09 00:02:38 Finished examples/sat_encodings/translation                    3m33s   3GB
Apr 09 00:02:39 Starting examples/sat_encodings/translation/compilation
Apr 09 00:04:34 Finished examples/sat_encodings/translation/compilation        1m53s   4GB
Apr 09 00:04:35 Starting examples/deflate
Apr 09 00:05:03 Finished examples/deflate                                        27s 762MB
Apr 09 00:05:04 Starting examples/deflate/translation
Apr 09 00:06:07 Finished examples/deflate/translation                          1m02s   4GB
Apr 09 00:06:08 Starting examples/deflate/translation/compilation
Apr 09 00:07:00 Finished examples/deflate/translation/compilation                50s   3GB
Apr 09 00:07:01 Starting examples/vipr
Apr 09 00:10:47 Finished examples/vipr                                         3m45s  10GB
Apr 09 00:10:48 Starting examples/vipr/compilation
Apr 09 00:11:48 Finished examples/vipr/compilation                               58s   4GB
Apr 09 00:11:49 Starting translator/okasaki-examples
Apr 09 00:15:48 Finished translator/okasaki-examples                           3m58s   3GB
Apr 09 00:15:49 Starting translator/other-examples
Apr 09 00:16:41 Finished translator/other-examples                               51s   3GB
Apr 09 00:16:42 Starting translator/other-examples/auxiliary
Apr 09 00:16:43 Finished translator/other-examples/auxiliary                      0s  13MB
Apr 09 00:16:44 Starting compiler/parsing/tests
Apr 09 00:17:19 Finished compiler/parsing/tests                                  34s   1GB
Apr 09 00:17:20 Starting compiler/inference/tests
Apr 09 00:17:56 Finished compiler/inference/tests                                34s   2GB
Apr 09 00:17:57 Starting compiler/printing/test
Apr 09 00:19:10 Finished compiler/printing/test                                1m12s   5GB
Apr 09 00:19:11 Starting icing/flover
Apr 09 00:53:34 Finished icing/flover                                         34m21s   1GB
Apr 09 00:53:35 Starting icing/flover/Infra
Apr 09 00:53:36 Finished icing/flover/Infra                                       0s  13MB
Apr 09 00:53:37 Starting icing/flover/semantics
Apr 09 00:53:38 Finished icing/flover/semantics                                   0s  14MB
Apr 09 00:53:39 Starting icing/
Apr 09 01:20:41 Finished icing/                                               27m01s   8GB
Apr 09 01:20:42 Starting icing/examples
Apr 09 01:22:06 Finished icing/examples                                        1m23s   4GB
Apr 09 01:22:07 Starting compiler/repl
Apr 09 01:30:06 Finished compiler/repl                                         7m58s   7GB
Apr 09 01:30:07 Starting unverified/sexpr-bootstrap/x64/64
Apr 09 01:34:18 Finished unverified/sexpr-bootstrap/x64/64                     3m56s  17GB
Apr 09 01:34:19 Starting unverified/sexpr-bootstrap/x64/32
Apr 09 01:37:52 Finished unverified/sexpr-bootstrap/x64/32                     3m20s  14GB
Apr 09 01:37:53 Starting compiler/benchmarks
Apr 09 01:38:39 Finished compiler/benchmarks                                     44s 711MB
Apr 09 01:38:40 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Apr 09 01:38:43 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 259MB
Apr 09 01:38:44 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Apr 09 01:38:47 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 257MB
Apr 09 01:38:48 Starting compiler/bootstrap/compilation/x64/64
Apr 09 02:06:11 Finished compiler/bootstrap/compilation/x64/64                27m09s  99GB
Apr 09 02:06:12 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 09 02:30:05 Finished compiler/bootstrap/compilation/x64/64/proofs         23m52s  44GB
Apr 09 02:30:06 Starting compiler/bootstrap/compilation/x64/32
Apr 09 02:59:44 Finished compiler/bootstrap/compilation/x64/32                29m30s  88GB
Apr 09 02:59:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 09 03:03:44 Finished compiler/bootstrap/compilation/x64/32/proofs          3m56s  22GB
Apr 09 03:03:44 Starting compiler/bootstrap/compilation/arm8/64
Apr 09 03:46:19 Finished compiler/bootstrap/compilation/arm8/64               42m26s 128GB
Apr 09 03:46:19 Starting compiler/bootstrap/compilation/arm8/64/proofs
Apr 09 03:51:47 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m26s  29GB
Apr 09 03:51:48 Starting compiler/bootstrap/compilation/ag32/32
Apr 09 04:22:51 Finished compiler/bootstrap/compilation/ag32/32               31m01s  83GB
Apr 09 04:22:52 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 09 04:27:55 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m02s  30GB
Apr 09 04:27:56 SUCCESS