Job 2564

CakeML:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:257a82233211da227f76888bb05d6fce7c91769c
  Remove some unused code [Aug 20 04:07:40]
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

Aug 21 14:28:48 Claimed job
Aug 21 14:28:53 Building HOL
Aug 21 14:43:26 Starting developers
Aug 21 14:43:29 Finished developers                                               2s 236MB
Aug 21 14:43:30 Starting developers/bin
Aug 21 14:43:40 Finished developers/bin                                           9s   1GB
Aug 21 14:43:41 Starting compiler/proofs
Aug 21 16:38:51 Finished compiler/proofs                                    1h55m08s  26GB
Aug 21 16:38:52 Starting compiler/bootstrap/translation
Aug 22 01:25:35 Finished compiler/bootstrap/translation                     8h46m41s  73GB
Aug 22 01:25:36 Starting semantics/ffi
Aug 22 01:25:45 Finished semantics/ffi                                            7s 657MB
Aug 22 01:25:45 Starting semantics
Aug 22 01:25:47 Finished semantics                                                0s  68MB
Aug 22 01:25:48 Starting semantics/proofs
Aug 22 01:26:26 Finished semantics/proofs                                        37s   2GB
Aug 22 01:26:27 Starting semantics/alt_semantics
Aug 22 01:27:16 Finished semantics/alt_semantics                                 48s   1GB
Aug 22 01:27:17 Starting semantics/alt_semantics/proofs
Aug 22 01:38:25 Finished semantics/alt_semantics/proofs                       11m07s   2GB
Aug 22 01:38:26 Starting basis/pure
Aug 22 01:38:27 Finished basis/pure                                               0s  77MB
Aug 22 01:38:28 Starting translator
Aug 22 01:40:18 Finished translator                                            1m48s   4GB
Aug 22 01:40:19 Starting compiler/parsing
Aug 22 01:40:20 Finished compiler/parsing                                         0s  72MB
Aug 22 01:40:21 Starting characteristic
Aug 22 01:40:22 Finished characteristic                                           0s  93MB
Aug 22 01:40:23 Starting translator/monadic
Aug 22 01:40:25 Finished translator/monadic                                       0s 102MB
Aug 22 01:40:26 Starting basis
Aug 22 01:44:03 Finished basis                                                 3m36s   5GB
Aug 22 01:44:04 Starting compiler/inference
Aug 22 01:44:05 Finished compiler/inference                                       0s  93MB
Aug 22 01:44:06 Starting compiler/backend/reg_alloc
Aug 22 01:44:07 Finished compiler/backend/reg_alloc                               0s  70MB
Aug 22 01:44:08 Starting compiler/backend/gc
Aug 22 01:44:10 Finished compiler/backend/gc                                      0s 140MB
Aug 22 01:44:11 Starting compiler/backend
Aug 22 01:44:32 Finished compiler/backend                                        19s   1GB
Aug 22 01:44:33 Starting compiler/encoders/asm
Aug 22 01:44:34 Finished compiler/encoders/asm                                    0s  91MB
Aug 22 01:44:35 Starting compiler/encoders/x64
Aug 22 01:44:37 Finished compiler/encoders/x64                                    0s  95MB
Aug 22 01:44:38 Starting compiler/encoders/arm7
Aug 22 01:44:39 Finished compiler/encoders/arm7                                   0s 103MB
Aug 22 01:44:40 Starting compiler/encoders/arm8
Aug 22 01:44:41 Finished compiler/encoders/arm8                                   0s 103MB
Aug 22 01:44:42 Starting compiler/encoders/arm8_asl
Aug 22 04:11:45 Finished compiler/encoders/arm8_asl                         2h27m02s  43GB
Aug 22 04:11:46 Starting compiler/encoders/mips
Aug 22 04:11:48 Finished compiler/encoders/mips                                   0s 104MB
Aug 22 04:11:49 Starting compiler/encoders/riscv
Aug 22 04:11:51 Finished compiler/encoders/riscv                                  0s 103MB
Aug 22 04:11:51 Starting compiler/encoders/ag32
Aug 22 04:11:53 Finished compiler/encoders/ag32                                   0s  95MB
Aug 22 04:11:54 Starting compiler/backend/x64
Aug 22 04:11:56 Finished compiler/backend/x64                                     0s 138MB
Aug 22 04:11:57 Starting compiler/backend/arm7
Aug 22 04:11:58 Finished compiler/backend/arm7                                    0s 145MB
Aug 22 04:11:59 Starting compiler/backend/arm8
Aug 22 04:12:01 Finished compiler/backend/arm8                                    0s 145MB
Aug 22 04:12:02 Starting compiler/backend/mips
Aug 22 04:12:04 Finished compiler/backend/mips                                    0s 143MB
Aug 22 04:12:05 Starting compiler/backend/riscv
Aug 22 04:12:07 Finished compiler/backend/riscv                                   0s 143MB
Aug 22 04:12:07 Starting compiler/backend/ag32
Aug 22 04:13:28 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 22 04:13:29 Starting compiler/parsing/proofs
Aug 22 04:13:30 Finished compiler/parsing/proofs                                  0s  74MB
Aug 22 04:13:31 Starting compiler/inference/proofs
Aug 22 04:13:32 Finished compiler/inference/proofs                                0s 101MB
Aug 22 04:13:33 Starting compiler/backend/semantics
Aug 22 04:17:24 Finished compiler/backend/semantics                            3m49s   4GB
Aug 22 04:17:25 Starting compiler/backend/reg_alloc/proofs
Aug 22 04:17:26 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
Aug 22 04:17:27 Starting compiler/backend/proofs
Aug 22 04:18:32 Finished compiler/backend/proofs                               1m03s   3GB
Aug 22 04:18:33 Starting compiler/backend/serialiser
Aug 22 04:18:35 Finished compiler/backend/serialiser                              0s 149MB
Aug 22 04:18:36 Starting compiler/encoders/x64/proofs
Aug 22 04:27:57 Finished compiler/encoders/x64/proofs                          9m19s   5GB
Aug 22 04:27:58 Starting compiler/encoders/arm7/proofs
Aug 22 04:40:47 Finished compiler/encoders/arm7/proofs                        12m48s   8GB
Aug 22 04:40:48 Starting compiler/encoders/arm8/proofs
Aug 22 04:47:36 Finished compiler/encoders/arm8/proofs                         6m47s   4GB
Aug 22 04:47:37 Starting compiler/encoders/arm8_asl/proofs
Aug 22 05:35:11 Finished compiler/encoders/arm8_asl/proofs                    47m32s  11GB
Aug 22 05:35:11 Starting compiler/encoders/mips/proofs
Aug 22 05:45:23 Finished compiler/encoders/mips/proofs                        10m10s  10GB
Aug 22 05:45:24 Starting compiler/encoders/riscv/proofs
Aug 22 05:53:44 Finished compiler/encoders/riscv/proofs                        8m18s   5GB
Aug 22 05:53:45 Starting compiler/encoders/ag32/proofs
Aug 22 05:56:09 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Aug 22 05:56:09 Starting compiler/backend/x64/proofs
Aug 22 05:56:55 Finished compiler/backend/x64/proofs                             44s   3GB
Aug 22 05:56:56 Starting compiler/backend/arm7/proofs
Aug 22 05:57:42 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 22 05:57:43 Starting compiler/backend/arm8/proofs
Aug 22 05:58:26 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 22 05:58:26 Starting compiler/backend/arm8_asl
Aug 22 05:58:55 Finished compiler/backend/arm8_asl                               27s   2GB
Aug 22 05:58:56 Starting compiler/backend/mips/proofs
Aug 22 05:59:44 Finished compiler/backend/mips/proofs                            47s   3GB
Aug 22 05:59:45 Starting compiler/backend/riscv/proofs
Aug 22 06:00:37 Finished compiler/backend/riscv/proofs                           51s   4GB
Aug 22 06:00:38 Starting compiler/backend/ag32/proofs
Aug 22 06:14:53 Finished compiler/backend/ag32/proofs                         14m13s   6GB
Aug 22 06:14:54 Starting compiler/backend/cv_compute
Aug 22 06:16:41 Finished compiler/backend/cv_compute                           1m46s   3GB
Aug 22 06:16:42 Starting cv_translator
Aug 22 06:36:21 Finished cv_translator                                        19m37s  10GB
Aug 22 06:36:22 Starting candle/set-theory
Aug 22 06:37:13 Finished candle/set-theory                                       50s   1GB
Aug 22 06:37:14 Starting candle/syntax-lib
Aug 22 06:37:15 Finished candle/syntax-lib                                        0s  73MB
Aug 22 06:37:16 Starting candle/standard/syntax
Aug 22 06:37:35 Finished candle/standard/syntax                                  17s   1GB
Aug 22 06:37:36 Starting candle/standard/semantics
Aug 22 06:40:18 Finished candle/standard/semantics                             2m41s   3GB
Aug 22 06:40:19 Starting candle/standard/monadic
Aug 22 06:40:21 Finished candle/standard/monadic                                  0s 108MB
Aug 22 06:40:22 Starting candle/standard/ml_kernel
Aug 22 06:42:23 Finished candle/standard/ml_kernel                             2m00s   4GB
Aug 22 06:42:24 Starting candle/overloading/syntax
Aug 22 06:46:07 Finished candle/overloading/syntax                             3m41s   2GB
Aug 22 06:46:08 Starting candle/overloading/semantics
Aug 22 06:57:55 Finished candle/overloading/semantics                         11m46s  11GB
Aug 22 06:57:56 Starting candle/overloading/monadic
Aug 22 07:00:34 Finished candle/overloading/monadic                            2m36s   2GB
Aug 22 07:00:35 Starting candle/overloading/ml_kernel
Aug 22 07:08:26 Finished candle/overloading/ml_kernel                          7m50s   6GB
Aug 22 07:08:27 Starting candle/overloading/ml_checker
Aug 22 07:11:09 Finished candle/overloading/ml_checker                         2m40s   7GB
Aug 22 07:11:10 Starting candle/prover
Aug 22 07:21:36 Finished candle/prover                                        10m25s   5GB
Aug 22 07:21:36 Starting pancake
Aug 22 07:22:46 Finished pancake                                               1m08s   1GB
Aug 22 07:22:46 Starting pancake/ffi
Aug 22 07:22:47 Finished pancake/ffi                                              0s  24MB
Aug 22 07:22:48 Starting pancake/semantics
Aug 22 07:25:32 Finished pancake/semantics                                     2m42s   2GB
Aug 22 07:25:32 Starting pancake/parser
Aug 22 07:26:09 Finished pancake/parser                                          35s   2GB
Aug 22 07:26:10 Starting pancake/proofs
Aug 22 07:41:58 Finished pancake/proofs                                       15m46s   8GB
Aug 22 07:41:59 Starting characteristic/examples
Aug 22 07:43:39 Finished characteristic/examples                               1m39s   6GB
Aug 22 07:43:40 Starting tutorial/solutions
Aug 22 07:46:25 Finished tutorial/solutions                                    2m44s   6GB
Aug 22 07:46:26 Starting translator/monadic/examples
Aug 22 07:50:27 Finished translator/monadic/examples                           3m59s   5GB
Aug 22 07:50:27 Starting examples
Aug 22 08:05:32 Finished examples                                             15m03s   8GB
Aug 22 08:05:33 Starting examples/compilation/x64
Aug 22 08:15:12 Finished examples/compilation/x64                              9m38s   7GB
Aug 22 08:15:13 Starting examples/compilation/x64/proofs
Aug 22 08:19:56 Finished examples/compilation/x64/proofs                       4m41s   9GB
Aug 22 08:19:57 Starting examples/compilation/ag32
Aug 22 08:22:45 Finished examples/compilation/ag32                             2m47s   5GB
Aug 22 08:22:46 Starting examples/compilation/ag32/proofs
Aug 22 08:24:42 Finished examples/compilation/ag32/proofs                      1m55s   8GB
Aug 22 08:24:43 Starting examples/compilation/to_word
Aug 22 08:28:48 Finished examples/compilation/to_word                          4m03s  13GB
Aug 22 08:28:48 Starting examples/lpr_checker
Aug 22 08:30:13 Finished examples/lpr_checker                                  1m23s   2GB
Aug 22 08:30:14 Starting examples/lpr_checker/array
Aug 22 08:59:29 Finished examples/lpr_checker/array                           29m14s  10GB
Aug 22 08:59:30 Starting examples/lpr_checker/array/compilation
Aug 22 09:02:04 Finished examples/lpr_checker/array/compilation                2m32s   9GB
Aug 22 09:02:05 Starting examples/lpr_checker/array/compilation/proofs
Aug 22 09:03:59 Finished examples/lpr_checker/array/compilation/proofs         1m53s   8GB
Aug 22 09:04:00 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 22 09:05:53 Finished examples/lpr_checker/array/compilation/proofsARM8     1m52s   8GB
Aug 22 09:05:54 Starting examples/xlrup_checker
Aug 22 09:07:12 Finished examples/xlrup_checker                                1m16s   2GB
Aug 22 09:07:13 Starting examples/xlrup_checker/array
Aug 22 09:23:07 Finished examples/xlrup_checker/array                         15m53s   7GB
Aug 22 09:23:08 Starting examples/xlrup_checker/array/compilation
Aug 22 09:24:35 Finished examples/xlrup_checker/array/compilation              1m26s   6GB
Aug 22 09:24:36 Starting examples/xlrup_checker/array/compilation/proofs
Aug 22 09:26:19 Finished examples/xlrup_checker/array/compilation/proofs       1m41s   7GB
Aug 22 09:26:20 Starting examples/pseudo_bool
Aug 22 09:28:31 Finished examples/pseudo_bool                                  2m10s   2GB
Aug 22 09:28:32 Starting examples/pseudo_bool/cnf_encoding
Aug 22 09:29:13 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Aug 22 09:29:14 Starting examples/pseudo_bool/graph_encoding
Aug 22 09:30:07 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Aug 22 09:30:08 Starting examples/pseudo_bool/array
Aug 22 10:37:40 Finished examples/pseudo_bool/array                         1h07m30s  39GB
Aug 22 10:37:41 Starting examples/pseudo_bool/array/compilation
Aug 22 10:51:05 Finished examples/pseudo_bool/array/compilation               13m23s  30GB
Aug 22 10:51:06 Starting examples/pseudo_bool/array/compilation/proofs
Aug 22 10:55:03 Finished examples/pseudo_bool/array/compilation/proofs         3m56s  10GB
Aug 22 10:55:04 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 22 10:56:54 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m49s  10GB
Aug 22 10:56:55 Starting examples/opentheory
Aug 22 11:07:52 Finished examples/opentheory                                  10m55s   7GB
Aug 22 11:07:52 Starting examples/opentheory
Aug 22 11:07:54 Finished examples/opentheory                                      0s 137MB
Aug 22 11:07:55 Starting examples/opentheory/compilation
Aug 22 11:10:07 Finished examples/opentheory/compilation                       2m11s   6GB
Aug 22 11:10:08 Starting examples/opentheory/compilation/proofs
Aug 22 11:11:49 Finished examples/opentheory/compilation/proofs                1m40s   8GB
Aug 22 11:11:50 Starting examples/opentheory/compilation/ag32
Aug 22 11:14:00 Finished examples/opentheory/compilation/ag32                  2m08s   9GB
Aug 22 11:14:01 Starting examples/opentheory/compilation/ag32/proofs
Aug 22 11:16:21 Finished examples/opentheory/compilation/ag32/proofs           2m19s  12GB
Aug 22 11:16:22 Starting examples/sat_encodings
Aug 22 11:19:18 Finished examples/sat_encodings                                2m54s   1GB
Aug 22 11:19:18 Starting examples/sat_encodings/case_studies
Aug 22 11:21:24 Finished examples/sat_encodings/case_studies                   2m04s   2GB
Aug 22 11:21:25 Starting examples/sat_encodings/translation
Aug 22 11:27:52 Finished examples/sat_encodings/translation                    6m26s   7GB
Aug 22 11:27:53 Starting examples/sat_encodings/translation/compilation
Aug 22 11:30:18 Finished examples/sat_encodings/translation/compilation        2m24s   7GB
Aug 22 11:30:19 Starting examples/deflate
Aug 22 11:31:43 Finished examples/deflate                                      1m22s   1GB
Aug 22 11:31:44 Starting examples/deflate/translation
Aug 22 11:33:31 Finished examples/deflate/translation                          1m45s   7GB
Aug 22 11:33:32 Starting examples/deflate/translation/compilation
Aug 22 11:34:38 Finished examples/deflate/translation/compilation              1m05s   5GB
Aug 22 11:34:39 Starting examples/vipr
Aug 22 11:38:54 Finished examples/vipr                                         4m14s   8GB
Aug 22 11:38:55 Starting examples/vipr/compilation
Aug 22 11:40:14 Finished examples/vipr/compilation                             1m18s   6GB
Aug 22 11:40:15 Starting translator/okasaki-examples
Aug 22 11:45:26 Finished translator/okasaki-examples                           5m09s   4GB
Aug 22 11:45:27 Starting translator/other-examples
Aug 22 11:50:34 Finished translator/other-examples                             5m06s   3GB
Aug 22 11:50:34 Starting compiler/parsing/tests
Aug 22 11:51:13 Finished compiler/parsing/tests                                  37s   1GB
Aug 22 11:51:13 Starting compiler/inference/tests
Aug 22 11:51:58 Finished compiler/inference/tests                                44s   3GB
Aug 22 11:51:59 Starting compiler/printing/test
Aug 22 11:53:35 Finished compiler/printing/test                                1m34s   6GB
Aug 22 11:53:36 Starting icing/flover
Aug 22 12:30:21 Finished icing/flover                                         36m44s   4GB
Aug 22 12:30:22 Starting icing/
Aug 22 12:58:02 Finished icing/                                               27m39s   6GB
Aug 22 12:58:03 Starting icing/examples
Aug 22 12:59:55 Finished icing/examples                                        1m51s   9GB
Aug 22 12:59:56 Starting compiler/repl
Aug 22 13:08:58 Finished compiler/repl                                         9m01s   9GB
Aug 22 13:08:59 Starting unverified/sexpr-bootstrap/x64/64
Aug 22 13:22:34 Finished unverified/sexpr-bootstrap/x64/64                    13m09s  17GB
Aug 22 13:22:35 Starting unverified/sexpr-bootstrap/x64/32
Aug 22 13:33:20 Finished unverified/sexpr-bootstrap/x64/32                    10m25s  14GB
Aug 22 13:33:20 Starting compiler/benchmarks
Aug 22 13:34:05 Finished compiler/benchmarks                                     43s 713MB
Aug 22 13:34:06 Starting compiler/bootstrap/compilation/x64/64
Aug 22 14:15:04 Finished compiler/bootstrap/compilation/x64/64                40m45s 102GB
Aug 22 14:15:05 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 22 14:38:51 Finished compiler/bootstrap/compilation/x64/64/proofs         23m44s  49GB
Aug 22 14:38:52 Starting compiler/bootstrap/compilation/x64/32
Aug 22 15:17:17 Finished compiler/bootstrap/compilation/x64/32                38m17s 100GB
Aug 22 15:17:18 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 22 15:22:04 Finished compiler/bootstrap/compilation/x64/32/proofs          4m44s  27GB
Aug 22 15:22:05 Starting compiler/bootstrap/compilation/arm8/64
Aug 22 16:18:32 Finished compiler/bootstrap/compilation/arm8/64               56m18s 139GB
Aug 22 16:18:33 Starting compiler/bootstrap/compilation/arm8/64/proofs
Aug 22 16:24:19 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m44s  30GB
Aug 22 16:24:20 Starting compiler/bootstrap/compilation/ag32/32
Aug 22 17:03:17 Finished compiler/bootstrap/compilation/ag32/32               38m56s 104GB
Aug 22 17:03:18 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 22 17:08:39 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m20s  29GB
Aug 22 17:08:40 SUCCESS