Job 1910

CakeML:7c4f5d1ea435d9c438fa5c6f782526b8154e7f1e
  Merge pull request #865 from CakeML/Iced_cake [May 24 14:01:13]
HOL:6a1ba20cc9ca0bffba3c7aa005b4699fa8fd2da2
  Congruence rule for composition of functions. Prompted by example fro [May 25 19:48:20]
Machine:oven3

Jun 04 19:50:48 Claimed job
Jun 04 19:50:49 Reusing HOL
Jun 04 19:51:41 Starting developers
Jun 04 19:51:50 Finished developers                                               8s 121MB
Jun 04 19:51:51 Starting developers/bin
Jun 04 19:52:03 Finished developers/bin                                          12s   1GB
Jun 04 19:52:03 Starting semantics/ffi
Jun 04 19:52:30 Finished semantics/ffi                                           26s 251MB
Jun 04 19:52:30 Starting semantics
Jun 04 19:57:29 Finished semantics                                             4m58s   1GB
Jun 04 19:57:29 Starting semantics/proofs
Jun 04 20:12:43 Finished semantics/proofs                                     15m14s   1GB
Jun 04 20:12:43 Starting semantics/alt_semantics
Jun 04 20:13:41 Finished semantics/alt_semantics                                 56s 527MB
Jun 04 20:13:41 Starting semantics/alt_semantics/proofs
Jun 04 20:38:55 Finished semantics/alt_semantics/proofs                       25m13s   1GB
Jun 04 20:38:55 Starting basis/pure
Jun 04 20:41:15 Finished basis/pure                                            2m19s   1GB
Jun 04 20:41:15 Starting translator
Jun 04 20:49:03 Finished translator                                            7m47s   2GB
Jun 04 20:49:03 Starting compiler/parsing
Jun 04 20:51:55 Finished compiler/parsing                                      2m51s   5GB
Jun 04 20:51:55 Starting characteristic
Jun 04 21:06:35 Finished characteristic                                       14m39s   2GB
Jun 04 21:06:35 Starting translator/monadic
Jun 04 21:10:49 Finished translator/monadic                                    4m13s   1GB
Jun 04 21:10:49 Starting basis
Jun 04 23:07:07 Finished basis                                              1h56m17s  14GB
Jun 04 23:07:07 Starting compiler/inference
Jun 04 23:10:40 Finished compiler/inference                                    3m31s   2GB
Jun 04 23:10:40 Starting compiler/backend/reg_alloc
Jun 04 23:13:56 Finished compiler/backend/reg_alloc                            3m15s   1GB
Jun 04 23:13:58 Starting compiler/backend/gc
Jun 04 23:23:51 Finished compiler/backend/gc                                   9m53s   2GB
Jun 04 23:23:52 Starting compiler/backend
Jun 04 23:37:20 Finished compiler/backend                                     13m27s   2GB
Jun 04 23:37:20 Starting compiler/encoders/asm
Jun 04 23:38:36 Finished compiler/encoders/asm                                 1m15s 748MB
Jun 04 23:38:36 Starting compiler/encoders/x64
Jun 04 23:39:42 Finished compiler/encoders/x64                                 1m05s 665MB
Jun 04 23:39:42 Starting compiler/encoders/arm7
Jun 04 23:41:56 Finished compiler/encoders/arm7                                2m13s 798MB
Jun 04 23:41:56 Starting compiler/encoders/arm8
Jun 04 23:42:32 Finished compiler/encoders/arm8                                  35s 801MB
Jun 04 23:42:32 Starting compiler/encoders/arm8_asl
Jun 04 23:50:07 Finished compiler/encoders/arm8_asl                            7m34s   1GB
Jun 04 23:50:07 Starting compiler/encoders/mips
Jun 04 23:50:54 Finished compiler/encoders/mips                                  46s   1GB
Jun 04 23:50:54 Starting compiler/encoders/riscv
Jun 04 23:51:33 Finished compiler/encoders/riscv                                 38s 829MB
Jun 04 23:51:33 Starting compiler/encoders/ag32
Jun 04 23:52:27 Finished compiler/encoders/ag32                                  54s 830MB
Jun 04 23:52:28 Starting compiler/backend/x64
Jun 04 23:53:28 Finished compiler/backend/x64                                  1m00s   1GB
Jun 04 23:53:28 Starting compiler/backend/arm7
Jun 04 23:54:25 Finished compiler/backend/arm7                                   56s   1GB
Jun 04 23:54:25 Starting compiler/backend/arm8
Jun 04 23:55:22 Finished compiler/backend/arm8                                   56s   1GB
Jun 04 23:55:23 Starting compiler/backend/mips
Jun 04 23:56:17 Finished compiler/backend/mips                                   53s   1GB
Jun 04 23:56:17 Starting compiler/backend/riscv
Jun 04 23:57:19 Finished compiler/backend/riscv                                1m01s   1GB
Jun 04 23:57:19 Starting compiler/backend/ag32
Jun 05 00:00:34 Finished compiler/backend/ag32                                 3m14s   1GB
Jun 05 00:00:34 Starting compiler/parsing/proofs
Jun 05 00:09:08 Finished compiler/parsing/proofs                               8m33s   1GB
Jun 05 00:09:09 Starting compiler/inference/proofs
Jun 05 00:15:21 Finished compiler/inference/proofs                             6m11s   1GB
Jun 05 00:15:21 Starting compiler/backend/semantics
Jun 05 01:25:35 Finished compiler/backend/semantics                         1h10m13s   2GB
Jun 05 01:25:35 Starting compiler/backend/reg_alloc/proofs
Jun 05 01:33:25 Finished compiler/backend/reg_alloc/proofs                     7m49s   1GB
Jun 05 01:33:25 Starting compiler/backend/proofs
Jun 05 03:22:00 Finished compiler/backend/proofs                            1h48m33s  11GB
Jun 05 03:22:00 Starting compiler/backend/serialiser
Jun 05 03:25:22 Finished compiler/backend/serialiser                           3m22s   1GB
Jun 05 03:25:22 Starting compiler/encoders/x64/proofs
Jun 05 03:46:42 Finished compiler/encoders/x64/proofs                         21m19s   5GB
Jun 05 03:46:42 Starting compiler/encoders/arm7/proofs
Jun 05 04:16:39 Finished compiler/encoders/arm7/proofs                        29m56s   3GB
Jun 05 04:16:39 Starting compiler/encoders/arm8/proofs
Jun 05 04:32:14 Finished compiler/encoders/arm8/proofs                        15m34s   1GB
Jun 05 04:32:14 Starting compiler/encoders/arm8_asl/proofs
Jun 05 05:07:28 Finished compiler/encoders/arm8_asl/proofs                    35m13s   2GB
Jun 05 05:07:28 Starting compiler/encoders/mips/proofs
Jun 05 05:30:44 Finished compiler/encoders/mips/proofs                        23m15s   2GB
Jun 05 05:30:44 Starting compiler/encoders/riscv/proofs
Jun 05 05:51:07 Finished compiler/encoders/riscv/proofs                       20m21s   1GB
Jun 05 05:51:07 Starting compiler/encoders/ag32/proofs
Jun 05 05:56:49 Finished compiler/encoders/ag32/proofs                         5m42s 991MB
Jun 05 05:56:49 Starting compiler/backend/x64/proofs
Jun 05 05:57:52 Finished compiler/backend/x64/proofs                           1m02s   2GB
Jun 05 05:57:53 Starting compiler/backend/arm7/proofs
Jun 05 05:58:56 Finished compiler/backend/arm7/proofs                          1m03s   1GB
Jun 05 05:58:57 Starting compiler/backend/arm8/proofs
Jun 05 06:00:01 Finished compiler/backend/arm8/proofs                          1m03s   1GB
Jun 05 06:00:01 Starting compiler/backend/arm8_asl
Jun 05 06:00:51 Finished compiler/backend/arm8_asl                               49s   1GB
Jun 05 06:00:51 Starting compiler/backend/mips/proofs
Jun 05 06:01:55 Finished compiler/backend/mips/proofs                          1m04s   1GB
Jun 05 06:01:56 Starting compiler/backend/riscv/proofs
Jun 05 06:02:59 Finished compiler/backend/riscv/proofs                         1m03s   1GB
Jun 05 06:03:00 Starting compiler/backend/ag32/proofs
Jun 05 06:33:25 Finished compiler/backend/ag32/proofs                         30m25s   4GB
Jun 05 06:33:25 Starting compiler/proofs
Jun 05 06:38:02 Finished compiler/proofs                                       4m36s   3GB
Jun 05 06:38:02 Starting candle/set-theory
Jun 05 06:39:09 Finished candle/set-theory                                     1m07s   1GB
Jun 05 06:39:09 Starting candle/syntax-lib
Jun 05 06:39:40 Finished candle/syntax-lib                                       30s 707MB
Jun 05 06:39:40 Starting candle/standard/syntax
Jun 05 06:44:09 Finished candle/standard/syntax                                4m28s   1GB
Jun 05 06:44:09 Starting candle/standard/semantics
Jun 05 06:48:10 Finished candle/standard/semantics                             4m00s   1GB
Jun 05 06:48:11 Starting candle/standard/monadic
Jun 05 06:52:18 Finished candle/standard/monadic                               4m06s   1GB
Jun 05 06:52:18 Starting candle/standard/ml_kernel
Jun 05 07:06:08 Finished candle/standard/ml_kernel                            13m50s   3GB
Jun 05 07:06:08 Starting candle/overloading/syntax
Jun 05 07:13:06 Finished candle/overloading/syntax                             6m56s   1GB
Jun 05 07:13:06 Starting candle/overloading/semantics
Jun 05 07:38:35 Finished candle/overloading/semantics                         25m28s   2GB
Jun 05 07:38:35 Starting candle/overloading/monadic
Jun 05 07:44:05 Finished candle/overloading/monadic                            5m29s   1GB
Jun 05 07:44:05 Starting candle/overloading/ml_kernel
Jun 05 07:59:57 Finished candle/overloading/ml_kernel                         15m51s   3GB
Jun 05 07:59:57 Starting candle/overloading/ml_checker
Jun 05 08:05:14 Finished candle/overloading/ml_checker                         5m16s   3GB
Jun 05 08:05:14 Starting candle/prover
Jun 05 08:29:43 Finished candle/prover                                        24m29s   3GB
Jun 05 08:29:44 Starting pancake
Jun 05 08:37:44 Finished pancake                                               7m59s   4GB
Jun 05 08:37:44 Starting pancake/ffi
Jun 05 08:37:45 Finished pancake/ffi                                              0s  30MB
Jun 05 08:37:45 Starting pancake/semantics
Jun 05 08:43:05 Finished pancake/semantics                                     5m19s   1GB
Jun 05 08:43:05 Starting pancake/proofs
Jun 05 09:09:14 Finished pancake/proofs                                       26m08s   7GB
Jun 05 09:09:14 Starting characteristic/examples
Jun 05 09:12:19 Finished characteristic/examples                               3m04s   4GB
Jun 05 09:12:19 Starting tutorial/solutions
Jun 05 09:49:41 Finished tutorial/solutions                                   37m21s   9GB
Jun 05 09:49:41 Starting translator/monadic/examples
Jun 05 09:56:51 Finished translator/monadic/examples                           7m09s   2GB
Jun 05 09:56:51 Starting examples
Jun 05 10:15:55 Finished examples                                             19m03s   3GB
Jun 05 10:15:55 Starting examples/compilation/x64
Jun 05 15:52:58 Finished examples/compilation/x64                           5h37m02s  19GB
Jun 05 15:52:59 Starting examples/compilation/x64/proofs
Jun 05 15:57:25 Finished examples/compilation/x64/proofs                       4m26s   3GB
Jun 05 15:57:25 Starting examples/compilation/ag32
Jun 05 17:15:21 Finished examples/compilation/ag32                          1h17m54s   9GB
Jun 05 17:15:21 Starting examples/compilation/ag32/proofs
Jun 05 17:17:21 Finished examples/compilation/ag32/proofs                      1m59s   2GB
Jun 05 17:17:21 Starting examples/cost
Jun 05 19:25:25 Finished examples/cost                                      2h08m03s   8GB
Jun 05 19:25:26 Starting examples/lpr_checker
Jun 05 19:27:36 Finished examples/lpr_checker                                  2m10s   1GB
Jun 05 19:27:36 Starting examples/lpr_checker/array
Jun 05 20:42:10 Finished examples/lpr_checker/array                         1h14m31s   9GB
Jun 05 20:42:10 Starting examples/lpr_checker/array/compilation
Jun 05 23:49:06 Finished examples/lpr_checker/array/compilation             3h06m54s  38GB
Jun 05 23:49:06 Starting examples/lpr_checker/array/compilation/proofs
Jun 05 23:52:04 Finished examples/lpr_checker/array/compilation/proofs         2m58s   6GB
Jun 05 23:52:04 Starting examples/opentheory
Jun 06 00:14:52 Finished examples/opentheory                                  22m47s   4GB
Jun 06 00:14:53 Starting examples/opentheory
Jun 06 00:14:56 Finished examples/opentheory                                      2s  32MB
Jun 06 00:14:56 Starting examples/opentheory/compilation
Jun 06 01:48:26 Finished examples/opentheory/compilation                    1h33m29s  36GB
Jun 06 01:48:26 Starting examples/opentheory/compilation/proofs
Jun 06 01:51:01 Finished examples/opentheory/compilation/proofs                2m34s   3GB
Jun 06 01:51:01 Starting examples/opentheory/compilation/ag32
Jun 06 03:15:06 Finished examples/opentheory/compilation/ag32               1h24m03s  30GB
Jun 06 03:15:06 Starting examples/opentheory/compilation/ag32/proofs
Jun 06 03:19:02 Finished examples/opentheory/compilation/ag32/proofs           3m56s   6GB
Jun 06 03:19:03 Starting examples/sat_encodings
Jun 06 03:23:28 Finished examples/sat_encodings                                4m24s 965MB
Jun 06 03:23:28 Starting examples/sat_encodings/case_studies
Jun 06 03:27:15 Finished examples/sat_encodings/case_studies                   3m47s 747MB
Jun 06 03:27:16 Starting examples/sat_encodings/translation
Jun 06 03:39:33 Finished examples/sat_encodings/translation                   12m16s   4GB
Jun 06 03:39:33 Starting examples/sat_encodings/translation/compilation
Jun 06 05:08:04 Finished examples/sat_encodings/translation/compilation     1h28m29s  23GB
Jun 06 05:08:04 Starting translator/okasaki-examples
Jun 06 05:18:26 Finished translator/okasaki-examples                          10m21s   1GB
Jun 06 05:18:26 Starting translator/other-examples
Jun 06 05:20:03 Finished translator/other-examples                             1m36s   1GB
Jun 06 05:20:03 Starting compiler/parsing/tests
Jun 06 05:21:12 Finished compiler/parsing/tests                                1m08s 625MB
Jun 06 05:21:12 Starting compiler/inference/tests
Jun 06 05:37:58 Finished compiler/inference/tests                             16m46s   5GB
Jun 06 05:37:59 Starting compiler/printing/test
Jun 06 05:45:48 Finished compiler/printing/test                                7m49s   3GB
Jun 06 05:45:48 Starting icing/flover
Jun 06 06:13:03 Finished icing/flover                                         27m12s   1GB
Jun 06 06:13:03 Starting icing/
Jun 06 08:27:08 Finished icing/                                             2h14m04s   7GB
Jun 06 08:27:08 Starting icing/examples
Jun 06 08:30:05 Finished icing/examples                                        2m57s   5GB
Jun 06 08:30:06 Starting compiler/repl
Jun 06 08:57:15 Finished compiler/repl                                        27m09s   5GB
Jun 06 08:57:16 Starting compiler/bootstrap/translation
Jun 06 18:05:51 Finished compiler/bootstrap/translation                     9h08m34s  34GB
Jun 06 18:05:51 Starting unverified/sexpr-bootstrap/x64/64
Jun 06 18:28:55 Finished unverified/sexpr-bootstrap/x64/64                    23m03s  12GB
Jun 06 18:28:55 Starting unverified/sexpr-bootstrap/x64/32
Jun 06 18:47:54 Finished unverified/sexpr-bootstrap/x64/32                    18m58s  12GB
Jun 06 18:47:54 Starting compiler/benchmarks
Jun 06 18:48:00 Finished compiler/benchmarks                                      5s  57MB
Jun 06 18:48:00 Starting compiler/bootstrap/compilation/x64/64
Jun 08 12:06:38 Finished compiler/bootstrap/compilation/x64/64             41h18m36s 108GB
Jun 08 12:06:38 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 08 12:49:20 Finished compiler/bootstrap/compilation/x64/64/proofs         42m41s  35GB
Jun 08 12:49:20 Starting compiler/bootstrap/compilation/x64/32
Jun 09 18:08:46 Finished compiler/bootstrap/compilation/x64/32             29h19m24s  89GB
Jun 09 18:08:46 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 09 18:17:56 Finished compiler/bootstrap/compilation/x64/32/proofs          9m10s  15GB
Jun 09 18:17:57 Starting compiler/bootstrap/compilation/ag32/32
Jun 11 00:01:56 Finished compiler/bootstrap/compilation/ag32/32            29h43m59s 103GB
Jun 11 00:01:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 11 00:26:47 Finished compiler/bootstrap/compilation/ag32/32/proofs        24m49s  48GB
Jun 11 00:26:47 SUCCESS