Job 2802

CakeML:8ea3640e9c76f53cd35724642349f46665fb0630
  Merge pull request #1152 from CakeML/lexer-fix [Apr 09 07:17:23]
HOL:aa266667af464b9d3a22e8be1415d8f3af014c82
  Implement EQ_MP_TAC, which reverses primitive rule EQ_MP [Apr 01 04:57:21]
Machine:pavlova
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 09 07:17:42 Claimed job
Apr 09 07:17:49 Reusing HOL
Apr 09 07:17:59 Starting developers
Apr 09 07:18:03 Finished developers                                               3s 176MB
Apr 09 07:18:04 Starting developers/bin
Apr 09 07:18:11 Finished developers/bin                                           5s 746MB
Apr 09 07:18:12 Starting misc
Apr 09 07:18:55 Finished misc                                                    42s   1GB
Apr 09 07:18:56 Starting compiler/proofs
Apr 09 09:02:48 Finished compiler/proofs                                    1h43m50s  36GB
Apr 09 09:02:49 Starting compiler/bootstrap/translation
Apr 09 14:50:27 Finished compiler/bootstrap/translation                     5h47m36s  75GB
Apr 09 14:50:28 Starting semantics/ffi
Apr 09 14:50:39 Finished semantics/ffi                                            9s 572MB
Apr 09 14:50:40 Starting semantics
Apr 09 14:50:41 Finished semantics                                                0s  51MB
Apr 09 14:50:42 Starting semantics/proofs
Apr 09 14:51:05 Finished semantics/proofs                                        21s 880MB
Apr 09 14:51:06 Starting semantics/alt_semantics
Apr 09 14:51:27 Finished semantics/alt_semantics                                 20s 892MB
Apr 09 14:51:27 Starting semantics/alt_semantics/proofs
Apr 09 15:01:38 Finished semantics/alt_semantics/proofs                       10m09s   2GB
Apr 09 15:01:39 Starting basis/pure
Apr 09 15:01:41 Finished basis/pure                                               0s  92MB
Apr 09 15:01:42 Starting translator
Apr 09 15:03:15 Finished translator                                            1m32s   3GB
Apr 09 15:03:15 Starting compiler/parsing
Apr 09 15:03:17 Finished compiler/parsing                                         0s  60MB
Apr 09 15:03:18 Starting characteristic
Apr 09 15:03:20 Finished characteristic                                           1s 116MB
Apr 09 15:03:21 Starting translator/monadic
Apr 09 15:03:23 Finished translator/monadic                                       1s 122MB
Apr 09 15:03:24 Starting translator/monadic/monad_base
Apr 09 15:03:25 Finished translator/monadic/monad_base                            0s  53MB
Apr 09 15:03:26 Starting basis
Apr 09 15:05:47 Finished basis                                                 2m20s   4GB
Apr 09 15:05:48 Starting compiler
Apr 09 15:05:51 Finished compiler                                                 1s 220MB
Apr 09 15:05:52 Starting compiler/inference
Apr 09 15:05:54 Finished compiler/inference                                       1s 113MB
Apr 09 15:05:55 Starting compiler/backend/reg_alloc
Apr 09 15:05:56 Finished compiler/backend/reg_alloc                               0s  58MB
Apr 09 15:05:57 Starting compiler/backend/gc
Apr 09 15:05:59 Finished compiler/backend/gc                                      1s 146MB
Apr 09 15:06:00 Starting compiler/backend
Apr 09 15:06:05 Finished compiler/backend                                         4s 262MB
Apr 09 15:06:06 Starting compiler/encoders/asm
Apr 09 15:06:08 Finished compiler/encoders/asm                                    0s  86MB
Apr 09 15:06:09 Starting compiler/encoders/x64
Apr 09 15:06:10 Finished compiler/encoders/x64                                    0s  86MB
Apr 09 15:06:11 Starting compiler/encoders/arm7
Apr 09 15:06:13 Finished compiler/encoders/arm7                                   0s  90MB
Apr 09 15:06:14 Starting compiler/encoders/arm8
Apr 09 15:06:16 Finished compiler/encoders/arm8                                   0s  89MB
Apr 09 15:06:17 Starting compiler/encoders/arm8_asl
Apr 09 15:07:14 Finished compiler/encoders/arm8_asl                              56s  20GB
Apr 09 15:07:15 Starting compiler/encoders/mips
Apr 09 15:07:16 Finished compiler/encoders/mips                                   0s  92MB
Apr 09 15:07:17 Starting compiler/encoders/riscv
Apr 09 15:07:19 Finished compiler/encoders/riscv                                  0s  87MB
Apr 09 15:07:20 Starting compiler/encoders/ag32
Apr 09 15:07:22 Finished compiler/encoders/ag32                                   0s  85MB
Apr 09 15:07:22 Starting compiler/encoders/tests
Apr 09 15:07:24 Finished compiler/encoders/tests                                  1s 111MB
Apr 09 15:07:25 Starting compiler/encoders/monadic_enc
Apr 09 15:07:27 Finished compiler/encoders/monadic_enc                            1s 138MB
Apr 09 15:07:28 Starting compiler/backend/x64
Apr 09 15:07:31 Finished compiler/backend/x64                                     1s 134MB
Apr 09 15:07:31 Starting compiler/backend/arm7
Apr 09 15:07:34 Finished compiler/backend/arm7                                    1s 144MB
Apr 09 15:07:35 Starting compiler/backend/arm8
Apr 09 15:07:37 Finished compiler/backend/arm8                                    1s 145MB
Apr 09 15:07:38 Starting compiler/backend/mips
Apr 09 15:07:40 Finished compiler/backend/mips                                    1s 145MB
Apr 09 15:07:41 Starting compiler/backend/riscv
Apr 09 15:07:43 Finished compiler/backend/riscv                                   1s 145MB
Apr 09 15:07:44 Starting compiler/backend/ag32
Apr 09 15:08:49 Finished compiler/backend/ag32                                 1m04s   2GB
Apr 09 15:08:50 Starting compiler/backend/pattern_matching
Apr 09 15:08:51 Finished compiler/backend/pattern_matching                        0s  52MB
Apr 09 15:08:52 Starting compiler/parsing/ocaml
Apr 09 15:10:35 Finished compiler/parsing/ocaml                                1m41s   1GB
Apr 09 15:10:35 Starting compiler/printing
Apr 09 15:10:37 Finished compiler/printing                                        1s 119MB
Apr 09 15:10:38 Starting compiler/parsing/proofs
Apr 09 15:10:40 Finished compiler/parsing/proofs                                  0s  62MB
Apr 09 15:10:41 Starting compiler/inference/proofs
Apr 09 15:10:43 Finished compiler/inference/proofs                                1s 124MB
Apr 09 15:10:44 Starting compiler/backend/semantics
Apr 09 15:13:55 Finished compiler/backend/semantics                            3m08s   2GB
Apr 09 15:13:56 Starting compiler/backend/reg_alloc/proofs
Apr 09 15:13:59 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Apr 09 15:14:00 Starting compiler/backend/proofs
Apr 09 15:14:47 Finished compiler/backend/proofs                                 45s   2GB
Apr 09 15:14:48 Starting compiler/backend/serialiser
Apr 09 15:14:50 Finished compiler/backend/serialiser                              1s 149MB
Apr 09 15:14:51 Starting compiler/encoders/x64/proofs
Apr 09 15:25:04 Finished compiler/encoders/x64/proofs                         10m12s   5GB
Apr 09 15:25:05 Starting compiler/encoders/arm7/proofs
Apr 09 15:38:21 Finished compiler/encoders/arm7/proofs                        13m15s  12GB
Apr 09 15:38:22 Starting compiler/encoders/arm8/proofs
Apr 09 15:45:08 Finished compiler/encoders/arm8/proofs                         6m44s   6GB
Apr 09 15:45:09 Starting compiler/encoders/arm8_asl/proofs
Apr 09 16:00:38 Finished compiler/encoders/arm8_asl/proofs                    15m27s   3GB
Apr 09 16:00:39 Starting compiler/encoders/mips/proofs
Apr 09 16:10:41 Finished compiler/encoders/mips/proofs                        10m00s   4GB
Apr 09 16:10:42 Starting compiler/encoders/riscv/proofs
Apr 09 16:19:08 Finished compiler/encoders/riscv/proofs                        8m25s   4GB
Apr 09 16:19:09 Starting compiler/encoders/ag32/proofs
Apr 09 16:22:01 Finished compiler/encoders/ag32/proofs                         2m51s   2GB
Apr 09 16:22:02 Starting compiler/backend/x64/proofs
Apr 09 16:22:32 Finished compiler/backend/x64/proofs                             29s   2GB
Apr 09 16:22:33 Starting compiler/backend/arm7/proofs
Apr 09 16:23:03 Finished compiler/backend/arm7/proofs                            28s   1GB
Apr 09 16:23:04 Starting compiler/backend/arm8/proofs
Apr 09 16:23:34 Finished compiler/backend/arm8/proofs                            29s   2GB
Apr 09 16:23:35 Starting compiler/backend/arm8_asl
Apr 09 16:23:58 Finished compiler/backend/arm8_asl                               21s   2GB
Apr 09 16:23:59 Starting compiler/backend/mips/proofs
Apr 09 16:24:30 Finished compiler/backend/mips/proofs                            29s   2GB
Apr 09 16:24:31 Starting compiler/backend/riscv/proofs
Apr 09 16:25:05 Finished compiler/backend/riscv/proofs                           33s   2GB
Apr 09 16:25:06 Starting compiler/backend/ag32/proofs
Apr 09 16:38:40 Finished compiler/backend/ag32/proofs                         13m33s   5GB
Apr 09 16:38:41 Starting compiler/backend/cv_compute
Apr 09 16:39:51 Finished compiler/backend/cv_compute                           1m08s   2GB
Apr 09 16:39:52 Starting cv_translator
Apr 09 17:00:32 Finished cv_translator                                        20m39s  12GB
Apr 09 17:00:33 Starting candle
Apr 09 17:00:34 Finished candle                                                   0s  12MB
Apr 09 17:00:35 Starting candle/set-theory
Apr 09 17:01:10 Finished candle/set-theory                                       33s   1GB
Apr 09 17:01:10 Starting candle/syntax-lib
Apr 09 17:01:12 Finished candle/syntax-lib                                        0s  92MB
Apr 09 17:01:13 Starting candle/standard
Apr 09 17:01:14 Finished candle/standard                                          0s  11MB
Apr 09 17:01:15 Starting candle/standard/syntax
Apr 09 17:01:28 Finished candle/standard/syntax                                  11s 806MB
Apr 09 17:01:29 Starting candle/standard/semantics
Apr 09 17:03:30 Finished candle/standard/semantics                             2m00s   1GB
Apr 09 17:03:31 Starting candle/standard/monadic
Apr 09 17:03:33 Finished candle/standard/monadic                                  1s 126MB
Apr 09 17:03:34 Starting candle/standard/ml_kernel
Apr 09 17:05:18 Finished candle/standard/ml_kernel                             1m43s   4GB
Apr 09 17:05:19 Starting candle/standard/ml_kernel/lisp
Apr 09 17:05:20 Finished candle/standard/ml_kernel/lisp                           0s  49MB
Apr 09 17:05:21 Starting candle/overloading
Apr 09 17:05:22 Finished candle/overloading                                       0s  11MB
Apr 09 17:05:23 Starting candle/overloading/syntax
Apr 09 17:08:30 Finished candle/overloading/syntax                             3m05s   2GB
Apr 09 17:08:31 Starting candle/overloading/semantics
Apr 09 17:19:30 Finished candle/overloading/semantics                         10m58s   4GB
Apr 09 17:19:31 Starting candle/overloading/monadic
Apr 09 17:21:50 Finished candle/overloading/monadic                            2m17s   2GB
Apr 09 17:21:51 Starting candle/overloading/ml_kernel
Apr 09 17:29:07 Finished candle/overloading/ml_kernel                          7m14s   6GB
Apr 09 17:29:07 Starting candle/overloading/ml_checker
Apr 09 17:31:22 Finished candle/overloading/ml_checker                         2m13s   6GB
Apr 09 17:31:23 Starting candle/prover
Apr 09 17:40:57 Finished candle/prover                                         9m33s   5GB
Apr 09 17:40:58 Starting candle/prover/compute
Apr 09 17:41:00 Finished candle/prover/compute                                    1s 146MB
Apr 09 17:41:01 Starting pancake
Apr 09 17:41:22 Finished pancake                                                 19s 718MB
Apr 09 17:41:23 Starting pancake/semantics
Apr 09 17:43:29 Finished pancake/semantics                                     2m05s   1GB
Apr 09 17:43:30 Starting pancake/parser
Apr 09 17:43:54 Finished pancake/parser                                          22s 477MB
Apr 09 17:43:54 Starting pancake/static_checker
Apr 09 17:44:33 Finished pancake/static_checker                                  37s   1GB
Apr 09 17:44:34 Starting pancake/proofs
Apr 09 18:00:23 Finished pancake/proofs                                       15m48s   6GB
Apr 09 18:00:24 Starting pancake/ta_progs
Apr 09 18:00:25 Finished pancake/ta_progs                                         0s  12MB
Apr 09 18:00:26 Starting compiler/dafny
Apr 09 18:03:26 Finished compiler/dafny                                        2m58s  11GB
Apr 09 18:03:27 Starting compiler/dafny/translation
Apr 09 18:22:23 Finished compiler/dafny/translation                           18m55s  21GB
Apr 09 18:22:24 Starting compiler/dafny/compilation
Apr 09 18:25:19 Finished compiler/dafny/compilation                            2m53s  11GB
Apr 09 18:25:20 Starting compiler/dafny/semantics
Apr 09 18:25:55 Finished compiler/dafny/semantics                                34s   1GB
Apr 09 18:25:56 Starting characteristic/examples
Apr 09 18:27:21 Finished characteristic/examples                               1m23s   4GB
Apr 09 18:27:22 Starting tutorial/solutions
Apr 09 18:29:49 Finished tutorial/solutions                                    2m26s   3GB
Apr 09 18:29:50 Starting translator/monadic/examples
Apr 09 18:32:43 Finished translator/monadic/examples                           2m52s   4GB
Apr 09 18:32:43 Starting examples
Apr 09 18:38:37 Finished examples                                              5m52s   4GB
Apr 09 18:38:37 Starting examples/compilation
Apr 09 18:38:38 Finished examples/compilation                                     0s  11MB
Apr 09 18:38:39 Starting examples/compilation/x64
Apr 09 18:45:35 Finished examples/compilation/x64                              6m54s   4GB
Apr 09 18:45:36 Starting examples/compilation/x64/proofs
Apr 09 18:47:58 Finished examples/compilation/x64/proofs                       2m21s   4GB
Apr 09 18:47:59 Starting examples/compilation/ag32
Apr 09 18:49:54 Finished examples/compilation/ag32                             1m53s   3GB
Apr 09 18:49:54 Starting examples/compilation/ag32/proofs
Apr 09 18:50:55 Finished examples/compilation/ag32/proofs                        59s   5GB
Apr 09 18:50:56 Starting examples/lpr_checker
Apr 09 18:51:26 Finished examples/lpr_checker                                    29s   1GB
Apr 09 18:51:27 Starting examples/lpr_checker/array
Apr 09 19:17:34 Finished examples/lpr_checker/array                           26m05s  27GB
Apr 09 19:17:35 Starting examples/lpr_checker/array/compilation
Apr 09 19:19:59 Finished examples/lpr_checker/array/compilation                2m22s   7GB
Apr 09 19:20:00 Starting examples/lpr_checker/array/compilation/proofs
Apr 09 19:21:14 Finished examples/lpr_checker/array/compilation/proofs         1m13s   6GB
Apr 09 19:21:15 Starting examples/lpr_checker/array/compilation/proofsARM8
Apr 09 19:22:26 Finished examples/lpr_checker/array/compilation/proofsARM8     1m09s   6GB
Apr 09 19:22:26 Starting .
Apr 09 19:22:30 Finished .                                                        2s 338MB
Apr 09 19:22:31 Starting examples/xlrup_checker
Apr 09 19:23:06 Finished examples/xlrup_checker                                  33s   1GB
Apr 09 19:23:06 Starting examples/xlrup_checker/array
Apr 09 19:35:58 Finished examples/xlrup_checker/array                         12m50s  10GB
Apr 09 19:35:59 Starting examples/xlrup_checker/array/compilation
Apr 09 19:37:03 Finished examples/xlrup_checker/array/compilation              1m02s   5GB
Apr 09 19:37:04 Starting examples/xlrup_checker/array/compilation/proofs
Apr 09 19:38:01 Finished examples/xlrup_checker/array/compilation/proofs         56s   5GB
Apr 09 19:38:02 Starting examples/pseudo_bool
Apr 09 19:39:34 Finished examples/pseudo_bool                                  1m31s   2GB
Apr 09 19:39:35 Starting examples/pseudo_bool/cnf_encoding
Apr 09 19:40:05 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Apr 09 19:40:06 Starting examples/pseudo_bool/graph_encoding
Apr 09 19:40:52 Finished examples/pseudo_bool/graph_encoding                     45s   2GB
Apr 09 19:40:53 Starting examples/pseudo_bool/array
Apr 09 20:50:07 Finished examples/pseudo_bool/array                         1h09m13s  42GB
Apr 09 20:50:08 Starting examples/pseudo_bool/array/compilation
Apr 09 21:00:03 Finished examples/pseudo_bool/array/compilation                9m53s  19GB
Apr 09 21:00:03 Starting examples/pseudo_bool/array/compilation/proofs
Apr 09 21:02:39 Finished examples/pseudo_bool/array/compilation/proofs         2m34s   6GB
Apr 09 21:02:40 Starting examples/pseudo_bool/array/compilation/proofsARM8
Apr 09 21:03:55 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m14s   6GB
Apr 09 21:03:56 Starting examples/opentheory
Apr 09 21:12:20 Finished examples/opentheory                                   8m23s   5GB
Apr 09 21:12:21 Starting examples/opentheory/compilation
Apr 09 21:13:54 Finished examples/opentheory/compilation                       1m31s   6GB
Apr 09 21:13:55 Starting examples/opentheory/compilation/proofs
Apr 09 21:14:55 Finished examples/opentheory/compilation/proofs                  59s   4GB
Apr 09 21:14:56 Starting examples/opentheory/compilation/ag32
Apr 09 21:16:33 Finished examples/opentheory/compilation/ag32                  1m35s   6GB
Apr 09 21:16:34 Starting examples/opentheory/compilation/ag32/proofs
Apr 09 21:18:11 Finished examples/opentheory/compilation/ag32/proofs           1m35s   8GB
Apr 09 21:18:12 Starting examples/sat_encodings
Apr 09 21:19:11 Finished examples/sat_encodings                                  58s 845MB
Apr 09 21:19:12 Starting examples/sat_encodings/demo
Apr 09 21:19:13 Finished examples/sat_encodings/demo                              0s  12MB
Apr 09 21:19:14 Starting examples/sat_encodings/case_studies
Apr 09 21:21:00 Finished examples/sat_encodings/case_studies                   1m44s   1GB
Apr 09 21:21:01 Starting examples/sat_encodings/translation
Apr 09 21:24:33 Finished examples/sat_encodings/translation                    3m31s   4GB
Apr 09 21:24:34 Starting examples/sat_encodings/translation/compilation
Apr 09 21:26:28 Finished examples/sat_encodings/translation/compilation        1m53s   4GB
Apr 09 21:26:29 Starting examples/deflate
Apr 09 21:26:57 Finished examples/deflate                                        26s 750MB
Apr 09 21:26:58 Starting examples/deflate/translation
Apr 09 21:28:04 Finished examples/deflate/translation                          1m04s   4GB
Apr 09 21:28:04 Starting examples/deflate/translation/compilation
Apr 09 21:28:56 Finished examples/deflate/translation/compilation                50s   3GB
Apr 09 21:28:57 Starting examples/vipr
Apr 09 21:32:33 Finished examples/vipr                                         3m35s   7GB
Apr 09 21:32:34 Starting examples/vipr/compilation
Apr 09 21:33:30 Finished examples/vipr/compilation                               55s   4GB
Apr 09 21:33:31 Starting translator/okasaki-examples
Apr 09 21:37:32 Finished translator/okasaki-examples                           3m59s   3GB
Apr 09 21:37:33 Starting translator/other-examples
Apr 09 21:38:25 Finished translator/other-examples                               50s   3GB
Apr 09 21:38:25 Starting translator/other-examples/auxiliary
Apr 09 21:38:26 Finished translator/other-examples/auxiliary                      0s  14MB
Apr 09 21:38:27 Starting compiler/parsing/tests
Apr 09 21:39:03 Finished compiler/parsing/tests                                  34s   1GB
Apr 09 21:39:03 Starting compiler/inference/tests
Apr 09 21:39:39 Finished compiler/inference/tests                                34s   2GB
Apr 09 21:39:40 Starting compiler/printing/test
Apr 09 21:40:52 Finished compiler/printing/test                                1m11s   5GB
Apr 09 21:40:53 Starting icing/flover
Apr 09 22:15:07 Finished icing/flover                                         34m12s   2GB
Apr 09 22:15:07 Starting icing/flover/Infra
Apr 09 22:15:08 Finished icing/flover/Infra                                       0s  13MB
Apr 09 22:15:09 Starting icing/flover/semantics
Apr 09 22:15:10 Finished icing/flover/semantics                                   0s  15MB
Apr 09 22:15:11 Starting icing/
Apr 09 22:42:06 Finished icing/                                               26m53s   7GB
Apr 09 22:42:07 Starting icing/examples
Apr 09 22:43:41 Finished icing/examples                                        1m33s   7GB
Apr 09 22:43:41 Starting compiler/repl
Apr 09 22:51:37 Finished compiler/repl                                         7m54s   7GB
Apr 09 22:51:37 Starting unverified/sexpr-bootstrap/x64/64
Apr 09 22:56:03 Finished unverified/sexpr-bootstrap/x64/64                     4m10s  18GB
Apr 09 22:56:03 Starting unverified/sexpr-bootstrap/x64/32
Apr 09 22:59:35 Finished unverified/sexpr-bootstrap/x64/32                     3m20s  15GB
Apr 09 22:59:36 Starting compiler/benchmarks
Apr 09 23:00:21 Finished compiler/benchmarks                                     44s 711MB
Apr 09 23:00:22 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Apr 09 23:00:26 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 259MB
Apr 09 23:00:26 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Apr 09 23:00:30 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 248MB
Apr 09 23:00:31 Starting compiler/bootstrap/compilation/x64/64
Apr 09 23:28:02 Finished compiler/bootstrap/compilation/x64/64                27m19s 106GB
Apr 09 23:28:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 09 23:52:11 Finished compiler/bootstrap/compilation/x64/64/proofs         24m06s  53GB
Apr 09 23:52:12 Starting compiler/bootstrap/compilation/x64/32
Apr 10 00:20:50 Finished compiler/bootstrap/compilation/x64/32                28m30s  80GB
Apr 10 00:20:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 10 00:25:00 Finished compiler/bootstrap/compilation/x64/32/proofs          4m07s  22GB
Apr 10 00:25:01 Starting compiler/bootstrap/compilation/arm8/64
Apr 10 01:05:34 Finished compiler/bootstrap/compilation/arm8/64               40m24s 104GB
Apr 10 01:05:35 Starting compiler/bootstrap/compilation/arm8/64/proofs
Apr 10 01:10:44 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m08s  30GB
Apr 10 01:10:45 Starting compiler/bootstrap/compilation/ag32/32
Apr 10 01:41:30 Finished compiler/bootstrap/compilation/ag32/32               30m43s  92GB
Apr 10 01:41:31 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 10 01:46:14 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m42s  30GB
Apr 10 01:46:15 SUCCESS