Job 2085

CakeML:8c8f91d0ab4733db699d2b7b8cd1060ccd0daf3a
  pancake: misc lemmas for pan_to_target proof [Jan 23 22:52:16]
#923 (pan_misc_lemmas)
Merging into:0a80d59e3ef322e4ad28193e97b5d425c5fd2df4
  Merge pull request #922 from CakeML/unzip-fix [Jan 22 17:17:11]
HOL:1c1bd854c5fd8aae152dd0bc8f0acea9bad53ffa
  Make some theorems in set_relation automatic rewrites [Jan 18 22:09:17]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Jan 24 15:51:44 Claimed job
Jan 24 15:51:53 Building HOL
Jan 24 16:04:16 Starting developers
Jan 24 16:04:22 Finished developers                                               5s  91MB
Jan 24 16:04:22 Starting developers/bin
Jan 24 16:04:28 Finished developers/bin                                           6s   1GB
Jan 24 16:04:28 Starting compiler/proofs
Jan 24 17:56:07 Finished compiler/proofs                                    1h51m37s  21GB
Jan 24 17:56:07 Starting compiler/bootstrap/translation
Jan 25 01:25:07 Finished compiler/bootstrap/translation                     7h28m58s  38GB
Jan 25 01:25:07 Starting semantics/ffi
Jan 25 01:25:12 Finished semantics/ffi                                            4s 415MB
Jan 25 01:25:12 Starting semantics
Jan 25 01:25:14 Finished semantics                                                1s  20MB
Jan 25 01:25:14 Starting semantics/proofs
Jan 25 01:25:49 Finished semantics/proofs                                        34s   1GB
Jan 25 01:25:49 Starting semantics/alt_semantics
Jan 25 01:26:20 Finished semantics/alt_semantics                                 30s 663MB
Jan 25 01:26:20 Starting semantics/alt_semantics/proofs
Jan 25 01:38:10 Finished semantics/alt_semantics/proofs                       11m49s   1GB
Jan 25 01:38:10 Starting basis/pure
Jan 25 01:38:11 Finished basis/pure                                               1s  22MB
Jan 25 01:38:11 Starting translator
Jan 25 01:40:02 Finished translator                                            1m50s   1GB
Jan 25 01:40:02 Starting compiler/parsing
Jan 25 01:40:04 Finished compiler/parsing                                         1s  19MB
Jan 25 01:40:04 Starting characteristic
Jan 25 01:40:07 Finished characteristic                                           1s  24MB
Jan 25 01:40:07 Starting translator/monadic
Jan 25 01:40:09 Finished translator/monadic                                       1s  20MB
Jan 25 01:40:09 Starting basis
Jan 25 01:43:39 Finished basis                                                 3m29s   2GB
Jan 25 01:43:39 Starting compiler/inference
Jan 25 01:43:41 Finished compiler/inference                                       1s  20MB
Jan 25 01:43:41 Starting compiler/backend/reg_alloc
Jan 25 01:43:43 Finished compiler/backend/reg_alloc                               1s  18MB
Jan 25 01:43:43 Starting compiler/backend/gc
Jan 25 01:43:45 Finished compiler/backend/gc                                      2s  23MB
Jan 25 01:43:45 Starting compiler/backend
Jan 25 01:43:58 Finished compiler/backend                                        12s 757MB
Jan 25 01:43:58 Starting compiler/encoders/asm
Jan 25 01:44:00 Finished compiler/encoders/asm                                    1s  22MB
Jan 25 01:44:00 Starting compiler/encoders/x64
Jan 25 01:44:02 Finished compiler/encoders/x64                                    1s  25MB
Jan 25 01:44:02 Starting compiler/encoders/arm7
Jan 25 01:44:04 Finished compiler/encoders/arm7                                   1s  24MB
Jan 25 01:44:04 Starting compiler/encoders/arm8
Jan 25 01:44:06 Finished compiler/encoders/arm8                                   1s  25MB
Jan 25 01:44:06 Starting compiler/encoders/arm8_asl
Jan 25 04:09:20 Finished compiler/encoders/arm8_asl                         2h25m13s  46GB
Jan 25 04:09:21 Starting compiler/encoders/mips
Jan 25 04:09:22 Finished compiler/encoders/mips                                   1s  19MB
Jan 25 04:09:23 Starting compiler/encoders/riscv
Jan 25 04:09:24 Finished compiler/encoders/riscv                                  1s  22MB
Jan 25 04:09:24 Starting compiler/encoders/ag32
Jan 25 04:09:26 Finished compiler/encoders/ag32                                   1s  21MB
Jan 25 04:09:26 Starting compiler/backend/x64
Jan 25 04:09:29 Finished compiler/backend/x64                                     2s  26MB
Jan 25 04:09:29 Starting compiler/backend/arm7
Jan 25 04:09:31 Finished compiler/backend/arm7                                    2s  24MB
Jan 25 04:09:32 Starting compiler/backend/arm8
Jan 25 04:09:34 Finished compiler/backend/arm8                                    2s  23MB
Jan 25 04:09:34 Starting compiler/backend/mips
Jan 25 04:09:36 Finished compiler/backend/mips                                    2s  23MB
Jan 25 04:09:36 Starting compiler/backend/riscv
Jan 25 04:09:39 Finished compiler/backend/riscv                                   2s  28MB
Jan 25 04:09:39 Starting compiler/backend/ag32
Jan 25 04:11:07 Finished compiler/backend/ag32                                 1m28s   1GB
Jan 25 04:11:07 Starting compiler/parsing/proofs
Jan 25 04:11:09 Finished compiler/parsing/proofs                                  1s  20MB
Jan 25 04:11:09 Starting compiler/inference/proofs
Jan 25 04:11:11 Finished compiler/inference/proofs                                1s  20MB
Jan 25 04:11:11 Starting compiler/backend/semantics
Jan 25 04:12:25 Finished compiler/backend/semantics                            1m13s   1GB
Jan 25 04:12:25 Starting compiler/backend/reg_alloc/proofs
Jan 25 04:12:27 Finished compiler/backend/reg_alloc/proofs                        1s  19MB
Jan 25 04:12:27 Starting compiler/backend/proofs
Jan 25 04:13:24 Finished compiler/backend/proofs                                 57s   2GB
Jan 25 04:13:24 Starting compiler/backend/serialiser
Jan 25 04:13:27 Finished compiler/backend/serialiser                              2s  41MB
Jan 25 04:13:27 Starting compiler/encoders/x64/proofs
Jan 25 04:23:16 Finished compiler/encoders/x64/proofs                          9m48s   6GB
Jan 25 04:23:16 Starting compiler/encoders/arm7/proofs
Jan 25 04:36:52 Finished compiler/encoders/arm7/proofs                        13m35s   6GB
Jan 25 04:36:52 Starting compiler/encoders/arm8/proofs
Jan 25 04:43:51 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Jan 25 04:43:51 Starting compiler/encoders/arm8_asl/proofs
Jan 25 05:36:21 Finished compiler/encoders/arm8_asl/proofs                    52m29s   8GB
Jan 25 05:36:21 Starting compiler/encoders/mips/proofs
Jan 25 05:46:44 Finished compiler/encoders/mips/proofs                        10m23s   3GB
Jan 25 05:46:45 Starting compiler/encoders/riscv/proofs
Jan 25 05:55:40 Finished compiler/encoders/riscv/proofs                        8m55s   2GB
Jan 25 05:55:41 Starting compiler/encoders/ag32/proofs
Jan 25 05:58:20 Finished compiler/encoders/ag32/proofs                         2m38s 964MB
Jan 25 05:58:20 Starting compiler/backend/x64/proofs
Jan 25 05:58:51 Finished compiler/backend/x64/proofs                             30s   2GB
Jan 25 05:58:51 Starting compiler/backend/arm7/proofs
Jan 25 05:59:23 Finished compiler/backend/arm7/proofs                            32s   2GB
Jan 25 05:59:23 Starting compiler/backend/arm8/proofs
Jan 25 05:59:54 Finished compiler/backend/arm8/proofs                            31s   2GB
Jan 25 05:59:54 Starting compiler/backend/arm8_asl
Jan 25 06:00:18 Finished compiler/backend/arm8_asl                               23s   1GB
Jan 25 06:00:18 Starting compiler/backend/mips/proofs
Jan 25 06:00:50 Finished compiler/backend/mips/proofs                            31s   1GB
Jan 25 06:00:50 Starting compiler/backend/riscv/proofs
Jan 25 06:01:23 Finished compiler/backend/riscv/proofs                           33s   2GB
Jan 25 06:01:23 Starting compiler/backend/ag32/proofs
Jan 25 06:14:55 Finished compiler/backend/ag32/proofs                         13m31s   3GB
Jan 25 06:14:55 Starting candle/set-theory
Jan 25 06:15:35 Finished candle/set-theory                                       39s   1GB
Jan 25 06:15:35 Starting candle/syntax-lib
Jan 25 06:15:37 Finished candle/syntax-lib                                        1s  26MB
Jan 25 06:15:37 Starting candle/standard/syntax
Jan 25 06:15:47 Finished candle/standard/syntax                                  10s 802MB
Jan 25 06:15:48 Starting candle/standard/semantics
Jan 25 06:17:46 Finished candle/standard/semantics                             1m58s   1GB
Jan 25 06:17:46 Starting candle/standard/monadic
Jan 25 06:17:48 Finished candle/standard/monadic                                  1s  26MB
Jan 25 06:17:48 Starting candle/standard/ml_kernel
Jan 25 06:19:37 Finished candle/standard/ml_kernel                             1m49s   3GB
Jan 25 06:19:38 Starting candle/overloading/syntax
Jan 25 06:22:58 Finished candle/overloading/syntax                             3m20s   1GB
Jan 25 06:22:58 Starting candle/overloading/semantics
Jan 25 06:35:06 Finished candle/overloading/semantics                         12m08s   2GB
Jan 25 06:35:06 Starting candle/overloading/monadic
Jan 25 06:37:48 Finished candle/overloading/monadic                            2m40s   1GB
Jan 25 06:37:48 Starting candle/overloading/ml_kernel
Jan 25 06:45:41 Finished candle/overloading/ml_kernel                          7m53s   3GB
Jan 25 06:45:42 Starting candle/overloading/ml_checker
Jan 25 06:48:15 Finished candle/overloading/ml_checker                         2m33s   3GB
Jan 25 06:48:15 Starting candle/prover
Jan 25 06:58:08 Finished candle/prover                                         9m52s   3GB
Jan 25 06:58:08 Starting pancake
Jan 25 07:01:36 Finished pancake                                               3m27s   3GB
Jan 25 07:01:36 Starting pancake/ffi
Jan 25 07:01:37 Finished pancake/ffi                                              0s  13MB
Jan 25 07:01:37 Starting pancake/semantics
Jan 25 07:04:04 Finished pancake/semantics                                     2m27s   1GB
Jan 25 07:04:04 Starting pancake/proofs
Jan 25 07:08:19 Finished pancake/proofs                                        4m14s   3GB
Jan 25 07:08:19 Starting characteristic/examples
Jan 25 07:09:49 Finished characteristic/examples                               1m30s   2GB
Jan 25 07:09:49 Starting tutorial/solutions
Jan 25 07:24:59 Finished tutorial/solutions                                   15m09s   9GB
Jan 25 07:24:59 Starting translator/monadic/examples
Jan 25 07:28:59 Finished translator/monadic/examples                           3m59s   3GB
Jan 25 07:29:00 Starting examples
Jan 25 07:44:58 Finished examples                                             15m57s   4GB
Jan 25 07:44:58 Starting examples/compilation/x64
Jan 25 09:44:49 Finished examples/compilation/x64                           1h59m49s  13GB
Jan 25 09:44:49 Starting examples/compilation/x64/proofs
Jan 25 09:47:21 Finished examples/compilation/x64/proofs                       2m31s   4GB
Jan 25 09:47:21 Starting examples/compilation/ag32
Jan 25 10:17:53 Finished examples/compilation/ag32                            30m31s   7GB
Jan 25 10:17:53 Starting examples/compilation/ag32/proofs
Jan 25 10:18:56 Finished examples/compilation/ag32/proofs                      1m02s   5GB
Jan 25 10:18:56 Starting examples/compilation/to_word
Jan 25 10:22:24 Finished examples/compilation/to_word                          3m28s   5GB
Jan 25 10:22:25 Starting examples/lpr_checker
Jan 25 10:23:28 Finished examples/lpr_checker                                  1m03s   1GB
Jan 25 10:23:28 Starting examples/lpr_checker/array
Jan 25 10:58:02 Finished examples/lpr_checker/array                           34m31s   5GB
Jan 25 10:58:02 Starting examples/lpr_checker/array/compilation
Jan 25 11:36:44 Finished examples/lpr_checker/array/compilation               38m42s  23GB
Jan 25 11:36:44 Starting examples/lpr_checker/array/compilation/proofs
Jan 25 11:38:15 Finished examples/lpr_checker/array/compilation/proofs         1m30s   7GB
Jan 25 11:38:15 Starting examples/opentheory
Jan 25 11:49:03 Finished examples/opentheory                                  10m47s   3GB
Jan 25 11:49:03 Starting examples/opentheory
Jan 25 11:49:05 Finished examples/opentheory                                      1s  32MB
Jan 25 11:49:05 Starting examples/opentheory/compilation
Jan 25 12:25:23 Finished examples/opentheory/compilation                      36m17s  26GB
Jan 25 12:25:23 Starting examples/opentheory/compilation/proofs
Jan 25 12:26:28 Finished examples/opentheory/compilation/proofs                1m05s   5GB
Jan 25 12:26:28 Starting examples/opentheory/compilation/ag32
Jan 25 12:59:23 Finished examples/opentheory/compilation/ag32                 32m54s  27GB
Jan 25 12:59:23 Starting examples/opentheory/compilation/ag32/proofs
Jan 25 13:01:17 Finished examples/opentheory/compilation/ag32/proofs           1m53s   8GB
Jan 25 13:01:17 Starting examples/sat_encodings
Jan 25 13:03:18 Finished examples/sat_encodings                                2m00s 875MB
Jan 25 13:03:18 Starting examples/sat_encodings/case_studies
Jan 25 13:05:07 Finished examples/sat_encodings/case_studies                   1m48s   1GB
Jan 25 13:05:07 Starting examples/sat_encodings/translation
Jan 25 13:11:12 Finished examples/sat_encodings/translation                    6m03s   3GB
Jan 25 13:11:12 Starting examples/sat_encodings/translation/compilation
Jan 25 13:56:42 Finished examples/sat_encodings/translation/compilation       45m29s  22GB
Jan 25 13:56:42 Starting examples/deflate
Jan 25 13:57:42 Finished examples/deflate                                        59s 823MB
Jan 25 13:57:42 Starting examples/deflate/translation
Jan 25 13:59:22 Finished examples/deflate/translation                          1m39s   3GB
Jan 25 13:59:22 Starting examples/deflate/translation/compilation
Jan 25 14:18:52 Finished examples/deflate/translation/compilation             19m29s  15GB
Jan 25 14:18:52 Starting translator/okasaki-examples
Jan 25 14:24:05 Finished translator/okasaki-examples                           5m12s   1GB
Jan 25 14:24:05 Starting translator/other-examples
Jan 25 14:26:50 Finished translator/other-examples                             2m44s   1GB
Jan 25 14:26:50 Starting compiler/parsing/tests
Jan 25 14:27:22 Finished compiler/parsing/tests                                  31s 933MB
Jan 25 14:27:22 Starting compiler/inference/tests
Jan 25 14:36:35 Finished compiler/inference/tests                              9m12s   7GB
Jan 25 14:36:35 Starting compiler/printing/test
Jan 25 14:40:33 Finished compiler/printing/test                                3m57s   3GB
Jan 25 14:40:33 Starting icing/flover
Jan 25 15:25:10 Finished icing/flover                                         44m35s   2GB
Jan 25 15:25:10 Starting icing/
Jan 25 16:37:16 Finished icing/                                             1h12m05s   8GB
Jan 25 16:37:17 Starting icing/examples
Jan 25 16:39:12 Finished icing/examples                                        1m55s   5GB
Jan 25 16:39:13 Starting compiler/repl
Jan 25 16:48:03 Finished compiler/repl                                         8m50s   4GB
Jan 25 16:48:03 Starting unverified/sexpr-bootstrap/x64/64
Jan 25 17:01:17 Finished unverified/sexpr-bootstrap/x64/64                    13m13s  14GB
Jan 25 17:01:17 Starting unverified/sexpr-bootstrap/x64/32
Jan 25 17:11:41 Finished unverified/sexpr-bootstrap/x64/32                    10m24s  12GB
Jan 25 17:11:41 Starting compiler/benchmarks
Jan 25 17:11:46 Finished compiler/benchmarks                                      4s  57MB
Jan 25 17:11:46 Starting compiler/bootstrap/compilation/x64/64
Jan 26 05:20:01 Finished compiler/bootstrap/compilation/x64/64             12h08m14s  43GB
Jan 26 05:20:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 26 05:39:00 Finished compiler/bootstrap/compilation/x64/64/proofs         18m58s  30GB
Jan 26 05:39:01 Starting compiler/bootstrap/compilation/x64/32
Jan 26 12:12:51 Finished compiler/bootstrap/compilation/x64/32              6h33m49s  64GB
Jan 26 12:12:51 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 26 12:15:25 Finished compiler/bootstrap/compilation/x64/32/proofs          2m33s  15GB
Jan 26 12:15:25 Starting compiler/bootstrap/compilation/ag32/32
Jan 26 18:58:40 Finished compiler/bootstrap/compilation/ag32/32             6h43m14s  64GB
Jan 26 18:58:40 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 26 19:04:40 Finished compiler/bootstrap/compilation/ag32/32/proofs         5m59s  28GB
Jan 26 19:04:40 SUCCESS