Job 1901

CakeML:a986431ac4c37f9c4e3ea55de543535a0b08637c
  Merge pull request #885 from CakeML/caml-pattern-guards [May 16 00:45:00]
HOL:db0c48a4df81300b8f4ab65af329cee860f6d921
  Fix a l3_equivalence_misc proof [May 10 01:22:03]
Machine:oven3

May 16 21:45:10 Claimed job
May 16 21:45:17 Reusing HOL
May 16 21:46:09 Starting developers
May 16 21:46:17 Finished developers                                               8s 133MB
May 16 21:46:18 Starting developers/bin
May 16 21:49:29 Finished developers/bin                                        3m11s   1GB
May 16 21:49:29 Starting semantics/ffi
May 16 21:49:54 Finished semantics/ffi                                           24s 252MB
May 16 21:49:54 Starting semantics
May 16 21:53:51 Finished semantics                                             3m56s   1GB
May 16 21:53:51 Starting semantics/proofs
May 16 22:02:50 Finished semantics/proofs                                      8m58s   2GB
May 16 22:02:50 Starting semantics/alt_semantics
May 16 22:03:44 Finished semantics/alt_semantics                                 53s 497MB
May 16 22:03:45 Starting semantics/alt_semantics/proofs
May 16 22:10:28 Finished semantics/alt_semantics/proofs                        6m43s   1GB
May 16 22:10:28 Starting basis/pure
May 16 22:12:41 Finished basis/pure                                            2m12s 844MB
May 16 22:12:41 Starting translator
May 16 22:18:58 Finished translator                                            6m15s   1GB
May 16 22:18:59 Starting compiler/parsing
May 16 22:21:46 Finished compiler/parsing                                      2m47s   2GB
May 16 22:21:47 Starting characteristic
May 16 22:35:13 Finished characteristic                                       13m26s   2GB
May 16 22:35:13 Starting translator/monadic
May 16 22:39:15 Finished translator/monadic                                    4m01s   1GB
May 16 22:39:15 Starting basis
May 17 00:22:12 Finished basis                                              1h42m56s  24GB
May 17 00:22:12 Starting compiler/inference
May 17 00:25:09 Finished compiler/inference                                    2m56s   1GB
May 17 00:25:09 Starting compiler/backend/reg_alloc
May 17 00:28:21 Finished compiler/backend/reg_alloc                            3m12s   1GB
May 17 00:28:22 Starting compiler/backend/gc
May 17 00:36:36 Finished compiler/backend/gc                                   8m14s   2GB
May 17 00:36:37 Starting compiler/backend
May 17 00:47:23 Finished compiler/backend                                     10m45s   2GB
May 17 00:47:23 Starting compiler/encoders/asm
May 17 00:48:27 Finished compiler/encoders/asm                                 1m03s 712MB
May 17 00:48:27 Starting compiler/encoders/x64
May 17 00:49:36 Finished compiler/encoders/x64                                 1m08s 874MB
May 17 00:49:36 Starting compiler/encoders/arm7
May 17 00:51:38 Finished compiler/encoders/arm7                                2m02s 726MB
May 17 00:51:39 Starting compiler/encoders/arm8
May 17 00:52:15 Finished compiler/encoders/arm8                                  35s   1GB
May 17 00:52:15 Starting compiler/encoders/arm8_asl
May 17 00:58:54 Finished compiler/encoders/arm8_asl                            6m38s   1GB
May 17 00:58:54 Starting compiler/encoders/mips
May 17 00:59:37 Finished compiler/encoders/mips                                  42s   1GB
May 17 00:59:37 Starting compiler/encoders/riscv
May 17 01:00:20 Finished compiler/encoders/riscv                                 42s 831MB
May 17 01:00:20 Starting compiler/encoders/ag32
May 17 01:01:09 Finished compiler/encoders/ag32                                  48s 975MB
May 17 01:01:09 Starting compiler/backend/x64
May 17 01:01:57 Finished compiler/backend/x64                                    48s   1GB
May 17 01:01:58 Starting compiler/backend/arm7
May 17 01:02:48 Finished compiler/backend/arm7                                   50s   1GB
May 17 01:02:48 Starting compiler/backend/arm8
May 17 01:03:35 Finished compiler/backend/arm8                                   46s   1GB
May 17 01:03:35 Starting compiler/backend/mips
May 17 01:04:23 Finished compiler/backend/mips                                   47s   1GB
May 17 01:04:23 Starting compiler/backend/riscv
May 17 01:05:11 Finished compiler/backend/riscv                                  48s   1GB
May 17 01:05:11 Starting compiler/backend/ag32
May 17 01:08:12 Finished compiler/backend/ag32                                 3m00s   1GB
May 17 01:08:12 Starting compiler/parsing/proofs
May 17 01:16:39 Finished compiler/parsing/proofs                               8m26s   1GB
May 17 01:16:39 Starting compiler/inference/proofs
May 17 01:22:15 Finished compiler/inference/proofs                             5m35s   1GB
May 17 01:22:15 Starting compiler/backend/semantics
May 17 02:24:43 Finished compiler/backend/semantics                         1h02m27s   2GB
May 17 02:24:43 Starting compiler/backend/reg_alloc/proofs
May 17 02:32:33 Finished compiler/backend/reg_alloc/proofs                     7m50s   1GB
May 17 02:32:33 Starting compiler/backend/proofs
May 17 04:14:11 Finished compiler/backend/proofs                            1h41m37s  18GB
May 17 04:14:11 Starting compiler/backend/serialiser
May 17 04:17:33 Finished compiler/backend/serialiser                           3m21s   2GB
May 17 04:17:33 Starting compiler/encoders/x64/proofs
May 17 04:39:21 Finished compiler/encoders/x64/proofs                         21m47s   4GB
May 17 04:39:21 Starting compiler/encoders/arm7/proofs
May 17 05:09:35 Finished compiler/encoders/arm7/proofs                        30m13s   3GB
May 17 05:09:35 Starting compiler/encoders/arm8/proofs
May 17 05:25:03 Finished compiler/encoders/arm8/proofs                        15m26s   1GB
May 17 05:25:03 Starting compiler/encoders/arm8_asl/proofs
May 17 06:00:42 Finished compiler/encoders/arm8_asl/proofs                    35m38s   1GB
May 17 06:00:42 Starting compiler/encoders/mips/proofs
May 17 06:24:16 Finished compiler/encoders/mips/proofs                        23m33s   2GB
May 17 06:24:16 Starting compiler/encoders/riscv/proofs
May 17 06:44:09 Finished compiler/encoders/riscv/proofs                       19m53s   1GB
May 17 06:44:09 Starting compiler/encoders/ag32/proofs
May 17 06:49:55 Finished compiler/encoders/ag32/proofs                         5m45s 773MB
May 17 06:49:55 Starting compiler/backend/x64/proofs
May 17 06:50:58 Finished compiler/backend/x64/proofs                           1m03s   1GB
May 17 06:50:58 Starting compiler/backend/arm7/proofs
May 17 06:51:58 Finished compiler/backend/arm7/proofs                            59s   1GB
May 17 06:51:58 Starting compiler/backend/arm8/proofs
May 17 06:52:59 Finished compiler/backend/arm8/proofs                          1m01s   1GB
May 17 06:52:59 Starting compiler/backend/arm8_asl
May 17 06:53:52 Finished compiler/backend/arm8_asl                               52s   1GB
May 17 06:53:52 Starting compiler/backend/mips/proofs
May 17 06:54:56 Finished compiler/backend/mips/proofs                          1m03s   1GB
May 17 06:54:56 Starting compiler/backend/riscv/proofs
May 17 06:55:58 Finished compiler/backend/riscv/proofs                         1m01s   1GB
May 17 06:55:59 Starting compiler/backend/ag32/proofs
May 17 07:23:22 Finished compiler/backend/ag32/proofs                         27m23s   2GB
May 17 07:23:23 Starting compiler/proofs
May 17 07:28:00 Finished compiler/proofs                                       4m36s   4GB
May 17 07:28:00 Starting candle/set-theory
May 17 07:29:09 Finished candle/set-theory                                     1m09s 985MB
May 17 07:29:10 Starting candle/syntax-lib
May 17 07:29:39 Finished candle/syntax-lib                                       29s 661MB
May 17 07:29:40 Starting candle/standard/syntax
May 17 07:34:04 Finished candle/standard/syntax                                4m24s   1GB
May 17 07:34:04 Starting candle/standard/semantics
May 17 07:38:07 Finished candle/standard/semantics                             4m02s   1GB
May 17 07:38:07 Starting candle/standard/monadic
May 17 07:42:08 Finished candle/standard/monadic                               4m00s   1GB
May 17 07:42:08 Starting candle/standard/ml_kernel
May 17 07:55:14 Finished candle/standard/ml_kernel                            13m05s   4GB
May 17 07:55:14 Starting candle/overloading/syntax
May 17 08:02:09 Finished candle/overloading/syntax                             6m54s   1GB
May 17 08:02:09 Starting candle/overloading/semantics
May 17 08:28:07 Finished candle/overloading/semantics                         25m58s   2GB
May 17 08:28:08 Starting candle/overloading/monadic
May 17 08:33:32 Finished candle/overloading/monadic                            5m24s   1GB
May 17 08:33:32 Starting candle/overloading/ml_kernel
May 17 08:48:42 Finished candle/overloading/ml_kernel                         15m09s   3GB
May 17 08:48:42 Starting candle/overloading/ml_checker
May 17 08:54:02 Finished candle/overloading/ml_checker                         5m19s   2GB
May 17 08:54:02 Starting candle/prover
May 17 09:12:02 Finished candle/prover                                        17m59s   3GB
May 17 09:12:02 Starting pancake
May 17 09:19:44 Finished pancake                                               7m41s   4GB
May 17 09:19:44 Starting pancake/ffi
May 17 09:19:45 Finished pancake/ffi                                              0s  30MB
May 17 09:19:45 Starting pancake/semantics
May 17 09:25:06 Finished pancake/semantics                                     5m21s   1GB
May 17 09:25:07 Starting pancake/proofs
May 17 09:51:57 Finished pancake/proofs                                       26m50s   6GB
May 17 09:51:57 Starting characteristic/examples
May 17 09:54:55 Finished characteristic/examples                               2m57s   3GB
May 17 09:54:55 Starting tutorial/solutions
May 17 10:32:03 Finished tutorial/solutions                                   37m08s   9GB
May 17 10:32:03 Starting translator/monadic/examples
May 17 10:39:10 Finished translator/monadic/examples                           7m06s   3GB
May 17 10:39:10 Starting examples
May 17 10:57:27 Finished examples                                             18m16s   3GB
May 17 10:57:27 Starting examples/compilation/x64
May 17 16:37:15 Finished examples/compilation/x64                           5h39m47s  26GB
May 17 16:37:16 Starting examples/compilation/x64/proofs
May 17 16:41:36 Finished examples/compilation/x64/proofs                       4m19s   3GB
May 17 16:41:36 Starting examples/compilation/ag32
May 17 18:00:42 Finished examples/compilation/ag32                          1h19m04s   9GB
May 17 18:00:42 Starting examples/compilation/ag32/proofs
May 17 18:02:43 Finished examples/compilation/ag32/proofs                      2m00s   2GB
May 17 18:02:43 Starting examples/cost
May 17 20:04:17 Finished examples/cost                                      2h01m33s   9GB
May 17 20:04:17 Starting examples/lpr_checker
May 17 20:06:30 Finished examples/lpr_checker                                  2m12s   1GB
May 17 20:06:31 Starting examples/lpr_checker/array
May 17 21:11:25 Finished examples/lpr_checker/array                         1h04m53s   5GB
May 17 21:11:25 Starting examples/lpr_checker/array/compilation
May 18 00:18:17 Finished examples/lpr_checker/array/compilation             3h06m51s  38GB
May 18 00:18:18 Starting examples/lpr_checker/array/compilation/proofs
May 18 00:21:22 Finished examples/lpr_checker/array/compilation/proofs         3m04s   7GB
May 18 00:21:22 Starting examples/opentheory
May 18 00:42:52 Finished examples/opentheory                                  21m29s   4GB
May 18 00:42:53 Starting examples/opentheory
May 18 00:42:56 Finished examples/opentheory                                      2s  32MB
May 18 00:42:56 Starting examples/opentheory/compilation
May 18 02:17:34 Finished examples/opentheory/compilation                    1h34m37s  36GB
May 18 02:17:34 Starting examples/opentheory/compilation/proofs
May 18 02:19:52 Finished examples/opentheory/compilation/proofs                2m17s   3GB
May 18 02:19:52 Starting examples/opentheory/compilation/ag32
May 18 03:43:24 Finished examples/opentheory/compilation/ag32               1h23m31s  28GB
May 18 03:43:24 Starting examples/opentheory/compilation/ag32/proofs
May 18 03:47:17 Finished examples/opentheory/compilation/ag32/proofs           3m53s   7GB
May 18 03:47:18 Starting examples/sat_encodings
May 18 03:51:42 Finished examples/sat_encodings                                4m24s 973MB
May 18 03:51:42 Starting examples/sat_encodings/case_studies
May 18 03:55:25 Finished examples/sat_encodings/case_studies                   3m42s 717MB
May 18 03:55:25 Starting examples/sat_encodings/translation
May 18 04:07:02 Finished examples/sat_encodings/translation                   11m36s   3GB
May 18 04:07:02 Starting examples/sat_encodings/translation/compilation
May 18 05:37:27 Finished examples/sat_encodings/translation/compilation     1h30m24s  26GB
May 18 05:37:27 Starting translator/okasaki-examples
May 18 05:47:16 Finished translator/okasaki-examples                           9m48s   1GB
May 18 05:47:16 Starting translator/other-examples
May 18 05:48:45 Finished translator/other-examples                             1m28s   1GB
May 18 05:48:45 Starting compiler/parsing/tests
May 18 05:49:54 Finished compiler/parsing/tests                                1m08s 714MB
May 18 05:49:54 Starting compiler/inference/tests
May 18 06:06:25 Finished compiler/inference/tests                             16m30s   5GB
May 18 06:06:25 Starting compiler/printing/test
May 18 06:13:58 Finished compiler/printing/test                                7m33s   3GB
May 18 06:13:59 Starting compiler/repl
May 18 06:39:35 Finished compiler/repl                                        25m35s   8GB
May 18 06:39:35 Starting compiler/bootstrap/translation
May 18 15:16:22 Finished compiler/bootstrap/translation                     8h36m46s  37GB
May 18 15:16:23 Starting unverified/sexpr-bootstrap/x64/64
May 18 15:39:33 Finished unverified/sexpr-bootstrap/x64/64                    23m09s  12GB
May 18 15:39:33 Starting unverified/sexpr-bootstrap/x64/32
May 18 15:58:27 Finished unverified/sexpr-bootstrap/x64/32                    18m53s   9GB
May 18 15:58:27 Starting compiler/benchmarks
May 18 15:58:33 Finished compiler/benchmarks                                      5s  52MB
May 18 15:58:33 Starting compiler/bootstrap/compilation/x64/64
May 20 08:11:16 Finished compiler/bootstrap/compilation/x64/64             40h12m42s  84GB
May 20 08:11:17 Starting compiler/bootstrap/compilation/x64/64/proofs
May 20 08:52:01 Finished compiler/bootstrap/compilation/x64/64/proofs         40m43s  37GB
May 20 08:52:01 Starting compiler/bootstrap/compilation/x64/32
May 21 14:42:22 Finished compiler/bootstrap/compilation/x64/32             29h50m19s 109GB
May 21 14:42:22 Starting compiler/bootstrap/compilation/x64/32/proofs
May 21 14:48:58 Finished compiler/bootstrap/compilation/x64/32/proofs          6m35s  22GB
May 21 14:48:58 Starting compiler/bootstrap/compilation/ag32/32
May 22 22:44:42 Finished compiler/bootstrap/compilation/ag32/32            31h55m42s 109GB
May 22 22:44:42 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 22 23:36:10 Finished compiler/bootstrap/compilation/ag32/32/proofs        51m27s  25GB
May 22 23:36:10 SUCCESS