Job 1896

CakeML:b22ea8e8ba7e6a7474e33f8273f526a9360cc788
  Merge pull request #883 from CakeML/pan-lemma [May 09 03:44:38]
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 10 08:06:48 Claimed job
May 10 08:06:52 Building HOL
May 10 08:16:41 Starting developers
May 10 08:16:45 Finished developers                                               4s  96MB
May 10 08:16:45 Starting developers/bin
May 10 08:17:14 Finished developers/bin                                          28s   1GB
May 10 08:17:14 Starting semantics/ffi
May 10 08:17:24 Finished semantics/ffi                                            9s 225MB
May 10 08:17:24 Starting semantics
May 10 08:19:33 Finished semantics                                             2m08s   1GB
May 10 08:19:33 Starting semantics/proofs
May 10 08:23:38 Finished semantics/proofs                                      4m04s   4GB
May 10 08:23:38 Starting semantics/alt_semantics
May 10 08:24:01 Finished semantics/alt_semantics                                 23s 473MB
May 10 08:24:02 Starting semantics/alt_semantics/proofs
May 10 08:26:59 Finished semantics/alt_semantics/proofs                        2m57s   2GB
May 10 08:26:59 Starting basis/pure
May 10 08:30:29 Finished basis/pure                                            3m29s 837MB
May 10 08:30:29 Starting translator
May 10 08:33:30 Finished translator                                            3m01s   1GB
May 10 08:33:30 Starting compiler/parsing
May 10 08:34:46 Finished compiler/parsing                                      1m15s   3GB
May 10 08:34:46 Starting characteristic
May 10 08:41:16 Finished characteristic                                        6m29s   2GB
May 10 08:41:16 Starting translator/monadic
May 10 08:43:13 Finished translator/monadic                                    1m57s   1GB
May 10 08:43:14 Starting basis
May 10 09:30:23 Finished basis                                                47m08s  19GB
May 10 09:30:23 Starting compiler/inference
May 10 09:31:51 Finished compiler/inference                                    1m28s   1GB
May 10 09:31:51 Starting compiler/backend/reg_alloc
May 10 09:33:35 Finished compiler/backend/reg_alloc                            1m43s   1GB
May 10 09:33:35 Starting compiler/backend/gc
May 10 09:37:59 Finished compiler/backend/gc                                   4m23s   2GB
May 10 09:37:59 Starting compiler/backend
May 10 09:43:41 Finished compiler/backend                                      5m41s   2GB
May 10 09:43:41 Starting compiler/encoders/asm
May 10 09:44:11 Finished compiler/encoders/asm                                   29s 743MB
May 10 09:44:11 Starting compiler/encoders/x64
May 10 09:45:18 Finished compiler/encoders/x64                                 1m07s   1GB
May 10 09:45:19 Starting compiler/encoders/arm7
May 10 09:47:25 Finished compiler/encoders/arm7                                2m06s   1GB
May 10 09:47:25 Starting compiler/encoders/arm8
May 10 09:48:07 Finished compiler/encoders/arm8                                  42s 958MB
May 10 09:48:07 Starting compiler/encoders/arm8_asl
May 10 12:05:41 Finished compiler/encoders/arm8_asl                         2h17m32s  28GB
May 10 12:05:42 Starting compiler/encoders/mips
May 10 12:07:12 Finished compiler/encoders/mips                                1m30s   1GB
May 10 12:07:12 Starting compiler/encoders/riscv
May 10 12:09:00 Finished compiler/encoders/riscv                               1m48s   1GB
May 10 12:09:01 Starting compiler/encoders/ag32
May 10 12:09:22 Finished compiler/encoders/ag32                                  21s 732MB
May 10 12:09:22 Starting compiler/backend/x64
May 10 12:09:45 Finished compiler/backend/x64                                    22s   1GB
May 10 12:09:45 Starting compiler/backend/arm7
May 10 12:10:09 Finished compiler/backend/arm7                                   24s   1GB
May 10 12:10:09 Starting compiler/backend/arm8
May 10 12:10:32 Finished compiler/backend/arm8                                   22s   1GB
May 10 12:10:32 Starting compiler/backend/mips
May 10 12:10:55 Finished compiler/backend/mips                                   22s   1GB
May 10 12:10:55 Starting compiler/backend/riscv
May 10 12:11:18 Finished compiler/backend/riscv                                  22s   1GB
May 10 12:11:18 Starting compiler/backend/ag32
May 10 12:12:43 Finished compiler/backend/ag32                                 1m25s   1GB
May 10 12:12:43 Starting compiler/parsing/proofs
May 10 12:16:33 Finished compiler/parsing/proofs                               3m49s   1GB
May 10 12:16:33 Starting compiler/inference/proofs
May 10 12:19:04 Finished compiler/inference/proofs                             2m31s 915MB
May 10 12:19:04 Starting compiler/backend/semantics
May 10 12:48:09 Finished compiler/backend/semantics                           29m04s   2GB
May 10 12:48:09 Starting compiler/backend/reg_alloc/proofs
May 10 12:51:44 Finished compiler/backend/reg_alloc/proofs                     3m35s 802MB
May 10 12:51:44 Starting compiler/backend/proofs
May 10 13:43:02 Finished compiler/backend/proofs                              51m16s  20GB
May 10 13:43:02 Starting compiler/backend/serialiser
May 10 13:44:39 Finished compiler/backend/serialiser                           1m36s   2GB
May 10 13:44:39 Starting compiler/encoders/x64/proofs
May 10 13:54:08 Finished compiler/encoders/x64/proofs                          9m29s   4GB
May 10 13:54:09 Starting compiler/encoders/arm7/proofs
May 10 14:07:19 Finished compiler/encoders/arm7/proofs                        13m10s   3GB
May 10 14:07:20 Starting compiler/encoders/arm8/proofs
May 10 14:14:07 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
May 10 14:14:08 Starting compiler/encoders/arm8_asl/proofs
May 10 15:04:11 Finished compiler/encoders/arm8_asl/proofs                    50m01s   8GB
May 10 15:04:12 Starting compiler/encoders/mips/proofs
May 10 15:14:01 Finished compiler/encoders/mips/proofs                         9m49s   2GB
May 10 15:14:01 Starting compiler/encoders/riscv/proofs
May 10 15:22:48 Finished compiler/encoders/riscv/proofs                        8m46s   1GB
May 10 15:22:48 Starting compiler/encoders/ag32/proofs
May 10 15:25:21 Finished compiler/encoders/ag32/proofs                         2m33s 901MB
May 10 15:25:21 Starting compiler/backend/x64/proofs
May 10 15:25:50 Finished compiler/backend/x64/proofs                             28s   1GB
May 10 15:25:50 Starting compiler/backend/arm7/proofs
May 10 15:26:20 Finished compiler/backend/arm7/proofs                            29s   1GB
May 10 15:26:20 Starting compiler/backend/arm8/proofs
May 10 15:26:48 Finished compiler/backend/arm8/proofs                            28s   2GB
May 10 15:26:48 Starting compiler/backend/arm8_asl
May 10 15:27:11 Finished compiler/backend/arm8_asl                               22s   1GB
May 10 15:27:11 Starting compiler/backend/mips/proofs
May 10 15:27:39 Finished compiler/backend/mips/proofs                            27s   1GB
May 10 15:27:39 Starting compiler/backend/riscv/proofs
May 10 15:28:08 Finished compiler/backend/riscv/proofs                           28s   1GB
May 10 15:28:08 Starting compiler/backend/ag32/proofs
May 10 15:40:49 Finished compiler/backend/ag32/proofs                         12m41s   3GB
May 10 15:40:49 Starting compiler/proofs
May 10 15:43:13 Finished compiler/proofs                                       2m24s   3GB
May 10 15:43:14 Starting candle/set-theory
May 10 15:43:48 Finished candle/set-theory                                       34s   1GB
May 10 15:43:48 Starting candle/syntax-lib
May 10 15:44:01 Finished candle/syntax-lib                                       13s 554MB
May 10 15:44:01 Starting candle/standard/syntax
May 10 15:46:03 Finished candle/standard/syntax                                2m01s 929MB
May 10 15:46:03 Starting candle/standard/semantics
May 10 15:47:51 Finished candle/standard/semantics                             1m48s   1GB
May 10 15:47:51 Starting candle/standard/monadic
May 10 15:49:43 Finished candle/standard/monadic                               1m51s   1GB
May 10 15:49:43 Starting candle/standard/ml_kernel
May 10 15:55:49 Finished candle/standard/ml_kernel                             6m06s   3GB
May 10 15:55:50 Starting candle/overloading/syntax
May 10 15:59:00 Finished candle/overloading/syntax                             3m10s   1GB
May 10 15:59:00 Starting candle/overloading/semantics
May 10 16:10:57 Finished candle/overloading/semantics                         11m54s   2GB
May 10 16:10:57 Starting candle/overloading/monadic
May 10 16:13:32 Finished candle/overloading/monadic                            2m34s   1GB
May 10 16:13:32 Starting candle/overloading/ml_kernel
May 10 16:20:39 Finished candle/overloading/ml_kernel                          7m07s   3GB
May 10 16:20:39 Starting candle/overloading/ml_checker
May 10 16:23:05 Finished candle/overloading/ml_checker                         2m25s   2GB
May 10 16:23:05 Starting candle/prover
May 10 16:31:19 Finished candle/prover                                         8m13s   3GB
May 10 16:31:19 Starting pancake
May 10 16:35:08 Finished pancake                                               3m48s   4GB
May 10 16:35:08 Starting pancake/ffi
May 10 16:35:08 Finished pancake/ffi                                              0s  35MB
May 10 16:35:08 Starting pancake/semantics
May 10 16:37:35 Finished pancake/semantics                                     2m27s 922MB
May 10 16:37:36 Starting pancake/proofs
May 10 16:49:42 Finished pancake/proofs                                       12m05s   6GB
May 10 16:49:42 Starting characteristic/examples
May 10 16:51:04 Finished characteristic/examples                               1m21s   3GB
May 10 16:51:04 Starting tutorial/solutions
May 10 17:08:02 Finished tutorial/solutions                                   16m57s   8GB
May 10 17:08:02 Starting translator/monadic/examples
May 10 17:11:57 Finished translator/monadic/examples                           3m53s   2GB
May 10 17:11:57 Starting examples
May 10 17:21:28 Finished examples                                              9m30s   4GB
May 10 17:21:28 Starting examples/compilation/x64
May 10 19:54:21 Finished examples/compilation/x64                           2h32m52s  18GB
May 10 19:54:21 Starting examples/compilation/x64/proofs
May 10 19:57:07 Finished examples/compilation/x64/proofs                       2m46s   3GB
May 10 19:57:07 Starting examples/compilation/ag32
May 10 20:32:17 Finished examples/compilation/ag32                            35m09s   9GB
May 10 20:32:17 Starting examples/compilation/ag32/proofs
May 10 20:33:13 Finished examples/compilation/ag32/proofs                        55s   2GB
May 10 20:33:13 Starting examples/cost
May 10 21:28:56 Finished examples/cost                                        55m41s   9GB
May 10 21:28:56 Starting examples/lpr_checker
May 10 21:29:59 Finished examples/lpr_checker                                  1m03s   1GB
May 10 21:30:00 Starting examples/lpr_checker/array
May 10 21:58:17 Finished examples/lpr_checker/array                           28m17s   6GB
May 10 21:58:17 Starting examples/lpr_checker/array/compilation
May 10 23:21:26 Finished examples/lpr_checker/array/compilation             1h23m07s  31GB
May 10 23:21:26 Starting examples/lpr_checker/array/compilation/proofs
May 10 23:22:55 Finished examples/lpr_checker/array/compilation/proofs         1m29s   6GB
May 10 23:22:55 Starting examples/opentheory
May 10 23:33:02 Finished examples/opentheory                                  10m06s   4GB
May 10 23:33:03 Starting examples/opentheory
May 10 23:33:04 Finished examples/opentheory                                      1s 132MB
May 10 23:33:04 Starting examples/opentheory/compilation
May 11 00:12:47 Finished examples/opentheory/compilation                      39m43s  29GB
May 11 00:12:48 Starting examples/opentheory/compilation/proofs
May 11 00:13:53 Finished examples/opentheory/compilation/proofs                1m05s   2GB
May 11 00:13:53 Starting examples/opentheory/compilation/ag32
May 11 00:52:13 Finished examples/opentheory/compilation/ag32                 38m18s  29GB
May 11 00:52:13 Starting examples/opentheory/compilation/ag32/proofs
May 11 00:53:58 Finished examples/opentheory/compilation/ag32/proofs           1m44s   4GB
May 11 00:53:58 Starting examples/sat_encodings
May 11 00:56:00 Finished examples/sat_encodings                                2m02s 853MB
May 11 00:56:00 Starting examples/sat_encodings/case_studies
May 11 00:57:44 Finished examples/sat_encodings/case_studies                   1m43s 761MB
May 11 00:57:44 Starting examples/sat_encodings/translation
May 11 01:03:32 Finished examples/sat_encodings/translation                    5m47s   3GB
May 11 01:03:32 Starting examples/sat_encodings/translation/compilation
May 11 01:52:37 Finished examples/sat_encodings/translation/compilation       49m03s  18GB
May 11 01:52:37 Starting translator/okasaki-examples
May 11 01:57:23 Finished translator/okasaki-examples                           4m45s   2GB
May 11 01:57:23 Starting translator/other-examples
May 11 01:59:19 Finished translator/other-examples                             1m55s   1GB
May 11 01:59:19 Starting compiler/parsing/tests
May 11 01:59:49 Finished compiler/parsing/tests                                  30s 498MB
May 11 01:59:49 Starting compiler/inference/tests
May 11 02:08:19 Finished compiler/inference/tests                              8m29s   4GB
May 11 02:08:19 Starting compiler/printing/test
May 11 02:12:06 Finished compiler/printing/test                                3m46s   3GB
May 11 02:12:06 Starting compiler/repl
May 11 02:25:05 Finished compiler/repl                                        12m59s   5GB
May 11 02:25:06 Starting compiler/bootstrap/translation
May 11 06:20:45 Finished compiler/bootstrap/translation                     3h55m37s  50GB
May 11 06:20:45 Starting unverified/sexpr-bootstrap/x64/64
May 11 06:33:17 Finished unverified/sexpr-bootstrap/x64/64                    12m30s   8GB
May 11 06:33:17 Starting unverified/sexpr-bootstrap/x64/32
May 11 06:42:57 Finished unverified/sexpr-bootstrap/x64/32                     9m38s  10GB
May 11 06:42:57 Starting compiler/benchmarks
May 11 06:43:53 Finished compiler/benchmarks                                     55s 673MB
May 11 06:43:53 Starting compiler/bootstrap/compilation/x64/64
May 12 01:26:17 Finished compiler/bootstrap/compilation/x64/64             18h42m21s  64GB
May 12 01:26:17 Starting compiler/bootstrap/compilation/x64/64/proofs
May 12 01:43:56 Finished compiler/bootstrap/compilation/x64/64/proofs         17m39s  31GB
May 12 01:43:56 Starting compiler/bootstrap/compilation/x64/32
May 12 15:33:26 Finished compiler/bootstrap/compilation/x64/32             13h49m27s  64GB
May 12 15:33:26 Starting compiler/bootstrap/compilation/x64/32/proofs
May 12 15:37:57 Finished compiler/bootstrap/compilation/x64/32/proofs          4m30s  16GB
May 12 15:37:58 Starting compiler/bootstrap/compilation/ag32/32
May 13 05:06:57 Finished compiler/bootstrap/compilation/ag32/32            13h28m58s  64GB
May 13 05:06:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 13 05:22:58 Finished compiler/bootstrap/compilation/ag32/32/proofs        16m01s  20GB
May 13 05:22:59 SUCCESS