Job 2215

CakeML:9e4e7ac308ba27e9be6e569d09722e83907577e2
  Merge pull request #972 from CakeML/byte [Sep 14 08:45:51]
HOL:cff397e71140a8738a9f5e402181bea4a19b9d29
  Add simp rule to eliminate tau's under weak bisimulation [Sep 05 04:19:31]
Machine:lammington
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Sep 14 09:04:59 Claimed job
Sep 14 09:05:03 Building HOL
Sep 14 09:19:48 Starting developers
Sep 14 09:19:52 Finished developers                                               2s 229MB
Sep 14 09:19:53 Starting developers/bin
Sep 14 09:20:03 Finished developers/bin                                           9s   1GB
Sep 14 09:20:04 Starting compiler/proofs
Sep 14 11:04:21 Finished compiler/proofs                                    1h44m16s  31GB
Sep 14 11:04:22 Starting compiler/bootstrap/translation
Sep 14 19:13:17 Finished compiler/bootstrap/translation                     8h08m54s  71GB
Sep 14 19:13:18 Starting semantics/ffi
Sep 14 19:13:26 Finished semantics/ffi                                            7s 582MB
Sep 14 19:13:27 Starting semantics
Sep 14 19:13:28 Finished semantics                                                0s  65MB
Sep 14 19:13:29 Starting semantics/proofs
Sep 14 19:14:04 Finished semantics/proofs                                        34s   2GB
Sep 14 19:14:05 Starting semantics/alt_semantics
Sep 14 19:14:43 Finished semantics/alt_semantics                                 36s   1GB
Sep 14 19:14:44 Starting semantics/alt_semantics/proofs
Sep 14 19:25:38 Finished semantics/alt_semantics/proofs                       10m52s   4GB
Sep 14 19:25:38 Starting basis/pure
Sep 14 19:25:40 Finished basis/pure                                               0s  73MB
Sep 14 19:25:40 Starting translator
Sep 14 19:27:25 Finished translator                                            1m43s   4GB
Sep 14 19:27:25 Starting compiler/parsing
Sep 14 19:27:27 Finished compiler/parsing                                         0s  70MB
Sep 14 19:27:27 Starting characteristic
Sep 14 19:27:29 Finished characteristic                                           0s  85MB
Sep 14 19:27:30 Starting translator/monadic
Sep 14 19:27:31 Finished translator/monadic                                       0s  98MB
Sep 14 19:27:32 Starting basis
Sep 14 19:31:28 Finished basis                                                 3m54s   5GB
Sep 14 19:31:29 Starting compiler/inference
Sep 14 19:31:30 Finished compiler/inference                                       0s  85MB
Sep 14 19:31:31 Starting compiler/backend/reg_alloc
Sep 14 19:31:32 Finished compiler/backend/reg_alloc                               0s  65MB
Sep 14 19:31:33 Starting compiler/backend/gc
Sep 14 19:31:34 Finished compiler/backend/gc                                      0s 138MB
Sep 14 19:31:35 Starting compiler/backend
Sep 14 19:31:52 Finished compiler/backend                                        16s   1GB
Sep 14 19:31:53 Starting compiler/encoders/asm
Sep 14 19:31:55 Finished compiler/encoders/asm                                    0s  91MB
Sep 14 19:31:55 Starting compiler/encoders/x64
Sep 14 19:31:57 Finished compiler/encoders/x64                                    0s  95MB
Sep 14 19:31:58 Starting compiler/encoders/arm7
Sep 14 19:31:59 Finished compiler/encoders/arm7                                   0s  94MB
Sep 14 19:32:00 Starting compiler/encoders/arm8
Sep 14 19:32:01 Finished compiler/encoders/arm8                                   0s  89MB
Sep 14 19:32:02 Starting compiler/encoders/arm8_asl
Sep 14 21:42:42 Finished compiler/encoders/arm8_asl                         2h10m38s  43GB
Sep 14 21:42:43 Starting compiler/encoders/mips
Sep 14 21:42:44 Finished compiler/encoders/mips                                   0s  89MB
Sep 14 21:42:45 Starting compiler/encoders/riscv
Sep 14 21:42:46 Finished compiler/encoders/riscv                                  0s  89MB
Sep 14 21:42:47 Starting compiler/encoders/ag32
Sep 14 21:42:48 Finished compiler/encoders/ag32                                   0s  84MB
Sep 14 21:42:49 Starting compiler/backend/x64
Sep 14 21:42:51 Finished compiler/backend/x64                                     0s 128MB
Sep 14 21:42:52 Starting compiler/backend/arm7
Sep 14 21:42:53 Finished compiler/backend/arm7                                    0s 128MB
Sep 14 21:42:54 Starting compiler/backend/arm8
Sep 14 21:42:56 Finished compiler/backend/arm8                                    0s 128MB
Sep 14 21:42:57 Starting compiler/backend/mips
Sep 14 21:42:58 Finished compiler/backend/mips                                    0s 128MB
Sep 14 21:42:59 Starting compiler/backend/riscv
Sep 14 21:43:01 Finished compiler/backend/riscv                                   0s 128MB
Sep 14 21:43:01 Starting compiler/backend/ag32
Sep 14 21:44:25 Finished compiler/backend/ag32                                 1m22s   4GB
Sep 14 21:44:26 Starting compiler/parsing/proofs
Sep 14 21:44:27 Finished compiler/parsing/proofs                                  0s  73MB
Sep 14 21:44:28 Starting compiler/inference/proofs
Sep 14 21:44:30 Finished compiler/inference/proofs                                0s  89MB
Sep 14 21:44:30 Starting compiler/backend/semantics
Sep 14 21:45:55 Finished compiler/backend/semantics                            1m23s   3GB
Sep 14 21:45:56 Starting compiler/backend/reg_alloc/proofs
Sep 14 21:45:57 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Sep 14 21:45:58 Starting compiler/backend/proofs
Sep 14 21:47:01 Finished compiler/backend/proofs                               1m02s   3GB
Sep 14 21:47:02 Starting compiler/backend/serialiser
Sep 14 21:47:04 Finished compiler/backend/serialiser                              1s 188MB
Sep 14 21:47:05 Starting compiler/encoders/x64/proofs
Sep 14 21:56:39 Finished compiler/encoders/x64/proofs                          9m33s   5GB
Sep 14 21:56:40 Starting compiler/encoders/arm7/proofs
Sep 14 22:09:31 Finished compiler/encoders/arm7/proofs                        12m50s  10GB
Sep 14 22:09:32 Starting compiler/encoders/arm8/proofs
Sep 14 22:16:02 Finished compiler/encoders/arm8/proofs                         6m29s   5GB
Sep 14 22:16:03 Starting compiler/encoders/arm8_asl/proofs
Sep 14 23:03:43 Finished compiler/encoders/arm8_asl/proofs                    47m38s  10GB
Sep 14 23:03:44 Starting compiler/encoders/mips/proofs
Sep 14 23:13:54 Finished compiler/encoders/mips/proofs                        10m09s   7GB
Sep 14 23:13:55 Starting compiler/encoders/riscv/proofs
Sep 14 23:22:09 Finished compiler/encoders/riscv/proofs                        8m13s   5GB
Sep 14 23:22:09 Starting compiler/encoders/ag32/proofs
Sep 14 23:24:36 Finished compiler/encoders/ag32/proofs                         2m25s   2GB
Sep 14 23:24:37 Starting compiler/backend/x64/proofs
Sep 14 23:25:16 Finished compiler/backend/x64/proofs                             38s   3GB
Sep 14 23:25:17 Starting compiler/backend/arm7/proofs
Sep 14 23:26:00 Finished compiler/backend/arm7/proofs                            42s   2GB
Sep 14 23:26:01 Starting compiler/backend/arm8/proofs
Sep 14 23:26:40 Finished compiler/backend/arm8/proofs                            38s   3GB
Sep 14 23:26:41 Starting compiler/backend/arm8_asl
Sep 14 23:27:10 Finished compiler/backend/arm8_asl                               27s   2GB
Sep 14 23:27:11 Starting compiler/backend/mips/proofs
Sep 14 23:27:54 Finished compiler/backend/mips/proofs                            42s   3GB
Sep 14 23:27:55 Starting compiler/backend/riscv/proofs
Sep 14 23:28:44 Finished compiler/backend/riscv/proofs                           48s   4GB
Sep 14 23:28:45 Starting compiler/backend/ag32/proofs
Sep 14 23:41:52 Finished compiler/backend/ag32/proofs                         13m06s   6GB
Sep 14 23:41:53 Starting candle/set-theory
Sep 14 23:42:35 Finished candle/set-theory                                       41s   1GB
Sep 14 23:42:36 Starting candle/syntax-lib
Sep 14 23:42:37 Finished candle/syntax-lib                                        0s  67MB
Sep 14 23:42:38 Starting candle/standard/syntax
Sep 14 23:42:54 Finished candle/standard/syntax                                  15s   1GB
Sep 14 23:42:55 Starting candle/standard/semantics
Sep 14 23:45:20 Finished candle/standard/semantics                             2m23s   2GB
Sep 14 23:45:20 Starting candle/standard/monadic
Sep 14 23:45:22 Finished candle/standard/monadic                                  0s 101MB
Sep 14 23:45:23 Starting candle/standard/ml_kernel
Sep 14 23:47:13 Finished candle/standard/ml_kernel                             1m49s   5GB
Sep 14 23:47:14 Starting candle/overloading/syntax
Sep 14 23:50:48 Finished candle/overloading/syntax                             3m33s   3GB
Sep 14 23:50:48 Starting candle/overloading/semantics
Sep 20 22:12:08 Resuming candle/overloading/semantics
Sep 20 22:12:09 Finished candle/overloading/semantics                             0s  86MB
Sep 20 22:12:10 Starting candle/overloading/monadic
Sep 20 22:14:41 Finished candle/overloading/monadic                            2m29s   2GB
Sep 20 22:14:42 Starting candle/overloading/ml_kernel
Sep 20 22:22:13 Finished candle/overloading/ml_kernel                          7m30s   6GB
Sep 20 22:22:14 Starting candle/overloading/ml_checker
Sep 20 22:24:46 Finished candle/overloading/ml_checker                         2m30s   6GB
Sep 20 22:24:47 Starting candle/prover
Sep 20 22:34:42 Finished candle/prover                                         9m53s   5GB
Sep 20 22:34:43 Starting pancake
Sep 20 22:35:43 Finished pancake                                                 59s   1GB
Sep 20 22:35:44 Starting pancake/ffi
Sep 20 22:35:45 Finished pancake/ffi                                              0s  20MB
Sep 20 22:35:46 Starting pancake/semantics
Sep 20 22:38:03 Finished pancake/semantics                                     2m16s   2GB
Sep 20 22:38:04 Starting pancake/parser
Sep 20 22:38:32 Finished pancake/parser                                          26s   2GB
Sep 20 22:38:33 Starting pancake/proofs
Sep 20 23:07:58 Finished pancake/proofs                                       29m24s   8GB
Sep 20 23:07:59 Starting characteristic/examples
Sep 20 23:09:33 Finished characteristic/examples                               1m32s   5GB
Sep 20 23:09:34 Starting tutorial/solutions
Sep 20 23:24:58 Finished tutorial/solutions                                   15m22s  10GB
Sep 20 23:24:59 Starting translator/monadic/examples
Sep 20 23:28:40 Finished translator/monadic/examples                           3m39s   5GB
Sep 20 23:28:41 Starting examples
Sep 20 23:43:10 Finished examples                                             14m28s   7GB
Sep 20 23:43:11 Starting examples/compilation/x64
Sep 21 01:40:09 Finished examples/compilation/x64                           1h56m57s  39GB
Sep 21 01:40:10 Starting examples/compilation/x64/proofs
Sep 21 01:43:59 Finished examples/compilation/x64/proofs                       3m47s   6GB
Sep 21 01:44:00 Starting examples/compilation/ag32
Sep 21 02:13:46 Finished examples/compilation/ag32                            29m44s   9GB
Sep 21 02:13:47 Starting examples/compilation/ag32/proofs
Sep 21 02:15:16 Finished examples/compilation/ag32/proofs                      1m28s   7GB
Sep 21 02:15:17 Starting examples/compilation/to_word
Sep 21 02:19:03 Finished examples/compilation/to_word                          3m45s  11GB
Sep 21 02:19:04 Starting examples/lpr_checker
Sep 21 02:20:19 Finished examples/lpr_checker                                  1m13s   2GB
Sep 21 02:20:20 Starting examples/lpr_checker/array
Sep 21 02:54:59 Finished examples/lpr_checker/array                           34m38s   8GB
Sep 21 02:54:59 Starting examples/lpr_checker/array/compilation
Sep 21 03:29:01 Finished examples/lpr_checker/array/compilation               33m59s  50GB
Sep 21 03:29:01 Starting examples/lpr_checker/array/compilation/proofs
Sep 21 03:30:53 Finished examples/lpr_checker/array/compilation/proofs         1m50s  10GB
Sep 21 03:30:54 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 21 03:56:03 Finished examples/lpr_checker/array/compilation/proofsARM8    25m08s  38GB
Sep 21 03:56:04 Starting examples/opentheory
Sep 21 04:06:49 Finished examples/opentheory                                  10m43s   8GB
Sep 21 04:06:50 Starting examples/opentheory
Sep 21 04:06:51 Finished examples/opentheory                                      0s 122MB
Sep 21 04:06:52 Starting examples/opentheory/compilation
Sep 21 04:42:17 Finished examples/opentheory/compilation                      35m24s  49GB
Sep 21 04:42:18 Starting examples/opentheory/compilation/proofs
Sep 21 04:43:43 Finished examples/opentheory/compilation/proofs                1m23s   7GB
Sep 21 04:43:43 Starting examples/opentheory/compilation/ag32
Sep 21 05:15:32 Finished examples/opentheory/compilation/ag32                 31m47s  47GB
Sep 21 05:15:33 Starting examples/opentheory/compilation/ag32/proofs
Sep 21 05:17:49 Finished examples/opentheory/compilation/ag32/proofs           2m15s  11GB
Sep 21 05:17:49 Starting examples/sat_encodings
Sep 21 05:20:28 Finished examples/sat_encodings                                2m37s   1GB
Sep 21 05:20:29 Starting examples/sat_encodings/case_studies
Sep 21 05:22:28 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Sep 21 05:22:28 Starting examples/sat_encodings/translation
Sep 21 05:28:33 Finished examples/sat_encodings/translation                    6m03s   7GB
Sep 21 05:28:34 Starting examples/sat_encodings/translation/compilation
Sep 21 06:03:43 Finished examples/sat_encodings/translation/compilation       35m06s  28GB
Sep 21 06:03:44 Starting examples/deflate
Sep 21 06:04:58 Finished examples/deflate                                      1m12s   1GB
Sep 21 06:04:59 Starting examples/deflate/translation
Sep 21 06:06:36 Finished examples/deflate/translation                          1m36s   7GB
Sep 21 06:06:37 Starting examples/deflate/translation/compilation
Sep 21 06:23:07 Finished examples/deflate/translation/compilation             16m29s  27GB
Sep 21 06:23:08 Starting examples/vipr
Sep 21 06:27:11 Finished examples/vipr                                         4m02s   7GB
Sep 21 06:27:12 Starting examples/vipr/compilation
Sep 21 06:46:44 Finished examples/vipr/compilation                            19m30s  22GB
Sep 21 06:46:45 Starting translator/okasaki-examples
Sep 21 06:51:43 Finished translator/okasaki-examples                           4m57s   4GB
Sep 21 06:51:44 Starting translator/other-examples
Sep 21 06:55:21 Finished translator/other-examples                             3m35s   3GB
Sep 21 06:55:21 Starting compiler/parsing/tests
Sep 21 06:55:55 Finished compiler/parsing/tests                                  32s   1GB
Sep 21 06:55:56 Starting compiler/inference/tests
Sep 21 07:03:23 Finished compiler/inference/tests                              7m26s   5GB
Sep 21 07:03:24 Starting compiler/printing/test
Sep 21 07:06:53 Finished compiler/printing/test                                3m27s   6GB
Sep 21 07:06:54 Starting icing/flover
Sep 21 07:42:14 Finished icing/flover                                         35m19s   5GB
Sep 21 07:42:15 Starting icing/
Sep 21 08:38:40 Finished icing/                                               56m24s  30GB
Sep 21 08:38:41 Starting icing/examples
Sep 21 08:40:21 Finished icing/examples                                        1m38s   8GB
Sep 21 08:40:22 Starting compiler/repl
Sep 21 08:49:02 Finished compiler/repl                                         8m39s   9GB
Sep 21 08:49:03 Starting unverified/sexpr-bootstrap/x64/64
Sep 21 09:00:16 Finished unverified/sexpr-bootstrap/x64/64                    10m51s  16GB
Sep 21 09:00:17 Starting unverified/sexpr-bootstrap/x64/32
Sep 21 09:09:30 Finished unverified/sexpr-bootstrap/x64/32                     8m56s  14GB
Sep 21 09:09:31 Starting compiler/benchmarks
Sep 21 09:10:16 Finished compiler/benchmarks                                     43s 713MB
Sep 21 09:10:17 Starting compiler/bootstrap/compilation/x64/64
Sep 21 23:47:41 Finished compiler/bootstrap/compilation/x64/64             14h36m55s 156GB
Sep 21 23:47:42 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 22 00:08:51 Finished compiler/bootstrap/compilation/x64/64/proofs         21m08s  36GB
Sep 22 00:08:52 Starting compiler/bootstrap/compilation/x64/32
Sep 22 07:10:13 Finished compiler/bootstrap/compilation/x64/32              7h00m57s 122GB
Sep 22 07:10:14 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 22 07:13:39 Finished compiler/bootstrap/compilation/x64/32/proofs          3m24s  18GB
Sep 22 07:13:40 Starting compiler/bootstrap/compilation/ag32/32
Sep 22 14:50:05 Finished compiler/bootstrap/compilation/ag32/32             7h36m23s 128GB
Sep 22 14:50:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 22 14:57:33 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m27s  49GB
Sep 22 14:57:34 SUCCESS