Job 1889

CakeML:06cd5853339d9140de7599991146fa3b095aebee
  Add a simple property about Pancake semantics [May 06 06:12:30]
#883 (pan-lemma)
Merging into:d49028c882e2061b0b85fe1f775e9d1c157b9b23
  Merge pull request #882 from mktnk3/time_to_pan_cleanup [May 02 07:00:59]
HOL:9ef7738eaecdb725492f0929f6b270d1f4e63a40
  Teach Holmake and Parse.sml about the tmux terminal [Apr 28 21:56:05]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

May 06 07:53:37 Claimed job
May 06 07:53:40 Reusing HOL
May 06 07:53:54 Starting developers
May 06 07:53:58 Finished developers                                               4s 177MB
May 06 07:53:58 Starting developers/bin
May 06 07:54:30 Finished developers/bin                                          31s   1GB
May 06 07:54:30 Starting semantics/ffi
May 06 07:54:41 Finished semantics/ffi                                           10s 202MB
May 06 07:54:41 Starting semantics
May 06 07:56:39 Finished semantics                                             1m57s   1GB
May 06 07:56:39 Starting semantics/proofs
May 06 08:00:44 Finished semantics/proofs                                      4m05s   3GB
May 06 08:00:44 Starting semantics/alt_semantics
May 06 08:01:08 Finished semantics/alt_semantics                                 23s 506MB
May 06 08:01:08 Starting semantics/alt_semantics/proofs
May 06 08:04:06 Finished semantics/alt_semantics/proofs                        2m57s   1GB
May 06 08:04:06 Starting basis/pure
May 06 08:05:11 Finished basis/pure                                            1m05s   1GB
May 06 08:05:11 Starting translator
May 06 08:08:12 Finished translator                                            3m00s   1GB
May 06 08:08:12 Starting compiler/parsing
May 06 08:09:29 Finished compiler/parsing                                      1m16s   3GB
May 06 08:09:30 Starting characteristic
May 06 08:15:55 Finished characteristic                                        6m24s   2GB
May 06 08:15:55 Starting translator/monadic
May 06 08:17:55 Finished translator/monadic                                    2m00s   1GB
May 06 08:17:55 Starting basis
May 06 09:04:39 Finished basis                                                46m41s  16GB
May 06 09:04:39 Starting compiler/inference
May 06 09:06:01 Finished compiler/inference                                    1m21s   1GB
May 06 09:06:01 Starting compiler/backend/reg_alloc
May 06 09:07:44 Finished compiler/backend/reg_alloc                            1m43s   1GB
May 06 09:07:44 Starting compiler/backend/gc
May 06 09:12:01 Finished compiler/backend/gc                                   4m17s   2GB
May 06 09:12:01 Starting compiler/backend
May 06 09:17:39 Finished compiler/backend                                      5m37s   3GB
May 06 09:17:39 Starting compiler/encoders/asm
May 06 09:18:09 Finished compiler/encoders/asm                                   30s   1GB
May 06 09:18:09 Starting compiler/encoders/x64
May 06 09:18:39 Finished compiler/encoders/x64                                   29s   1GB
May 06 09:18:39 Starting compiler/encoders/arm7
May 06 09:19:37 Finished compiler/encoders/arm7                                  57s 842MB
May 06 09:19:37 Starting compiler/encoders/arm8
May 06 09:19:55 Finished compiler/encoders/arm8                                  17s 916MB
May 06 09:19:55 Starting compiler/encoders/arm8_asl
May 06 09:22:27 Finished compiler/encoders/arm8_asl                            2m32s   1GB
May 06 09:22:27 Starting compiler/encoders/mips
May 06 09:22:49 Finished compiler/encoders/mips                                  21s   1GB
May 06 09:22:49 Starting compiler/encoders/riscv
May 06 09:23:08 Finished compiler/encoders/riscv                                 18s 875MB
May 06 09:23:08 Starting compiler/encoders/ag32
May 06 09:23:29 Finished compiler/encoders/ag32                                  21s 795MB
May 06 09:23:29 Starting compiler/backend/x64
May 06 09:23:52 Finished compiler/backend/x64                                    22s   1GB
May 06 09:23:52 Starting compiler/backend/arm7
May 06 09:24:14 Finished compiler/backend/arm7                                   21s   1GB
May 06 09:24:14 Starting compiler/backend/arm8
May 06 09:24:36 Finished compiler/backend/arm8                                   21s   1GB
May 06 09:24:36 Starting compiler/backend/mips
May 06 09:24:59 Finished compiler/backend/mips                                   22s   1GB
May 06 09:24:59 Starting compiler/backend/riscv
May 06 09:25:21 Finished compiler/backend/riscv                                  22s   1GB
May 06 09:25:21 Starting compiler/backend/ag32
May 06 09:26:49 Finished compiler/backend/ag32                                 1m27s   1GB
May 06 09:26:49 Starting compiler/parsing/proofs
May 06 09:30:28 Finished compiler/parsing/proofs                               3m38s   1GB
May 06 09:30:28 Starting compiler/inference/proofs
May 06 09:33:00 Finished compiler/inference/proofs                             2m32s   1GB
May 06 09:33:01 Starting compiler/backend/semantics
May 06 10:01:02 Finished compiler/backend/semantics                           28m01s   2GB
May 06 10:01:02 Starting compiler/backend/reg_alloc/proofs
May 06 10:04:42 Finished compiler/backend/reg_alloc/proofs                     3m36s 775MB
May 06 10:04:43 Starting compiler/backend/proofs
May 06 10:55:58 Finished compiler/backend/proofs                              51m14s  19GB
May 06 10:55:58 Starting compiler/backend/serialiser
May 06 10:57:36 Finished compiler/backend/serialiser                           1m37s   2GB
May 06 10:57:36 Starting compiler/encoders/x64/proofs
May 06 11:07:15 Finished compiler/encoders/x64/proofs                          9m37s   4GB
May 06 11:07:15 Starting compiler/encoders/arm7/proofs
May 06 11:20:22 Finished compiler/encoders/arm7/proofs                        13m06s   3GB
May 06 11:20:22 Starting compiler/encoders/arm8/proofs
May 06 11:27:24 Finished compiler/encoders/arm8/proofs                         7m01s   1GB
May 06 11:27:24 Starting compiler/encoders/arm8_asl/proofs
May 06 11:43:00 Finished compiler/encoders/arm8_asl/proofs                    15m35s   1GB
May 06 11:43:00 Starting compiler/encoders/mips/proofs
May 06 11:53:06 Finished compiler/encoders/mips/proofs                        10m05s   1GB
May 06 11:53:06 Starting compiler/encoders/riscv/proofs
May 06 12:01:55 Finished compiler/encoders/riscv/proofs                        8m48s   1GB
May 06 12:01:55 Starting compiler/encoders/ag32/proofs
May 06 12:04:32 Finished compiler/encoders/ag32/proofs                         2m36s 699MB
May 06 12:04:32 Starting compiler/backend/x64/proofs
May 06 12:05:01 Finished compiler/backend/x64/proofs                             28s   1GB
May 06 12:05:01 Starting compiler/backend/arm7/proofs
May 06 12:05:30 Finished compiler/backend/arm7/proofs                            29s   1GB
May 06 12:05:30 Starting compiler/backend/arm8/proofs
May 06 12:05:59 Finished compiler/backend/arm8/proofs                            28s   1GB
May 06 12:05:59 Starting compiler/backend/arm8_asl
May 06 12:06:23 Finished compiler/backend/arm8_asl                               23s   1GB
May 06 12:06:23 Starting compiler/backend/mips/proofs
May 06 12:06:51 Finished compiler/backend/mips/proofs                            27s   1GB
May 06 12:06:51 Starting compiler/backend/riscv/proofs
May 06 12:07:20 Finished compiler/backend/riscv/proofs                           28s   1GB
May 06 12:07:20 Starting compiler/backend/ag32/proofs
May 06 12:20:24 Finished compiler/backend/ag32/proofs                         13m03s   3GB
May 06 12:20:24 Starting compiler/proofs
May 06 12:22:31 Finished compiler/proofs                                       2m06s   3GB
May 06 12:22:31 Starting candle/set-theory
May 06 12:23:06 Finished candle/set-theory                                       35s 920MB
May 06 12:23:06 Starting candle/syntax-lib
May 06 12:23:20 Finished candle/syntax-lib                                       13s 630MB
May 06 12:23:20 Starting candle/standard/syntax
May 06 12:25:23 Finished candle/standard/syntax                                2m02s   1GB
May 06 12:25:23 Starting candle/standard/semantics
May 06 12:27:12 Finished candle/standard/semantics                             1m49s   1GB
May 06 12:27:13 Starting candle/standard/monadic
May 06 12:29:06 Finished candle/standard/monadic                               1m53s   1GB
May 06 12:29:06 Starting candle/standard/ml_kernel
May 06 12:35:18 Finished candle/standard/ml_kernel                             6m12s   3GB
May 06 12:35:19 Starting candle/overloading/syntax
May 06 12:38:30 Finished candle/overloading/syntax                             3m10s   1GB
May 06 12:38:30 Starting candle/overloading/semantics
May 06 12:50:08 Finished candle/overloading/semantics                         11m38s   2GB
May 06 12:50:09 Starting candle/overloading/monadic
May 06 12:52:43 Finished candle/overloading/monadic                            2m34s   1GB
May 06 12:52:43 Starting candle/overloading/ml_kernel
May 06 12:59:36 Finished candle/overloading/ml_kernel                          6m52s   4GB
May 06 12:59:36 Starting candle/overloading/ml_checker
May 06 13:02:02 Finished candle/overloading/ml_checker                         2m26s   3GB
May 06 13:02:02 Starting candle/prover
May 06 13:10:15 Finished candle/prover                                         8m11s   2GB
May 06 13:10:15 Starting pancake
May 06 13:13:56 Finished pancake                                               3m40s   3GB
May 06 13:13:56 Starting pancake/ffi
May 06 13:13:57 Finished pancake/ffi                                              0s  35MB
May 06 13:13:57 Starting pancake/semantics
May 06 13:16:26 Finished pancake/semantics                                     2m29s 967MB
May 06 13:16:26 Starting pancake/proofs
May 06 13:28:28 Finished pancake/proofs                                       12m01s   5GB
May 06 13:28:28 Starting characteristic/examples
May 06 13:29:51 Finished characteristic/examples                               1m23s   3GB
May 06 13:29:51 Starting tutorial/solutions
May 06 13:46:38 Finished tutorial/solutions                                   16m46s   9GB
May 06 13:46:38 Starting translator/monadic/examples
May 06 13:50:29 Finished translator/monadic/examples                           3m50s   2GB
May 06 13:50:29 Starting examples
May 06 13:59:47 Finished examples                                              9m17s   4GB
May 06 13:59:47 Starting examples/compilation/x64
May 06 16:32:15 Finished examples/compilation/x64                           2h32m26s  17GB
May 06 16:32:15 Starting examples/compilation/x64/proofs
May 06 16:34:46 Finished examples/compilation/x64/proofs                       2m30s   3GB
May 06 16:34:46 Starting examples/compilation/ag32
May 06 17:09:54 Finished examples/compilation/ag32                            35m07s   9GB
May 06 17:09:54 Starting examples/compilation/ag32/proofs
May 06 17:11:24 Finished examples/compilation/ag32/proofs                      1m29s   1GB
May 06 17:11:24 Starting examples/cost
May 06 18:07:36 Finished examples/cost                                        56m10s   9GB
May 06 18:07:36 Starting examples/lpr_checker
May 06 18:08:39 Finished examples/lpr_checker                                  1m02s 965MB
May 06 18:08:39 Starting examples/lpr_checker/array
May 06 18:36:32 Finished examples/lpr_checker/array                           27m52s   7GB
May 06 18:36:32 Starting examples/lpr_checker/array/compilation
May 06 20:00:00 Finished examples/lpr_checker/array/compilation             1h23m27s  30GB
May 06 20:00:01 Starting examples/lpr_checker/array/compilation/proofs
May 06 20:01:29 Finished examples/lpr_checker/array/compilation/proofs         1m28s   7GB
May 06 20:01:29 Starting examples/opentheory
May 06 20:11:17 Finished examples/opentheory                                   9m47s   4GB
May 06 20:11:17 Starting examples/opentheory
May 06 20:11:19 Finished examples/opentheory                                      1s 138MB
May 06 20:11:19 Starting examples/opentheory/compilation
May 06 20:51:04 Finished examples/opentheory/compilation                      39m44s  25GB
May 06 20:51:04 Starting examples/opentheory/compilation/proofs
May 06 20:52:13 Finished examples/opentheory/compilation/proofs                1m09s   3GB
May 06 20:52:13 Starting examples/opentheory/compilation/ag32
May 06 21:30:15 Finished examples/opentheory/compilation/ag32                 38m01s  28GB
May 06 21:30:16 Starting examples/opentheory/compilation/ag32/proofs
May 06 21:32:02 Finished examples/opentheory/compilation/ag32/proofs           1m46s   6GB
May 06 21:32:02 Starting examples/sat_encodings
May 06 21:34:04 Finished examples/sat_encodings                                2m01s 886MB
May 06 21:34:04 Starting examples/sat_encodings/case_studies
May 06 21:35:46 Finished examples/sat_encodings/case_studies                   1m41s 747MB
May 06 21:35:46 Starting examples/sat_encodings/translation
May 06 21:41:32 Finished examples/sat_encodings/translation                    5m46s   3GB
May 06 21:41:32 Starting examples/sat_encodings/translation/compilation
May 06 22:30:17 Finished examples/sat_encodings/translation/compilation       48m43s  21GB
May 06 22:30:17 Starting translator/okasaki-examples
May 06 22:35:04 Finished translator/okasaki-examples                           4m47s   1GB
May 06 22:35:04 Starting translator/other-examples
May 06 22:35:53 Finished translator/other-examples                               48s   1GB
May 06 22:35:53 Starting compiler/parsing/tests
May 06 22:36:23 Finished compiler/parsing/tests                                  29s 606MB
May 06 22:36:23 Starting compiler/inference/tests
May 06 22:44:55 Finished compiler/inference/tests                              8m31s   5GB
May 06 22:44:55 Starting compiler/printing/test
May 06 22:48:45 Finished compiler/printing/test                                3m49s   3GB
May 06 22:48:45 Starting compiler/repl
May 06 23:01:48 Finished compiler/repl                                        13m02s   7GB
May 06 23:01:48 Starting compiler/bootstrap/translation
May 07 02:59:26 Finished compiler/bootstrap/translation                     3h57m36s  52GB
May 07 02:59:26 Starting unverified/sexpr-bootstrap/x64/64
May 07 03:11:07 Finished unverified/sexpr-bootstrap/x64/64                    11m41s  11GB
May 07 03:11:07 Starting unverified/sexpr-bootstrap/x64/32
May 07 03:20:48 Finished unverified/sexpr-bootstrap/x64/32                     9m41s  12GB
May 07 03:20:48 Starting compiler/benchmarks
May 07 03:21:44 Finished compiler/benchmarks                                     55s 674MB
May 07 03:21:44 Starting compiler/bootstrap/compilation/x64/64
May 07 22:13:16 Finished compiler/bootstrap/compilation/x64/64             18h51m29s  64GB
May 07 22:13:16 Starting compiler/bootstrap/compilation/x64/64/proofs
May 07 22:32:07 Finished compiler/bootstrap/compilation/x64/64/proofs         18m51s  45GB
May 07 22:32:07 Starting compiler/bootstrap/compilation/x64/32
May 08 12:17:36 Finished compiler/bootstrap/compilation/x64/32             13h45m25s  64GB
May 08 12:17:36 Starting compiler/bootstrap/compilation/x64/32/proofs
May 08 12:22:14 Finished compiler/bootstrap/compilation/x64/32/proofs          4m37s  15GB
May 08 12:22:14 Starting compiler/bootstrap/compilation/ag32/32
May 09 01:16:24 Finished compiler/bootstrap/compilation/ag32/32            12h54m08s  64GB
May 09 01:16:24 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 09 01:41:06 Finished compiler/bootstrap/compilation/ag32/32/proofs        24m41s  28GB
May 09 01:41:06 SUCCESS