Job 2091

CakeML:4aa53b5a0f34ba8cf84d8ac84f2e288342af905c
  pancake: some cleanup [Feb 03 06:30:09]
#923 (pan_misc_lemmas)
Merging into:0a80d59e3ef322e4ad28193e97b5d425c5fd2df4
  Merge pull request #922 from CakeML/unzip-fix [Jan 22 17:17:11]
HOL:b449b82bffe8efeaf753c77d8132f37c38d0e1a7
  Undo 27187edc1 [Jan 28 03:02:55]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 03 20:48:10 Claimed job
Feb 03 20:48:15 Reusing HOL
Feb 03 20:48:55 Starting developers
Feb 03 20:49:01 Finished developers                                               5s 137MB
Feb 03 20:49:01 Starting developers/bin
Feb 03 20:49:07 Finished developers/bin                                           6s   1GB
Feb 03 20:49:07 Starting compiler/proofs
Feb 04 16:16:18 Resuming compiler/proofs
Feb 04 16:20:14 Finished compiler/proofs                                       3m56s   3GB
Feb 04 16:20:14 Starting compiler/bootstrap/translation
Feb 04 23:55:28 Finished compiler/bootstrap/translation                     7h35m11s  44GB
Feb 04 23:55:28 Starting semantics/ffi
Feb 04 23:55:35 Finished semantics/ffi                                            6s 223MB
Feb 04 23:55:35 Starting semantics
Feb 04 23:55:36 Finished semantics                                                1s  19MB
Feb 04 23:55:36 Starting semantics/proofs
Feb 04 23:56:11 Finished semantics/proofs                                        34s   1GB
Feb 04 23:56:11 Starting semantics/alt_semantics
Feb 04 23:56:42 Finished semantics/alt_semantics                                 30s 744MB
Feb 04 23:56:42 Starting semantics/alt_semantics/proofs
Feb 05 00:08:25 Finished semantics/alt_semantics/proofs                       11m42s   1GB
Feb 05 00:08:25 Starting basis/pure
Feb 05 00:08:26 Finished basis/pure                                               1s  20MB
Feb 05 00:08:27 Starting translator
Feb 05 00:10:17 Finished translator                                            1m50s   1GB
Feb 05 00:10:17 Starting compiler/parsing
Feb 05 00:10:19 Finished compiler/parsing                                         1s  22MB
Feb 05 00:10:19 Starting characteristic
Feb 05 00:10:21 Finished characteristic                                           1s  23MB
Feb 05 00:10:21 Starting translator/monadic
Feb 05 00:10:23 Finished translator/monadic                                       1s  23MB
Feb 05 00:10:23 Starting basis
Feb 05 00:13:52 Finished basis                                                 3m29s   2GB
Feb 05 00:13:53 Starting compiler/inference
Feb 05 00:13:54 Finished compiler/inference                                       1s  23MB
Feb 05 00:13:54 Starting compiler/backend/reg_alloc
Feb 05 00:13:56 Finished compiler/backend/reg_alloc                               1s  19MB
Feb 05 00:13:56 Starting compiler/backend/gc
Feb 05 00:13:58 Finished compiler/backend/gc                                      2s  26MB
Feb 05 00:13:58 Starting compiler/backend
Feb 05 00:14:11 Finished compiler/backend                                        12s 774MB
Feb 05 00:14:11 Starting compiler/encoders/asm
Feb 05 00:14:13 Finished compiler/encoders/asm                                    1s  21MB
Feb 05 00:14:13 Starting compiler/encoders/x64
Feb 05 00:14:15 Finished compiler/encoders/x64                                    1s  21MB
Feb 05 00:14:15 Starting compiler/encoders/arm7
Feb 05 00:14:17 Finished compiler/encoders/arm7                                   1s  18MB
Feb 05 00:14:17 Starting compiler/encoders/arm8
Feb 05 00:14:19 Finished compiler/encoders/arm8                                   1s  21MB
Feb 05 00:14:19 Starting compiler/encoders/arm8_asl
Feb 05 00:17:34 Finished compiler/encoders/arm8_asl                            3m15s   1GB
Feb 05 00:17:34 Starting compiler/encoders/mips
Feb 05 00:17:36 Finished compiler/encoders/mips                                   1s  22MB
Feb 05 00:17:36 Starting compiler/encoders/riscv
Feb 05 00:17:38 Finished compiler/encoders/riscv                                  1s  24MB
Feb 05 00:17:38 Starting compiler/encoders/ag32
Feb 05 00:17:40 Finished compiler/encoders/ag32                                   1s  22MB
Feb 05 00:17:40 Starting compiler/backend/x64
Feb 05 00:17:42 Finished compiler/backend/x64                                     2s  29MB
Feb 05 00:17:42 Starting compiler/backend/arm7
Feb 05 00:17:44 Finished compiler/backend/arm7                                    2s  27MB
Feb 05 00:17:44 Starting compiler/backend/arm8
Feb 05 00:17:47 Finished compiler/backend/arm8                                    2s  21MB
Feb 05 00:17:47 Starting compiler/backend/mips
Feb 05 00:17:49 Finished compiler/backend/mips                                    2s  28MB
Feb 05 00:17:49 Starting compiler/backend/riscv
Feb 05 00:17:51 Finished compiler/backend/riscv                                   2s  22MB
Feb 05 00:17:51 Starting compiler/backend/ag32
Feb 05 00:19:19 Finished compiler/backend/ag32                                 1m27s   1GB
Feb 05 00:19:19 Starting compiler/parsing/proofs
Feb 05 00:19:21 Finished compiler/parsing/proofs                                  1s  19MB
Feb 05 00:19:21 Starting compiler/inference/proofs
Feb 05 00:19:23 Finished compiler/inference/proofs                                1s  24MB
Feb 05 00:19:23 Starting compiler/backend/semantics
Feb 05 00:20:36 Finished compiler/backend/semantics                            1m13s   1GB
Feb 05 00:20:36 Starting compiler/backend/reg_alloc/proofs
Feb 05 00:20:38 Finished compiler/backend/reg_alloc/proofs                        1s  25MB
Feb 05 00:20:38 Starting compiler/backend/proofs
Feb 05 00:21:37 Finished compiler/backend/proofs                                 58s   3GB
Feb 05 00:21:37 Starting compiler/backend/serialiser
Feb 05 00:21:40 Finished compiler/backend/serialiser                              2s  42MB
Feb 05 00:21:40 Starting compiler/encoders/x64/proofs
Feb 05 00:31:28 Finished compiler/encoders/x64/proofs                          9m47s   7GB
Feb 05 00:31:28 Starting compiler/encoders/arm7/proofs
Feb 05 00:45:13 Finished compiler/encoders/arm7/proofs                        13m44s   4GB
Feb 05 00:45:13 Starting compiler/encoders/arm8/proofs
Feb 05 00:52:16 Finished compiler/encoders/arm8/proofs                         7m03s   1GB
Feb 05 00:52:16 Starting compiler/encoders/arm8_asl/proofs
Feb 05 01:07:58 Finished compiler/encoders/arm8_asl/proofs                    15m41s   2GB
Feb 05 01:07:59 Starting compiler/encoders/mips/proofs
Feb 05 01:18:26 Finished compiler/encoders/mips/proofs                        10m27s   2GB
Feb 05 01:18:26 Starting compiler/encoders/riscv/proofs
Feb 05 01:27:28 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Feb 05 01:27:28 Starting compiler/encoders/ag32/proofs
Feb 05 01:30:09 Finished compiler/encoders/ag32/proofs                         2m41s 946MB
Feb 05 01:30:09 Starting compiler/backend/x64/proofs
Feb 05 01:30:40 Finished compiler/backend/x64/proofs                             31s   2GB
Feb 05 01:30:41 Starting compiler/backend/arm7/proofs
Feb 05 01:31:13 Finished compiler/backend/arm7/proofs                            32s   2GB
Feb 05 01:31:13 Starting compiler/backend/arm8/proofs
Feb 05 01:31:45 Finished compiler/backend/arm8/proofs                            31s   2GB
Feb 05 01:31:45 Starting compiler/backend/arm8_asl
Feb 05 01:32:09 Finished compiler/backend/arm8_asl                               24s   2GB
Feb 05 01:32:09 Starting compiler/backend/mips/proofs
Feb 05 01:32:40 Finished compiler/backend/mips/proofs                            31s   1GB
Feb 05 01:32:41 Starting compiler/backend/riscv/proofs
Feb 05 01:33:13 Finished compiler/backend/riscv/proofs                           32s   2GB
Feb 05 01:33:14 Starting compiler/backend/ag32/proofs
Feb 05 01:46:47 Finished compiler/backend/ag32/proofs                         13m33s   3GB
Feb 05 01:46:47 Starting candle/set-theory
Feb 05 01:47:27 Finished candle/set-theory                                       39s   1GB
Feb 05 01:47:27 Starting candle/syntax-lib
Feb 05 01:47:28 Finished candle/syntax-lib                                        1s  21MB
Feb 05 01:47:28 Starting candle/standard/syntax
Feb 05 01:47:39 Finished candle/standard/syntax                                  10s 781MB
Feb 05 01:47:39 Starting candle/standard/semantics
Feb 05 01:49:39 Finished candle/standard/semantics                             1m59s   1GB
Feb 05 01:49:39 Starting candle/standard/monadic
Feb 05 01:49:41 Finished candle/standard/monadic                                  1s  29MB
Feb 05 01:49:41 Starting candle/standard/ml_kernel
Feb 05 01:51:17 Finished candle/standard/ml_kernel                             1m36s   2GB
Feb 05 01:51:17 Starting candle/overloading/syntax
Feb 05 01:54:39 Finished candle/overloading/syntax                             3m21s   1GB
Feb 05 01:54:39 Starting candle/overloading/semantics
Feb 05 02:06:38 Finished candle/overloading/semantics                         11m59s   3GB
Feb 05 02:06:38 Starting candle/overloading/monadic
Feb 05 02:09:23 Finished candle/overloading/monadic                            2m42s   1GB
Feb 05 02:09:23 Starting candle/overloading/ml_kernel
Feb 05 02:17:07 Finished candle/overloading/ml_kernel                          7m43s   3GB
Feb 05 02:17:07 Starting candle/overloading/ml_checker
Feb 05 02:19:39 Finished candle/overloading/ml_checker                         2m32s   3GB
Feb 05 02:19:39 Starting candle/prover
Feb 05 02:29:33 Finished candle/prover                                         9m54s   3GB
Feb 05 02:29:33 Starting pancake
Feb 05 02:32:58 Finished pancake                                               3m24s   4GB
Feb 05 02:32:58 Starting pancake/ffi
Feb 05 02:32:58 Finished pancake/ffi                                              0s  13MB
Feb 05 02:32:58 Starting pancake/semantics
Feb 05 02:35:26 Finished pancake/semantics                                     2m27s   1GB
Feb 05 02:35:26 Starting pancake/proofs
Feb 05 02:39:41 Finished pancake/proofs                                        4m14s   1GB
Feb 05 02:39:41 Starting characteristic/examples
Feb 05 02:41:13 Finished characteristic/examples                               1m32s   2GB
Feb 05 02:41:13 Starting tutorial/solutions
Feb 05 02:56:42 Finished tutorial/solutions                                   15m29s   8GB
Feb 05 02:56:42 Starting translator/monadic/examples
Feb 05 03:00:44 Finished translator/monadic/examples                           4m01s   2GB
Feb 05 03:00:44 Starting examples
Feb 05 03:16:19 Finished examples                                             15m33s   5GB
Feb 05 03:16:19 Starting examples/compilation/x64
Feb 05 05:15:33 Finished examples/compilation/x64                           1h59m13s  14GB
Feb 05 05:15:33 Starting examples/compilation/x64/proofs
Feb 05 05:18:07 Finished examples/compilation/x64/proofs                       2m33s   4GB
Feb 05 05:18:07 Starting examples/compilation/ag32
Feb 05 05:48:43 Finished examples/compilation/ag32                            30m35s   9GB
Feb 05 05:48:43 Starting examples/compilation/ag32/proofs
Feb 05 05:49:44 Finished examples/compilation/ag32/proofs                      1m01s   5GB
Feb 05 05:49:44 Starting examples/compilation/to_word
Feb 05 05:53:03 Finished examples/compilation/to_word                          3m18s   6GB
Feb 05 05:53:03 Starting examples/lpr_checker
Feb 05 05:54:08 Finished examples/lpr_checker                                  1m04s   1GB
Feb 05 05:54:08 Starting examples/lpr_checker/array
Feb 05 06:28:35 Finished examples/lpr_checker/array                           34m25s   6GB
Feb 05 06:28:35 Starting examples/lpr_checker/array/compilation
Feb 05 07:07:06 Finished examples/lpr_checker/array/compilation               38m30s  24GB
Feb 05 07:07:06 Starting examples/lpr_checker/array/compilation/proofs
Feb 05 07:08:31 Finished examples/lpr_checker/array/compilation/proofs         1m25s   5GB
Feb 05 07:08:31 Starting examples/opentheory
Feb 05 07:19:36 Finished examples/opentheory                                  11m04s   3GB
Feb 05 07:19:36 Starting examples/opentheory
Feb 05 07:19:38 Finished examples/opentheory                                      1s  25MB
Feb 05 07:19:38 Starting examples/opentheory/compilation
Feb 05 07:55:52 Finished examples/opentheory/compilation                      36m13s  29GB
Feb 05 07:55:53 Starting examples/opentheory/compilation/proofs
Feb 05 07:56:55 Finished examples/opentheory/compilation/proofs                1m02s   4GB
Feb 05 07:56:55 Starting examples/opentheory/compilation/ag32
Feb 05 08:29:29 Finished examples/opentheory/compilation/ag32                 32m33s  29GB
Feb 05 08:29:29 Starting examples/opentheory/compilation/ag32/proofs
Feb 05 08:31:23 Finished examples/opentheory/compilation/ag32/proofs           1m53s   7GB
Feb 05 08:31:23 Starting examples/sat_encodings
Feb 05 08:33:24 Finished examples/sat_encodings                                2m00s 876MB
Feb 05 08:33:24 Starting examples/sat_encodings/case_studies
Feb 05 08:35:15 Finished examples/sat_encodings/case_studies                   1m50s   1GB
Feb 05 08:35:15 Starting examples/sat_encodings/translation
Feb 05 08:41:21 Finished examples/sat_encodings/translation                    6m05s   3GB
Feb 05 08:41:21 Starting examples/sat_encodings/translation/compilation
Feb 05 09:26:05 Finished examples/sat_encodings/translation/compilation       44m43s  22GB
Feb 05 09:26:06 Starting examples/deflate
Feb 05 09:27:05 Finished examples/deflate                                        59s 852MB
Feb 05 09:27:05 Starting examples/deflate/translation
Feb 05 09:28:44 Finished examples/deflate/translation                          1m39s   3GB
Feb 05 09:28:44 Starting examples/deflate/translation/compilation
Feb 05 09:48:24 Finished examples/deflate/translation/compilation             19m39s  11GB
Feb 05 09:48:24 Starting translator/okasaki-examples
Feb 05 09:53:38 Finished translator/okasaki-examples                           5m13s   1GB
Feb 05 09:53:38 Starting translator/other-examples
Feb 05 09:54:30 Finished translator/other-examples                               52s   1GB
Feb 05 09:54:30 Starting compiler/parsing/tests
Feb 05 09:55:03 Finished compiler/parsing/tests                                  32s 743MB
Feb 05 09:55:03 Starting compiler/inference/tests
Feb 05 10:03:29 Finished compiler/inference/tests                              8m26s   5GB
Feb 05 10:03:29 Starting compiler/printing/test
Feb 05 10:07:13 Finished compiler/printing/test                                3m44s   3GB
Feb 05 10:07:13 Starting icing/flover
Feb 05 10:49:54 Finished icing/flover                                         42m39s   2GB
Feb 05 10:49:54 Starting icing/
Feb 05 11:49:42 Finished icing/                                               59m47s   8GB
Feb 05 11:49:42 Starting icing/examples
Feb 05 11:51:35 Finished icing/examples                                        1m51s   7GB
Feb 05 11:51:35 Starting compiler/repl
Feb 05 12:00:05 Finished compiler/repl                                         8m30s   4GB
Feb 05 12:00:06 Starting unverified/sexpr-bootstrap/x64/64
Feb 05 12:12:49 Finished unverified/sexpr-bootstrap/x64/64                    12m43s  12GB
Feb 05 12:12:49 Starting unverified/sexpr-bootstrap/x64/32
Feb 05 12:23:12 Finished unverified/sexpr-bootstrap/x64/32                    10m22s  11GB
Feb 05 12:23:12 Starting compiler/benchmarks
Feb 05 12:23:16 Finished compiler/benchmarks                                      4s  35MB
Feb 05 12:23:16 Starting compiler/bootstrap/compilation/x64/64
Feb 05 23:24:27 Finished compiler/bootstrap/compilation/x64/64             11h01m10s  64GB
Feb 05 23:24:27 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 05 23:45:37 Finished compiler/bootstrap/compilation/x64/64/proofs         21m09s  34GB
Feb 05 23:45:37 Starting compiler/bootstrap/compilation/x64/32
Feb 06 06:18:48 Finished compiler/bootstrap/compilation/x64/32              6h33m09s  64GB
Feb 06 06:18:48 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 06 06:21:50 Finished compiler/bootstrap/compilation/x64/32/proofs          3m02s  17GB
Feb 06 06:21:51 Starting compiler/bootstrap/compilation/ag32/32
Feb 06 13:10:26 Finished compiler/bootstrap/compilation/ag32/32             6h48m34s  64GB
Feb 06 13:10:26 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 06 13:16:51 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m24s  35GB
Feb 06 13:16:51 SUCCESS