Job 2826

CakeML:a2057e6cc146098766fa1fb9bf9e62a067d6cfda
  pancake/crep_arith: simplify constant multiplies [May 05 13:07:03]
#1169 (talsewell:pan-const-multiply)
Merging into:421f54d7feabd143e522e58d881f9e23c63bf934
  Merge pull request #1175 from CakeML/mcandidate-fix [May 10 11:20:24]
HOL:725300ce5d22e30174177682d5870306852113d5
  Apply a patch to lem_relation before Holmake runs [May 09 00:00:24]
Machine:lammmington

May 12 12:38:05 Claimed job
May 12 12:38:12 Reusing HOL
May 12 12:38:23 Starting developers
May 12 12:38:27 Finished developers                                               3s 202MB
May 12 12:38:28 Starting developers/bin
May 12 12:38:32 Finished developers/bin                                           3s 592MB
May 12 12:38:33 Starting misc
May 12 12:39:15 Finished misc                                                    40s   2GB
May 12 12:39:16 Starting compiler/proofs
May 12 14:17:03 Finished compiler/proofs                                    1h37m44s  40GB
May 12 14:17:04 Starting compiler/bootstrap/translation
May 12 20:00:10 Finished compiler/bootstrap/translation                     5h43m04s 102GB
May 12 20:00:11 Starting semantics/ffi
May 12 20:00:20 Finished semantics/ffi                                            8s 548MB
May 12 20:00:21 Starting semantics
May 12 20:00:22 Finished semantics                                                0s  51MB
May 12 20:00:23 Starting semantics/proofs
May 12 20:00:47 Finished semantics/proofs                                        22s 704MB
May 12 20:00:48 Starting semantics/alt_semantics
May 12 20:01:08 Finished semantics/alt_semantics                                 19s 684MB
May 12 20:01:09 Starting semantics/alt_semantics/proofs
May 12 20:11:18 Finished semantics/alt_semantics/proofs                       10m08s   2GB
May 12 20:11:19 Starting basis/pure
May 12 20:11:21 Finished basis/pure                                               0s  91MB
May 12 20:11:22 Starting translator
May 12 20:12:56 Finished translator                                            1m33s   3GB
May 12 20:12:57 Starting compiler/parsing
May 12 20:12:58 Finished compiler/parsing                                         0s  62MB
May 12 20:12:59 Starting characteristic
May 12 20:13:01 Finished characteristic                                           1s 118MB
May 12 20:13:02 Starting translator/monadic
May 12 20:13:04 Finished translator/monadic                                       1s 113MB
May 12 20:13:05 Starting translator/monadic/monad_base
May 12 20:13:06 Finished translator/monadic/monad_base                            0s  57MB
May 12 20:13:07 Starting basis
May 12 20:15:31 Finished basis                                                 2m22s   3GB
May 12 20:15:32 Starting compiler
May 12 20:15:34 Finished compiler                                                 1s 210MB
May 12 20:15:35 Starting compiler/inference
May 12 20:15:37 Finished compiler/inference                                       1s 113MB
May 12 20:15:38 Starting compiler/backend/reg_alloc
May 12 20:15:40 Finished compiler/backend/reg_alloc                               0s  56MB
May 12 20:15:41 Starting compiler/backend/gc
May 12 20:15:43 Finished compiler/backend/gc                                      1s 134MB
May 12 20:15:44 Starting compiler/backend
May 12 20:15:49 Finished compiler/backend                                         4s 233MB
May 12 20:15:49 Starting compiler/encoders/asm
May 12 20:15:51 Finished compiler/encoders/asm                                    0s  85MB
May 12 20:15:52 Starting compiler/encoders/x64
May 12 20:15:54 Finished compiler/encoders/x64                                    0s  86MB
May 12 20:15:55 Starting compiler/encoders/arm7
May 12 20:15:56 Finished compiler/encoders/arm7                                   0s  83MB
May 12 20:15:57 Starting compiler/encoders/arm8
May 12 20:15:59 Finished compiler/encoders/arm8                                   0s  84MB
May 12 20:16:00 Starting compiler/encoders/arm8_asl
May 12 22:19:00 Finished compiler/encoders/arm8_asl                         2h02m59s  44GB
May 12 22:19:01 Starting compiler/encoders/mips
May 12 22:19:02 Finished compiler/encoders/mips                                   0s  84MB
May 12 22:19:03 Starting compiler/encoders/riscv
May 12 22:19:05 Finished compiler/encoders/riscv                                  0s  83MB
May 12 22:19:06 Starting compiler/encoders/ag32
May 12 22:19:07 Finished compiler/encoders/ag32                                   0s  82MB
May 12 22:19:08 Starting compiler/encoders/tests
May 12 22:19:10 Finished compiler/encoders/tests                                  0s 107MB
May 12 22:19:11 Starting compiler/encoders/monadic_enc
May 12 22:19:13 Finished compiler/encoders/monadic_enc                            1s 132MB
May 12 22:19:14 Starting compiler/backend/x64
May 12 22:19:16 Finished compiler/backend/x64                                     1s 134MB
May 12 22:19:17 Starting compiler/backend/arm7
May 12 22:19:19 Finished compiler/backend/arm7                                    1s 133MB
May 12 22:19:20 Starting compiler/backend/arm8
May 12 22:19:22 Finished compiler/backend/arm8                                    1s 133MB
May 12 22:19:23 Starting compiler/backend/mips
May 12 22:19:25 Finished compiler/backend/mips                                    1s 133MB
May 12 22:19:26 Starting compiler/backend/riscv
May 12 22:19:28 Finished compiler/backend/riscv                                   1s 126MB
May 12 22:19:29 Starting compiler/backend/ag32
May 12 22:20:34 Finished compiler/backend/ag32                                 1m03s   2GB
May 12 22:20:35 Starting compiler/backend/pattern_matching
May 12 22:20:36 Finished compiler/backend/pattern_matching                        0s  54MB
May 12 22:20:37 Starting compiler/parsing/ocaml
May 12 22:22:18 Finished compiler/parsing/ocaml                                1m40s   1GB
May 12 22:22:19 Starting compiler/printing
May 12 22:22:21 Finished compiler/printing                                        1s 112MB
May 12 22:22:22 Starting compiler/parsing/proofs
May 12 22:22:24 Finished compiler/parsing/proofs                                  0s  63MB
May 12 22:22:25 Starting compiler/inference/proofs
May 12 22:22:27 Finished compiler/inference/proofs                                1s 107MB
May 12 22:22:28 Starting compiler/backend/semantics
May 12 22:25:29 Finished compiler/backend/semantics                            3m00s   2GB
May 12 22:25:30 Starting compiler/backend/reg_alloc/proofs
May 12 22:25:32 Finished compiler/backend/reg_alloc/proofs                        1s 115MB
May 12 22:25:33 Starting compiler/backend/proofs
May 12 22:26:21 Finished compiler/backend/proofs                                 47s   4GB
May 12 22:26:22 Starting compiler/backend/serialiser
May 12 22:26:24 Finished compiler/backend/serialiser                              1s 148MB
May 12 22:26:25 Starting compiler/encoders/x64/proofs
May 12 22:36:27 Finished compiler/encoders/x64/proofs                         10m00s   5GB
May 12 22:36:28 Starting compiler/encoders/arm7/proofs
May 12 22:49:21 Finished compiler/encoders/arm7/proofs                        12m52s   5GB
May 12 22:49:22 Starting compiler/encoders/arm8/proofs
May 12 22:56:20 Finished compiler/encoders/arm8/proofs                         6m57s   4GB
May 12 22:56:21 Starting compiler/encoders/arm8_asl/proofs
May 12 23:45:39 Finished compiler/encoders/arm8_asl/proofs                    49m16s  20GB
May 12 23:45:40 Starting compiler/encoders/mips/proofs
May 12 23:55:44 Finished compiler/encoders/mips/proofs                        10m02s   6GB
May 12 23:55:45 Starting compiler/encoders/riscv/proofs
May 13 00:03:55 Finished compiler/encoders/riscv/proofs                        8m09s   3GB
May 13 00:03:56 Starting compiler/encoders/ag32/proofs
May 13 00:06:47 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
May 13 00:06:48 Starting compiler/backend/x64/proofs
May 13 00:07:16 Finished compiler/backend/x64/proofs                             27s   2GB
May 13 00:07:17 Starting compiler/backend/arm7/proofs
May 13 00:07:46 Finished compiler/backend/arm7/proofs                            27s   1GB
May 13 00:07:47 Starting compiler/backend/arm8/proofs
May 13 00:08:16 Finished compiler/backend/arm8/proofs                            28s   1GB
May 13 00:08:17 Starting compiler/backend/arm8_asl
May 13 00:08:39 Finished compiler/backend/arm8_asl                               20s   2GB
May 13 00:08:40 Starting compiler/backend/mips/proofs
May 13 00:09:11 Finished compiler/backend/mips/proofs                            30s   2GB
May 13 00:09:12 Starting compiler/backend/riscv/proofs
May 13 00:09:44 Finished compiler/backend/riscv/proofs                           31s   2GB
May 13 00:09:45 Starting compiler/backend/ag32/proofs
May 13 00:23:07 Finished compiler/backend/ag32/proofs                         13m21s   3GB
May 13 00:23:08 Starting compiler/backend/cv_compute
May 13 00:24:16 Finished compiler/backend/cv_compute                           1m06s   2GB
May 13 00:24:17 Starting cv_translator
May 13 00:44:21 Finished cv_translator                                        20m03s   8GB
May 13 00:44:22 Starting candle
May 13 00:44:23 Finished candle                                                   0s  12MB
May 13 00:44:24 Starting candle/set-theory
May 13 00:44:57 Finished candle/set-theory                                       31s   1GB
May 13 00:44:58 Starting candle/syntax-lib
May 13 00:44:59 Finished candle/syntax-lib                                        0s  94MB
May 13 00:45:00 Starting candle/standard
May 13 00:45:01 Finished candle/standard                                          0s  10MB
May 13 00:45:02 Starting candle/standard/syntax
May 13 00:45:14 Finished candle/standard/syntax                                  10s 737MB
May 13 00:45:14 Starting candle/standard/semantics
May 13 00:47:10 Finished candle/standard/semantics                             1m54s   2GB
May 13 00:47:11 Starting candle/standard/monadic
May 13 00:47:13 Finished candle/standard/monadic                                  1s 125MB
May 13 00:47:14 Starting candle/standard/ml_kernel
May 13 00:48:56 Finished candle/standard/ml_kernel                             1m41s   4GB
May 13 00:48:57 Starting candle/standard/ml_kernel/lisp
May 13 00:48:58 Finished candle/standard/ml_kernel/lisp                           0s  46MB
May 13 00:48:59 Starting candle/overloading
May 13 00:49:00 Finished candle/overloading                                       0s  11MB
May 13 00:49:01 Starting candle/overloading/syntax
May 13 00:52:02 Finished candle/overloading/syntax                             3m00s   1GB
May 13 00:52:03 Starting candle/overloading/semantics
May 13 01:02:53 Finished candle/overloading/semantics                         10m48s   3GB
May 13 01:02:54 Starting candle/overloading/monadic
May 13 01:05:09 Finished candle/overloading/monadic                            2m14s   2GB
May 13 01:05:10 Starting candle/overloading/ml_kernel
May 13 01:12:18 Finished candle/overloading/ml_kernel                          7m07s   5GB
May 13 01:12:19 Starting candle/overloading/ml_checker
May 13 01:14:28 Finished candle/overloading/ml_checker                         2m08s   6GB
May 13 01:14:29 Starting candle/prover
May 13 01:24:01 Finished candle/prover                                         9m30s   5GB
May 13 01:24:02 Starting candle/prover/compute
May 13 01:24:04 Finished candle/prover/compute                                    1s 140MB
May 13 01:24:05 Starting pancake
May 13 01:24:07 Finished pancake                                                  1s 137MB
May 13 01:24:08 Starting pancake/semantics
May 13 01:26:15 Finished pancake/semantics                                     2m06s   2GB
May 13 01:26:16 Starting pancake/parser
May 13 01:26:40 Finished pancake/parser                                          22s 428MB
May 13 01:26:41 Starting pancake/static_checker
May 13 01:27:17 Finished pancake/static_checker                                  35s   1GB
May 13 01:27:18 Starting pancake/proofs
May 13 01:42:57 Finished pancake/proofs                                       15m37s   7GB
May 13 01:42:57 Starting compiler/dafny
May 13 01:45:49 Finished compiler/dafny                                        2m50s  11GB
May 13 01:45:50 Starting compiler/dafny/translation
May 13 02:05:03 Finished compiler/dafny/translation                           19m11s  19GB
May 13 02:05:04 Starting compiler/dafny/compilation
May 13 02:08:04 Finished compiler/dafny/compilation                            2m59s  12GB
May 13 02:08:05 Starting compiler/dafny/semantics
May 13 02:08:41 Finished compiler/dafny/semantics                                35s   1GB
May 13 02:08:42 Starting characteristic/examples
May 13 02:10:07 Finished characteristic/examples                               1m24s   4GB
May 13 02:10:10 Starting tutorial/solutions
May 13 02:12:34 Finished tutorial/solutions                                    2m23s   3GB
May 13 02:12:35 Starting translator/monadic/examples
May 13 02:15:30 Finished translator/monadic/examples                           2m53s   3GB
May 13 02:15:31 Starting examples
May 13 02:21:30 Finished examples                                              5m57s   5GB
May 13 02:21:31 Starting examples/compilation
May 13 02:21:32 Finished examples/compilation                                     0s   9MB
May 13 02:21:34 Starting examples/compilation/x64
May 13 02:28:30 Finished examples/compilation/x64                              6m55s   4GB
May 13 02:28:31 Starting examples/compilation/x64/proofs
May 13 02:30:56 Finished examples/compilation/x64/proofs                       2m23s   4GB
May 13 02:30:57 Starting examples/compilation/ag32
May 13 02:32:54 Finished examples/compilation/ag32                             1m56s   3GB
May 13 02:32:55 Starting examples/compilation/ag32/proofs
May 13 02:33:56 Finished examples/compilation/ag32/proofs                      1m00s   5GB
May 13 02:33:57 Starting examples/lpr_checker
May 13 02:34:27 Finished examples/lpr_checker                                    29s   1GB
May 13 02:34:28 Starting examples/lpr_checker/array
May 13 03:00:48 Finished examples/lpr_checker/array                           26m18s  22GB
May 13 03:00:49 Starting examples/lpr_checker/array/compilation
May 13 03:03:11 Finished examples/lpr_checker/array/compilation                2m20s   7GB
May 13 03:03:13 Starting examples/lpr_checker/array/compilation/proofs
May 13 03:04:20 Finished examples/lpr_checker/array/compilation/proofs         1m06s   6GB
May 13 03:04:21 Starting examples/lpr_checker/array/compilation/proofsARM8
May 13 03:05:29 Finished examples/lpr_checker/array/compilation/proofsARM8     1m06s   6GB
May 13 03:05:29 Starting .
May 13 03:05:33 Finished .                                                        2s 298MB
May 13 03:05:34 Starting examples/xlrup_checker
May 13 03:06:08 Finished examples/xlrup_checker                                  32s   1GB
May 13 03:06:09 Starting examples/xlrup_checker/array
May 13 03:18:56 Finished examples/xlrup_checker/array                         12m46s   8GB
May 13 03:18:57 Starting examples/xlrup_checker/array/compilation
May 13 03:20:01 Finished examples/xlrup_checker/array/compilation              1m03s   4GB
May 13 03:20:03 Starting examples/xlrup_checker/array/compilation/proofs
May 13 03:21:01 Finished examples/xlrup_checker/array/compilation/proofs         57s   5GB
May 13 03:21:02 Starting examples/pseudo_bool
May 13 03:22:34 Finished examples/pseudo_bool                                  1m30s   2GB
May 13 03:22:35 Starting examples/pseudo_bool/cnf_encoding
May 13 03:23:03 Finished examples/pseudo_bool/cnf_encoding                       26s 986MB
May 13 03:23:03 Starting examples/pseudo_bool/graph_encoding
May 13 03:23:46 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
May 13 03:23:47 Starting examples/pseudo_bool/array
May 13 04:33:14 Finished examples/pseudo_bool/array                         1h09m26s  34GB
May 13 04:33:15 Starting examples/pseudo_bool/array/compilation
May 13 04:43:23 Finished examples/pseudo_bool/array/compilation               10m07s  19GB
May 13 04:43:24 Starting examples/pseudo_bool/array/compilation/proofs
May 13 04:45:57 Finished examples/pseudo_bool/array/compilation/proofs         2m32s   6GB
May 13 04:45:58 Starting examples/pseudo_bool/array/compilation/proofsARM8
May 13 04:47:12 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m12s   6GB
May 13 04:47:12 Starting examples/opentheory
May 13 04:55:40 Finished examples/opentheory                                   8m26s   5GB
May 13 04:55:41 Starting examples/opentheory/compilation
May 13 04:57:14 Finished examples/opentheory/compilation                       1m31s   6GB
May 13 04:57:15 Starting examples/opentheory/compilation/proofs
May 13 04:58:14 Finished examples/opentheory/compilation/proofs                  58s   4GB
May 13 04:58:15 Starting examples/opentheory/compilation/ag32
May 13 04:59:51 Finished examples/opentheory/compilation/ag32                  1m35s   6GB
May 13 04:59:52 Starting examples/opentheory/compilation/ag32/proofs
May 13 05:01:24 Finished examples/opentheory/compilation/ag32/proofs           1m31s   8GB
May 13 05:01:25 Starting examples/sat_encodings
May 13 05:02:25 Finished examples/sat_encodings                                  58s 778MB
May 13 05:02:26 Starting examples/sat_encodings/demo
May 13 05:02:26 Finished examples/sat_encodings/demo                              0s  11MB
May 13 05:02:27 Starting examples/sat_encodings/case_studies
May 13 05:04:10 Finished examples/sat_encodings/case_studies                   1m41s   1GB
May 13 05:04:11 Starting examples/sat_encodings/translation
May 13 05:07:45 Finished examples/sat_encodings/translation                    3m34s   5GB
May 13 05:07:46 Starting examples/sat_encodings/translation/compilation
May 13 05:09:40 Finished examples/sat_encodings/translation/compilation        1m52s   4GB
May 13 05:09:41 Starting examples/deflate
May 13 05:10:09 Finished examples/deflate                                        27s 711MB
May 13 05:10:10 Starting examples/deflate/translation
May 13 05:11:14 Finished examples/deflate/translation                          1m03s   4GB
May 13 05:11:15 Starting examples/deflate/translation/compilation
May 13 05:12:07 Finished examples/deflate/translation/compilation                50s   4GB
May 13 05:12:08 Starting examples/vipr
May 13 05:15:28 Finished examples/vipr                                         3m19s   7GB
May 13 05:15:29 Starting examples/vipr/compilation
May 13 05:16:25 Finished examples/vipr/compilation                               55s   4GB
May 13 05:16:26 Starting translator/okasaki-examples
May 13 05:20:29 Finished translator/okasaki-examples                           4m01s   3GB
May 13 05:20:30 Starting translator/other-examples
May 13 05:22:55 Finished translator/other-examples                             2m23s   2GB
May 13 05:22:56 Starting translator/other-examples/auxiliary
May 13 05:22:56 Finished translator/other-examples/auxiliary                      0s  13MB
May 13 05:22:57 Starting compiler/parsing/tests
May 13 05:23:32 Finished compiler/parsing/tests                                  33s   1GB
May 13 05:23:33 Starting compiler/inference/tests
May 13 05:24:09 Finished compiler/inference/tests                                35s   2GB
May 13 05:24:10 Starting compiler/printing/test
May 13 05:25:21 Finished compiler/printing/test                                1m10s   5GB
May 13 05:25:22 Starting icing/flover
May 13 05:57:36 Finished icing/flover                                         32m12s   2GB
May 13 05:57:37 Starting icing/flover/Infra
May 13 05:57:38 Finished icing/flover/Infra                                       0s  13MB
May 13 05:57:39 Starting icing/flover/semantics
May 13 05:57:40 Finished icing/flover/semantics                                   0s  15MB
May 13 05:57:41 Starting icing/
May 13 06:23:49 Finished icing/                                               26m07s   4GB
May 13 06:23:50 Starting icing/examples
May 13 06:25:15 Finished icing/examples                                        1m23s   7GB
May 13 06:25:16 Starting compiler/repl
May 13 06:33:02 Finished compiler/repl                                         7m45s   6GB
May 13 06:33:03 Starting unverified/sexpr-bootstrap/x64/64
May 13 06:36:40 Finished unverified/sexpr-bootstrap/x64/64                     3m36s  15GB
May 13 06:36:41 Starting unverified/sexpr-bootstrap/x64/32
May 13 06:40:09 Finished unverified/sexpr-bootstrap/x64/32                     3m26s  15GB
May 13 06:40:10 Starting compiler/benchmarks
May 13 06:40:55 Finished compiler/benchmarks                                     44s 711MB
May 13 06:40:56 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
May 13 06:41:00 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 249MB
May 13 06:41:00 Starting compiler/benchmarks/mlton_benchmarks/cakeml
May 13 06:41:04 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 246MB
May 13 06:41:05 Starting compiler/bootstrap/compilation/x64/64
May 13 07:10:22 Finished compiler/bootstrap/compilation/x64/64                29m16s  93GB
May 13 07:10:23 Starting compiler/bootstrap/compilation/x64/64/proofs
May 13 07:33:19 Finished compiler/bootstrap/compilation/x64/64/proofs         22m55s  42GB
May 13 07:33:20 Starting compiler/bootstrap/compilation/x64/32
May 13 08:01:37 Finished compiler/bootstrap/compilation/x64/32                28m16s  74GB
May 13 08:01:38 Starting compiler/bootstrap/compilation/x64/32/proofs
May 13 08:05:42 Finished compiler/bootstrap/compilation/x64/32/proofs          4m03s  23GB
May 13 08:05:43 Starting compiler/bootstrap/compilation/arm8/64
May 13 08:47:37 Finished compiler/bootstrap/compilation/arm8/64               41m52s 120GB
May 13 08:47:37 Starting compiler/bootstrap/compilation/arm8/64/proofs
May 13 08:53:16 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m37s  31GB
May 13 08:53:17 Starting compiler/bootstrap/compilation/ag32/32
May 13 09:22:53 Finished compiler/bootstrap/compilation/ag32/32               29m35s  91GB
May 13 09:22:54 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 13 09:28:27 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m32s  30GB
May 13 09:28:28 SUCCESS