Job 1899

CakeML:27966171eba31e086a266c4870d0e3f41e74c5a6
  Merge branch 'master' into Iced_cake [May 10 08:02:28]
#865 (Iced_cake)
Merging into: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:stove 4.15.0-143-generic x86_64 GNU/Linux

May 16 00:46:43 Claimed job
May 16 00:46:46 Reusing HOL
May 16 00:47:00 Starting developers
May 16 00:47:04 Finished developers                                               4s 130MB
May 16 00:47:04 Starting developers/bin
May 16 00:47:11 Finished developers/bin                                           6s   1GB
May 16 00:47:11 Starting semantics/ffi
May 16 00:47:22 Finished semantics/ffi                                           10s 208MB
May 16 00:47:22 Starting semantics
May 16 00:49:48 Finished semantics                                             2m25s   1GB
May 16 00:49:48 Starting semantics/proofs
May 16 00:56:44 Finished semantics/proofs                                      6m56s   1GB
May 16 00:56:45 Starting semantics/alt_semantics
May 16 00:57:12 Finished semantics/alt_semantics                                 27s 531MB
May 16 00:57:12 Starting semantics/alt_semantics/proofs
May 16 01:08:37 Finished semantics/alt_semantics/proofs                       11m23s   1GB
May 16 01:08:38 Starting basis/pure
May 16 01:09:45 Finished basis/pure                                            1m06s   1GB
May 16 01:09:45 Starting translator
May 16 01:13:23 Finished translator                                            3m37s   2GB
May 16 01:13:23 Starting compiler/parsing
May 16 01:14:48 Finished compiler/parsing                                      1m24s   5GB
May 16 01:14:48 Starting characteristic
May 16 01:21:46 Finished characteristic                                        6m57s   1GB
May 16 01:21:46 Starting translator/monadic
May 16 01:23:50 Finished translator/monadic                                    2m04s   1GB
May 16 01:23:50 Starting basis
May 16 02:15:13 Finished basis                                                51m20s  24GB
May 16 02:15:13 Starting compiler/inference
May 16 02:16:44 Finished compiler/inference                                    1m30s   1GB
May 16 02:16:44 Starting compiler/backend/reg_alloc
May 16 02:18:29 Finished compiler/backend/reg_alloc                            1m44s   1GB
May 16 02:18:29 Starting compiler/backend/gc
May 16 02:22:55 Finished compiler/backend/gc                                   4m25s   1GB
May 16 02:22:55 Starting compiler/backend
May 16 02:28:44 Finished compiler/backend                                      5m48s   2GB
May 16 02:28:44 Starting compiler/encoders/asm
May 16 02:29:15 Finished compiler/encoders/asm                                   30s 773MB
May 16 02:29:15 Starting compiler/encoders/x64
May 16 02:29:45 Finished compiler/encoders/x64                                   29s 819MB
May 16 02:29:45 Starting compiler/encoders/arm7
May 16 02:30:39 Finished compiler/encoders/arm7                                  54s 747MB
May 16 02:30:39 Starting compiler/encoders/arm8
May 16 02:30:56 Finished compiler/encoders/arm8                                  16s   1GB
May 16 02:30:56 Starting compiler/encoders/arm8_asl
May 16 02:33:28 Finished compiler/encoders/arm8_asl                            2m31s   1GB
May 16 02:33:28 Starting compiler/encoders/mips
May 16 02:33:50 Finished compiler/encoders/mips                                  21s   1GB
May 16 02:33:50 Starting compiler/encoders/riscv
May 16 02:34:10 Finished compiler/encoders/riscv                                 19s 895MB
May 16 02:34:10 Starting compiler/encoders/ag32
May 16 02:34:32 Finished compiler/encoders/ag32                                  22s 940MB
May 16 02:34:32 Starting compiler/backend/x64
May 16 02:34:55 Finished compiler/backend/x64                                    22s   1GB
May 16 02:34:55 Starting compiler/backend/arm7
May 16 02:35:20 Finished compiler/backend/arm7                                   24s   1GB
May 16 02:35:20 Starting compiler/backend/arm8
May 16 02:35:42 Finished compiler/backend/arm8                                   22s   1GB
May 16 02:35:43 Starting compiler/backend/mips
May 16 02:36:05 Finished compiler/backend/mips                                   22s   1GB
May 16 02:36:05 Starting compiler/backend/riscv
May 16 02:36:28 Finished compiler/backend/riscv                                  22s   1GB
May 16 02:36:28 Starting compiler/backend/ag32
May 16 02:37:56 Finished compiler/backend/ag32                                 1m28s   1GB
May 16 02:37:56 Starting compiler/parsing/proofs
May 16 02:41:42 Finished compiler/parsing/proofs                               3m44s   1GB
May 16 02:41:42 Starting compiler/inference/proofs
May 16 02:44:30 Finished compiler/inference/proofs                             2m48s   1GB
May 16 02:44:30 Starting compiler/backend/semantics
May 16 03:15:29 Finished compiler/backend/semantics                           30m57s   3GB
May 16 03:15:29 Starting compiler/backend/reg_alloc/proofs
May 16 03:19:02 Finished compiler/backend/reg_alloc/proofs                     3m33s 893MB
May 16 03:19:02 Starting compiler/backend/proofs
May 16 04:11:58 Finished compiler/backend/proofs                              52m55s  19GB
May 16 04:11:58 Starting compiler/backend/serialiser
May 16 04:13:35 Finished compiler/backend/serialiser                           1m37s   1GB
May 16 04:13:35 Starting compiler/encoders/x64/proofs
May 16 04:23:01 Finished compiler/encoders/x64/proofs                          9m24s   6GB
May 16 04:23:01 Starting compiler/encoders/arm7/proofs
May 16 04:36:18 Finished compiler/encoders/arm7/proofs                        13m16s   3GB
May 16 04:36:18 Starting compiler/encoders/arm8/proofs
May 16 04:43:05 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
May 16 04:43:05 Starting compiler/encoders/arm8_asl/proofs
May 16 04:58:18 Finished compiler/encoders/arm8_asl/proofs                    15m12s   1GB
May 16 04:58:18 Starting compiler/encoders/mips/proofs
May 16 05:08:15 Finished compiler/encoders/mips/proofs                         9m56s   2GB
May 16 05:08:15 Starting compiler/encoders/riscv/proofs
May 16 05:17:06 Finished compiler/encoders/riscv/proofs                        8m50s   1GB
May 16 05:17:06 Starting compiler/encoders/ag32/proofs
May 16 05:19:42 Finished compiler/encoders/ag32/proofs                         2m35s 758MB
May 16 05:19:42 Starting compiler/backend/x64/proofs
May 16 05:20:10 Finished compiler/backend/x64/proofs                             27s   1GB
May 16 05:20:10 Starting compiler/backend/arm7/proofs
May 16 05:20:39 Finished compiler/backend/arm7/proofs                            29s   1GB
May 16 05:20:39 Starting compiler/backend/arm8/proofs
May 16 05:21:08 Finished compiler/backend/arm8/proofs                            28s   1GB
May 16 05:21:08 Starting compiler/backend/arm8_asl
May 16 05:21:31 Finished compiler/backend/arm8_asl                               23s   1GB
May 16 05:21:31 Starting compiler/backend/mips/proofs
May 16 05:21:59 Finished compiler/backend/mips/proofs                            27s   1GB
May 16 05:21:59 Starting compiler/backend/riscv/proofs
May 16 05:22:27 Finished compiler/backend/riscv/proofs                           27s   1GB
May 16 05:22:27 Starting compiler/backend/ag32/proofs
May 16 05:35:49 Finished compiler/backend/ag32/proofs                         13m20s   2GB
May 16 05:35:49 Starting compiler/proofs
May 16 05:38:07 Finished compiler/proofs                                       2m17s   5GB
May 16 05:38:07 Starting candle/set-theory
May 16 05:38:41 Finished candle/set-theory                                       34s 988MB
May 16 05:38:41 Starting candle/syntax-lib
May 16 05:38:55 Finished candle/syntax-lib                                       13s 634MB
May 16 05:38:55 Starting candle/standard/syntax
May 16 05:40:57 Finished candle/standard/syntax                                2m02s   1GB
May 16 05:40:58 Starting candle/standard/semantics
May 16 05:42:48 Finished candle/standard/semantics                             1m50s   1GB
May 16 05:42:48 Starting candle/standard/monadic
May 16 05:44:43 Finished candle/standard/monadic                               1m54s   1GB
May 16 05:44:43 Starting candle/standard/ml_kernel
May 16 05:51:11 Finished candle/standard/ml_kernel                             6m27s   3GB
May 16 05:51:11 Starting candle/overloading/syntax
May 16 05:54:24 Finished candle/overloading/syntax                             3m12s   1GB
May 16 05:54:24 Starting candle/overloading/semantics
May 16 06:06:05 Finished candle/overloading/semantics                         11m41s   2GB
May 16 06:06:05 Starting candle/overloading/monadic
May 16 06:08:42 Finished candle/overloading/monadic                            2m37s   1GB
May 16 06:08:42 Starting candle/overloading/ml_kernel
May 16 06:16:02 Finished candle/overloading/ml_kernel                          7m19s   4GB
May 16 06:16:02 Starting candle/overloading/ml_checker
May 16 06:18:22 Finished candle/overloading/ml_checker                         2m19s   3GB
May 16 06:18:22 Starting candle/prover
May 16 06:29:05 Finished candle/prover                                        10m42s   3GB
May 16 06:29:05 Starting pancake
May 16 06:32:50 Finished pancake                                               3m44s   4GB
May 16 06:32:50 Starting pancake/ffi
May 16 06:32:50 Finished pancake/ffi                                              0s  35MB
May 16 06:32:50 Starting pancake/semantics
May 16 06:35:21 Finished pancake/semantics                                     2m30s   1GB
May 16 06:35:21 Starting pancake/proofs
May 16 06:47:27 Finished pancake/proofs                                       12m03s   6GB
May 16 06:47:27 Starting characteristic/examples
May 16 06:48:55 Finished characteristic/examples                               1m27s   2GB
May 16 06:48:55 Starting tutorial/solutions
May 16 07:06:10 Finished tutorial/solutions                                   17m14s   9GB
May 16 07:06:10 Starting translator/monadic/examples
May 16 07:10:04 Finished translator/monadic/examples                           3m54s   2GB
May 16 07:10:04 Starting examples
May 16 07:19:48 Finished examples                                              9m43s   3GB
May 16 07:19:49 Starting examples/compilation/x64
May 16 09:50:04 Finished examples/compilation/x64                           2h30m12s  28GB
May 16 09:50:05 Starting examples/compilation/x64/proofs
May 16 09:52:25 Finished examples/compilation/x64/proofs                       2m19s   3GB
May 16 09:52:25 Starting examples/compilation/ag32
May 16 10:27:32 Finished examples/compilation/ag32                            35m06s   8GB
May 16 10:27:32 Starting examples/compilation/ag32/proofs
May 16 10:28:29 Finished examples/compilation/ag32/proofs                        56s   3GB
May 16 10:28:29 Starting examples/cost
May 16 11:27:58 Finished examples/cost                                        59m28s   9GB
May 16 11:27:58 Starting examples/lpr_checker
May 16 11:29:01 Finished examples/lpr_checker                                  1m02s   1GB
May 16 11:29:01 Starting examples/lpr_checker/array
May 16 12:01:46 Finished examples/lpr_checker/array                           32m44s   6GB
May 16 12:01:46 Starting examples/lpr_checker/array/compilation
May 16 13:27:49 Finished examples/lpr_checker/array/compilation             1h26m02s  31GB
May 16 13:27:49 Starting examples/lpr_checker/array/compilation/proofs
May 16 13:29:21 Finished examples/lpr_checker/array/compilation/proofs         1m31s   7GB
May 16 13:29:21 Starting examples/opentheory
May 16 13:39:45 Finished examples/opentheory                                  10m24s   6GB
May 16 13:39:46 Starting examples/opentheory
May 16 13:39:47 Finished examples/opentheory                                      1s 139MB
May 16 13:39:47 Starting examples/opentheory/compilation
May 16 14:21:46 Finished examples/opentheory/compilation                      41m59s  36GB
May 16 14:21:46 Starting examples/opentheory/compilation/proofs
May 16 14:22:39 Finished examples/opentheory/compilation/proofs                  52s   3GB
May 16 14:22:39 Starting examples/opentheory/compilation/ag32
May 16 15:00:27 Finished examples/opentheory/compilation/ag32                 37m47s  28GB
May 16 15:00:27 Starting examples/opentheory/compilation/ag32/proofs
May 16 15:02:19 Finished examples/opentheory/compilation/ag32/proofs           1m51s   6GB
May 16 15:02:19 Starting examples/sat_encodings
May 16 15:04:21 Finished examples/sat_encodings                                2m02s 734MB
May 16 15:04:21 Starting examples/sat_encodings/case_studies
May 16 15:06:04 Finished examples/sat_encodings/case_studies                   1m42s 713MB
May 16 15:06:04 Starting examples/sat_encodings/translation
May 16 15:11:49 Finished examples/sat_encodings/translation                    5m44s   4GB
May 16 15:11:49 Starting examples/sat_encodings/translation/compilation
May 16 16:01:18 Finished examples/sat_encodings/translation/compilation       49m27s  22GB
May 16 16:01:18 Starting translator/okasaki-examples
May 16 16:06:21 Finished translator/okasaki-examples                           5m02s   1GB
May 16 16:06:21 Starting translator/other-examples
May 16 16:07:10 Finished translator/other-examples                               49s   1GB
May 16 16:07:11 Starting compiler/parsing/tests
May 16 16:07:41 Finished compiler/parsing/tests                                  30s 607MB
May 16 16:07:41 Starting compiler/inference/tests
May 16 16:16:14 Finished compiler/inference/tests                              8m33s   4GB
May 16 16:16:14 Starting compiler/printing/test
May 16 16:19:57 Finished compiler/printing/test                                3m42s   3GB
May 16 16:19:57 Starting icing/flover
May 16 16:31:57 Finished icing/flover                                         11m59s   1GB
May 16 16:31:57 Starting icing/
May 16 17:30:02 Finished icing/                                               58m04s   8GB
May 16 17:30:02 Starting icing/examples
May 16 17:31:31 Finished icing/examples                                        1m29s   6GB
May 16 17:31:31 Starting compiler/repl
May 16 17:44:47 Finished compiler/repl                                        13m15s   5GB
May 16 17:44:47 Starting compiler/bootstrap/translation
May 16 21:51:27 Finished compiler/bootstrap/translation                     4h06m38s  40GB
May 16 21:51:27 Starting unverified/sexpr-bootstrap/x64/64
May 16 22:04:22 Finished unverified/sexpr-bootstrap/x64/64                    12m54s   8GB
May 16 22:04:22 Starting unverified/sexpr-bootstrap/x64/32
May 16 22:14:03 Finished unverified/sexpr-bootstrap/x64/32                     9m40s  10GB
May 16 22:14:03 Starting compiler/benchmarks
May 16 22:14:58 Finished compiler/benchmarks                                     55s 673MB
May 16 22:14:58 Starting compiler/bootstrap/compilation/x64/64 May 16 22:14:58 2643s