Job 2125

CakeML:4029ad0a1fd71834ff75765e3cf501db8ce9a3f9
  pancake: pan_to_target semantics correctness proof [May 13 10:31:30]
#951 (pan_compose)
Merging into:90e158ecb61cc3974c249811f350943545a8b2c1
  Merge pull request #950 from CakeML/rev_list [May 13 10:18:57]
HOL:63a4c9c66796e8d93b355a237575ca63c550a059
  Replace sprintf with snprintf to quiet some deprecation warnings [May 11 01:37:07]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

May 15 13:50:36 Claimed job
May 15 13:50:39 Building HOL
May 15 14:02:55 Starting developers
May 15 14:03:00 Finished developers                                               5s 176MB
May 15 14:03:00 Starting developers/bin
May 15 14:03:06 Finished developers/bin                                           6s   1GB
May 15 14:03:06 Starting compiler/proofs
May 15 15:55:55 Finished compiler/proofs                                    1h52m46s  22GB
May 15 15:55:55 Starting compiler/bootstrap/translation
May 15 23:56:30 Finished compiler/bootstrap/translation                     8h00m33s  42GB
May 15 23:56:30 Starting semantics/ffi
May 15 23:56:35 Finished semantics/ffi                                            4s 426MB
May 15 23:56:35 Starting semantics
May 15 23:56:36 Finished semantics                                                1s  17MB
May 15 23:56:37 Starting semantics/proofs
May 15 23:57:08 Finished semantics/proofs                                        31s 739MB
May 15 23:57:08 Starting semantics/alt_semantics
May 15 23:57:39 Finished semantics/alt_semantics                                 30s 876MB
May 15 23:57:39 Starting semantics/alt_semantics/proofs
May 16 00:09:26 Finished semantics/alt_semantics/proofs                       11m47s   1GB
May 16 00:09:27 Starting basis/pure
May 16 00:09:28 Finished basis/pure                                               1s  19MB
May 16 00:09:28 Starting translator
May 16 00:11:18 Finished translator                                            1m49s   1GB
May 16 00:11:18 Starting compiler/parsing
May 16 00:11:20 Finished compiler/parsing                                         1s  19MB
May 16 00:11:20 Starting characteristic
May 16 00:11:22 Finished characteristic                                           1s  22MB
May 16 00:11:22 Starting translator/monadic
May 16 00:11:24 Finished translator/monadic                                       1s  28MB
May 16 00:11:24 Starting basis
May 16 00:15:22 Finished basis                                                 3m58s   3GB
May 16 00:15:23 Starting compiler/inference
May 16 00:15:24 Finished compiler/inference                                       1s  18MB
May 16 00:15:24 Starting compiler/backend/reg_alloc
May 16 00:15:26 Finished compiler/backend/reg_alloc                               1s  18MB
May 16 00:15:26 Starting compiler/backend/gc
May 16 00:15:29 Finished compiler/backend/gc                                      2s  25MB
May 16 00:15:29 Starting compiler/backend
May 16 00:15:41 Finished compiler/backend                                        12s 844MB
May 16 00:15:41 Starting compiler/encoders/asm
May 16 00:15:43 Finished compiler/encoders/asm                                    1s  24MB
May 16 00:15:43 Starting compiler/encoders/x64
May 16 00:15:45 Finished compiler/encoders/x64                                    1s  23MB
May 16 00:15:45 Starting compiler/encoders/arm7
May 16 00:15:47 Finished compiler/encoders/arm7                                   1s  24MB
May 16 00:15:47 Starting compiler/encoders/arm8
May 16 00:15:49 Finished compiler/encoders/arm8                                   1s  27MB
May 16 00:15:49 Starting compiler/encoders/arm8_asl
May 16 02:40:57 Finished compiler/encoders/arm8_asl                         2h25m07s  46GB
May 16 02:40:57 Starting compiler/encoders/mips
May 16 02:40:59 Finished compiler/encoders/mips                                   1s  24MB
May 16 02:40:59 Starting compiler/encoders/riscv
May 16 02:41:01 Finished compiler/encoders/riscv                                  1s  27MB
May 16 02:41:01 Starting compiler/encoders/ag32
May 16 02:41:03 Finished compiler/encoders/ag32                                   1s  20MB
May 16 02:41:03 Starting compiler/backend/x64
May 16 02:41:05 Finished compiler/backend/x64                                     2s  25MB
May 16 02:41:05 Starting compiler/backend/arm7
May 16 02:41:08 Finished compiler/backend/arm7                                    2s  24MB
May 16 02:41:08 Starting compiler/backend/arm8
May 16 02:41:10 Finished compiler/backend/arm8                                    2s  23MB
May 16 02:41:10 Starting compiler/backend/mips
May 16 02:41:12 Finished compiler/backend/mips                                    2s  22MB
May 16 02:41:12 Starting compiler/backend/riscv
May 16 02:41:15 Finished compiler/backend/riscv                                   2s  28MB
May 16 02:41:15 Starting compiler/backend/ag32
May 16 02:42:43 Finished compiler/backend/ag32                                 1m28s   1GB
May 16 02:42:43 Starting compiler/parsing/proofs
May 16 02:42:45 Finished compiler/parsing/proofs                                  1s  24MB
May 16 02:42:45 Starting compiler/inference/proofs
May 16 02:42:47 Finished compiler/inference/proofs                                1s  20MB
May 16 02:42:47 Starting compiler/backend/semantics
May 16 02:43:59 Finished compiler/backend/semantics                            1m12s   1GB
May 16 02:43:59 Starting compiler/backend/reg_alloc/proofs
May 16 02:44:01 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
May 16 02:44:02 Starting compiler/backend/proofs
May 16 02:45:01 Finished compiler/backend/proofs                                 58s   3GB
May 16 02:45:01 Starting compiler/backend/serialiser
May 16 02:45:04 Finished compiler/backend/serialiser                              2s  39MB
May 16 02:45:04 Starting compiler/encoders/x64/proofs
May 16 02:54:54 Finished compiler/encoders/x64/proofs                          9m50s   7GB
May 16 02:54:54 Starting compiler/encoders/arm7/proofs
May 16 03:08:44 Finished compiler/encoders/arm7/proofs                        13m49s   3GB
May 16 03:08:44 Starting compiler/encoders/arm8/proofs
May 16 03:15:35 Finished compiler/encoders/arm8/proofs                         6m51s   1GB
May 16 03:15:36 Starting compiler/encoders/arm8_asl/proofs
May 16 04:07:50 Finished compiler/encoders/arm8_asl/proofs                    52m12s   5GB
May 16 04:07:52 Starting compiler/encoders/mips/proofs
May 16 04:18:40 Finished compiler/encoders/mips/proofs                        10m47s   2GB
May 16 04:18:40 Starting compiler/encoders/riscv/proofs
May 16 04:27:44 Finished compiler/encoders/riscv/proofs                        9m03s   1GB
May 16 04:27:44 Starting compiler/encoders/ag32/proofs
May 16 04:30:19 Finished compiler/encoders/ag32/proofs                         2m35s   1GB
May 16 04:30:19 Starting compiler/backend/x64/proofs
May 16 04:30:49 Finished compiler/backend/x64/proofs                             30s   2GB
May 16 04:30:50 Starting compiler/backend/arm7/proofs
May 16 04:31:23 Finished compiler/backend/arm7/proofs                            33s   1GB
May 16 04:31:23 Starting compiler/backend/arm8/proofs
May 16 04:31:54 Finished compiler/backend/arm8/proofs                            30s   1GB
May 16 04:31:54 Starting compiler/backend/arm8_asl
May 16 04:32:16 Finished compiler/backend/arm8_asl                               22s   1GB
May 16 04:32:16 Starting compiler/backend/mips/proofs
May 16 04:32:48 Finished compiler/backend/mips/proofs                            31s   2GB
May 16 04:32:48 Starting compiler/backend/riscv/proofs
May 16 04:33:23 Finished compiler/backend/riscv/proofs                           34s   2GB
May 16 04:33:23 Starting compiler/backend/ag32/proofs
May 16 04:47:01 Finished compiler/backend/ag32/proofs                         13m38s   2GB
May 16 04:47:01 Starting candle/set-theory
May 16 04:47:41 Finished candle/set-theory                                       39s   1GB
May 16 04:47:41 Starting candle/syntax-lib
May 16 04:47:42 Finished candle/syntax-lib                                        1s  18MB
May 16 04:47:42 Starting candle/standard/syntax
May 16 04:47:53 Finished candle/standard/syntax                                  10s 823MB
May 16 04:47:53 Starting candle/standard/semantics
May 16 04:49:49 Finished candle/standard/semantics                             1m55s   1GB
May 16 04:49:50 Starting candle/standard/monadic
May 16 04:49:51 Finished candle/standard/monadic                                  1s  30MB
May 16 04:49:52 Starting candle/standard/ml_kernel
May 16 04:51:29 Finished candle/standard/ml_kernel                             1m37s   3GB
May 16 04:51:30 Starting candle/overloading/syntax
May 16 04:54:50 Finished candle/overloading/syntax                             3m20s   1GB
May 16 04:54:50 Starting candle/overloading/semantics
May 16 05:06:58 Finished candle/overloading/semantics                         12m07s   2GB
May 16 05:06:58 Starting candle/overloading/monadic
May 16 05:09:38 Finished candle/overloading/monadic                            2m38s   1GB
May 16 05:09:41 Starting candle/overloading/ml_kernel
May 16 05:17:42 Finished candle/overloading/ml_kernel                          8m01s   4GB
May 16 05:17:42 Starting candle/overloading/ml_checker
May 16 05:20:21 Finished candle/overloading/ml_checker                         2m39s   2GB
May 16 05:20:21 Starting candle/prover
May 16 05:30:17 Finished candle/prover                                         9m55s   3GB
May 16 05:30:17 Starting pancake
May 16 05:31:01 Finished pancake                                                 43s   1GB
May 16 05:31:01 Starting pancake/ffi
May 16 05:31:02 Finished pancake/ffi                                              0s  13MB
May 16 05:31:02 Starting pancake/semantics
May 16 05:33:27 Finished pancake/semantics                                     2m25s   1GB
May 16 05:33:27 Starting pancake/proofs
May 16 05:48:43 Finished pancake/proofs                                       15m15s   3GB
May 16 05:48:43 Starting characteristic/examples
May 16 05:50:16 Finished characteristic/examples                               1m32s   2GB
May 16 05:50:16 Starting tutorial/solutions
May 16 06:05:23 Finished tutorial/solutions                                   15m07s   8GB
May 16 06:05:23 Starting translator/monadic/examples
May 16 06:09:25 Finished translator/monadic/examples                           4m01s   3GB
May 16 06:09:25 Starting examples
May 16 06:25:32 Finished examples                                             16m06s   4GB
May 16 06:25:32 Starting examples/compilation/x64
May 16 08:25:24 Finished examples/compilation/x64                           1h59m50s  14GB
May 16 08:25:24 Starting examples/compilation/x64/proofs
May 16 08:27:55 Finished examples/compilation/x64/proofs                       2m31s   4GB
May 16 08:27:55 Starting examples/compilation/ag32
May 16 08:58:30 Finished examples/compilation/ag32                            30m34s   6GB
May 16 08:58:30 Starting examples/compilation/ag32/proofs
May 16 08:59:31 Finished examples/compilation/ag32/proofs                      1m01s   3GB
May 16 08:59:31 Starting examples/compilation/to_word
May 16 09:02:54 Finished examples/compilation/to_word                          3m22s   6GB
May 16 09:02:54 Starting examples/lpr_checker
May 16 09:03:59 Finished examples/lpr_checker                                  1m05s   1GB
May 16 09:04:00 Starting examples/lpr_checker/array
May 16 09:40:35 Finished examples/lpr_checker/array                           36m33s   6GB
May 16 09:40:35 Starting examples/lpr_checker/array/compilation
May 16 10:21:22 Finished examples/lpr_checker/array/compilation               40m46s  23GB
May 16 10:21:22 Starting examples/lpr_checker/array/compilation/proofs
May 16 10:22:56 Finished examples/lpr_checker/array/compilation/proofs         1m33s   7GB
May 16 10:22:56 Starting examples/opentheory
May 16 10:33:50 Finished examples/opentheory                                  10m53s   4GB
May 16 10:33:50 Starting examples/opentheory
May 16 10:33:52 Finished examples/opentheory                                      1s  26MB
May 16 10:33:52 Starting examples/opentheory/compilation
May 16 11:10:16 Finished examples/opentheory/compilation                      36m22s  29GB
May 16 11:10:16 Starting examples/opentheory/compilation/proofs
May 16 11:11:19 Finished examples/opentheory/compilation/proofs                1m02s   4GB
May 16 11:11:19 Starting examples/opentheory/compilation/ag32
May 16 11:44:15 Finished examples/opentheory/compilation/ag32                 32m55s  28GB
May 16 11:44:15 Starting examples/opentheory/compilation/ag32/proofs
May 16 11:46:09 Finished examples/opentheory/compilation/ag32/proofs           1m53s   8GB
May 16 11:46:09 Starting examples/sat_encodings
May 16 11:48:13 Finished examples/sat_encodings                                2m03s 858MB
May 16 11:48:13 Starting examples/sat_encodings/case_studies
May 16 11:50:01 Finished examples/sat_encodings/case_studies                   1m47s   1GB
May 16 11:50:01 Starting examples/sat_encodings/translation
May 16 11:56:15 Finished examples/sat_encodings/translation                    6m14s   6GB
May 16 11:56:15 Starting examples/sat_encodings/translation/compilation
May 16 12:40:24 Finished examples/sat_encodings/translation/compilation       44m05s  19GB
May 16 12:40:25 Starting examples/deflate
May 16 12:41:24 Finished examples/deflate                                        59s 879MB
May 16 12:41:24 Starting examples/deflate/translation
May 16 12:43:05 Finished examples/deflate/translation                          1m41s   3GB
May 16 12:43:06 Starting examples/deflate/translation/compilation
May 16 13:03:08 Finished examples/deflate/translation/compilation             20m02s  10GB
May 16 13:03:08 Starting translator/okasaki-examples
May 16 13:08:13 Finished translator/okasaki-examples                           5m04s   2GB
May 16 13:08:13 Starting translator/other-examples
May 16 13:10:56 Finished translator/other-examples                             2m42s   1GB
May 16 13:10:56 Starting compiler/parsing/tests
May 16 13:11:32 Finished compiler/parsing/tests                                  36s 320MB
May 16 13:11:32 Starting compiler/inference/tests
May 16 13:20:01 Finished compiler/inference/tests                              8m28s   3GB
May 16 13:20:01 Starting compiler/printing/test
May 16 13:23:52 Finished compiler/printing/test                                3m50s   3GB
May 16 13:23:52 Starting icing/flover
May 16 14:07:47 Finished icing/flover                                         43m49s   2GB
May 16 14:07:47 Starting icing/
May 16 15:04:06 Finished icing/                                               56m18s   7GB
May 16 15:04:06 Starting icing/examples
May 16 15:05:38 Finished icing/examples                                        1m31s   3GB
May 16 15:05:38 Starting compiler/repl
May 16 15:14:17 Finished compiler/repl                                         8m38s   4GB
May 16 15:14:18 Starting unverified/sexpr-bootstrap/x64/64
May 16 15:27:29 Finished unverified/sexpr-bootstrap/x64/64                    13m10s  16GB
May 16 15:27:29 Starting unverified/sexpr-bootstrap/x64/32
May 16 15:38:10 Finished unverified/sexpr-bootstrap/x64/32                    10m41s  13GB
May 16 15:38:10 Starting compiler/benchmarks
May 16 15:53:35 Finished compiler/benchmarks                                  15m25s   2GB
May 16 15:53:35 Starting compiler/bootstrap/compilation/x64/64
May 17 03:45:25 Finished compiler/bootstrap/compilation/x64/64             11h51m47s  64GB
May 17 03:45:25 Starting compiler/bootstrap/compilation/x64/64/proofs
May 17 04:06:05 Finished compiler/bootstrap/compilation/x64/64/proofs         20m40s  44GB
May 17 04:06:06 Starting compiler/bootstrap/compilation/x64/32
May 17 11:01:40 Finished compiler/bootstrap/compilation/x64/32              6h55m32s  64GB
May 17 11:01:40 Starting compiler/bootstrap/compilation/x64/32/proofs
May 17 11:04:36 Finished compiler/bootstrap/compilation/x64/32/proofs          2m55s  15GB
May 17 11:04:36 Starting compiler/bootstrap/compilation/ag32/32
May 17 18:06:38 Finished compiler/bootstrap/compilation/ag32/32             7h02m00s  64GB
May 17 18:06:38 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 17 18:20:17 Finished compiler/bootstrap/compilation/ag32/32/proofs        13m38s  21GB
May 17 18:20:17 SUCCESS