Job 2111

CakeML:0c1fb827a567d2b789948a864bd8085dfdd32c43
  Move some definitions/lemmas [Mar 13 17:37:43]
#933 (pure-end-to-end)
Merging into:a4a3f0b318b9eef32403ec5fbcc2157b8da0f120
  Merge pull request #930 from CakeML/print_app_list [Mar 03 21:23:14]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Mar 13 17:41:18 Claimed job
Mar 13 17:41:23 Reusing HOL
Mar 13 17:42:04 Starting developers
Mar 13 17:42:09 Finished developers                                               5s 136MB
Mar 13 17:42:09 Starting developers/bin
Mar 13 17:42:15 Finished developers/bin                                           6s   1GB
Mar 13 17:42:16 Starting compiler/proofs
Mar 13 19:56:41 Finished compiler/proofs                                    2h14m24s  17GB
Mar 13 19:56:41 Starting compiler/bootstrap/translation
Mar 14 04:01:35 Finished compiler/bootstrap/translation                     8h04m53s  41GB
Mar 14 04:01:35 Starting semantics/ffi
Mar 14 04:01:42 Finished semantics/ffi                                            5s 213MB
Mar 14 04:01:42 Starting semantics
Mar 14 04:01:43 Finished semantics                                                1s  19MB
Mar 14 04:01:43 Starting semantics/proofs
Mar 14 04:02:16 Finished semantics/proofs                                        32s 706MB
Mar 14 04:02:16 Starting semantics/alt_semantics
Mar 14 04:02:49 Finished semantics/alt_semantics                                 32s 665MB
Mar 14 04:02:50 Starting semantics/alt_semantics/proofs
Mar 14 04:14:38 Finished semantics/alt_semantics/proofs                       11m48s   1GB
Mar 14 04:14:38 Starting basis/pure
Mar 14 04:14:40 Finished basis/pure                                               1s  20MB
Mar 14 04:14:40 Starting translator
Mar 14 04:16:29 Finished translator                                            1m49s   1GB
Mar 14 04:16:29 Starting compiler/parsing
Mar 14 04:16:31 Finished compiler/parsing                                         1s  18MB
Mar 14 04:16:31 Starting characteristic
Mar 14 04:16:33 Finished characteristic                                           1s  22MB
Mar 14 04:16:33 Starting translator/monadic
Mar 14 04:16:35 Finished translator/monadic                                       1s  23MB
Mar 14 04:16:35 Starting basis
Mar 14 04:20:35 Finished basis                                                 3m59s   2GB
Mar 14 04:20:35 Starting compiler/inference
Mar 14 04:20:37 Finished compiler/inference                                       1s  23MB
Mar 14 04:20:37 Starting compiler/backend/reg_alloc
Mar 14 04:20:39 Finished compiler/backend/reg_alloc                               1s  21MB
Mar 14 04:20:39 Starting compiler/backend/gc
Mar 14 04:20:41 Finished compiler/backend/gc                                      2s  28MB
Mar 14 04:20:41 Starting compiler/backend
Mar 14 04:20:53 Finished compiler/backend                                        12s 792MB
Mar 14 04:20:54 Starting compiler/encoders/asm
Mar 14 04:20:55 Finished compiler/encoders/asm                                    1s  19MB
Mar 14 04:20:55 Starting compiler/encoders/x64
Mar 14 04:20:57 Finished compiler/encoders/x64                                    1s  22MB
Mar 14 04:20:57 Starting compiler/encoders/arm7
Mar 14 04:20:59 Finished compiler/encoders/arm7                                   1s  22MB
Mar 14 04:20:59 Starting compiler/encoders/arm8
Mar 14 04:21:01 Finished compiler/encoders/arm8                                   1s  21MB
Mar 14 04:21:01 Starting compiler/encoders/arm8_asl
Mar 14 04:24:17 Finished compiler/encoders/arm8_asl                            3m15s   1GB
Mar 14 04:24:17 Starting compiler/encoders/mips
Mar 14 04:24:19 Finished compiler/encoders/mips                                   1s  23MB
Mar 14 04:24:19 Starting compiler/encoders/riscv
Mar 14 04:24:21 Finished compiler/encoders/riscv                                  1s  22MB
Mar 14 04:24:21 Starting compiler/encoders/ag32
Mar 14 04:24:23 Finished compiler/encoders/ag32                                   1s  20MB
Mar 14 04:24:23 Starting compiler/backend/x64
Mar 14 04:24:25 Finished compiler/backend/x64                                     2s  27MB
Mar 14 04:24:25 Starting compiler/backend/arm7
Mar 14 04:24:27 Finished compiler/backend/arm7                                    2s  26MB
Mar 14 04:24:27 Starting compiler/backend/arm8
Mar 14 04:24:30 Finished compiler/backend/arm8                                    2s  34MB
Mar 14 04:24:30 Starting compiler/backend/mips
Mar 14 04:24:32 Finished compiler/backend/mips                                    2s  24MB
Mar 14 04:24:32 Starting compiler/backend/riscv
Mar 14 04:24:34 Finished compiler/backend/riscv                                   2s  28MB
Mar 14 04:24:34 Starting compiler/backend/ag32
Mar 14 04:26:03 Finished compiler/backend/ag32                                 1m28s   1GB
Mar 14 04:26:03 Starting compiler/parsing/proofs
Mar 14 04:26:05 Finished compiler/parsing/proofs                                  1s  19MB
Mar 14 04:26:05 Starting compiler/inference/proofs
Mar 14 04:26:07 Finished compiler/inference/proofs                                1s  20MB
Mar 14 04:26:07 Starting compiler/backend/semantics
Mar 14 04:27:19 Finished compiler/backend/semantics                            1m11s   1GB
Mar 14 04:27:19 Starting compiler/backend/reg_alloc/proofs
Mar 14 04:27:21 Finished compiler/backend/reg_alloc/proofs                        1s  19MB
Mar 14 04:27:21 Starting compiler/backend/proofs
Mar 14 04:28:19 Finished compiler/backend/proofs                                 58s   2GB
Mar 14 04:28:20 Starting compiler/backend/serialiser
Mar 14 04:28:22 Finished compiler/backend/serialiser                              2s  34MB
Mar 14 04:28:23 Starting compiler/encoders/x64/proofs
Mar 14 04:38:14 Finished compiler/encoders/x64/proofs                          9m51s   5GB
Mar 14 04:38:14 Starting compiler/encoders/arm7/proofs
Mar 14 04:52:03 Finished compiler/encoders/arm7/proofs                        13m48s   4GB
Mar 14 04:52:03 Starting compiler/encoders/arm8/proofs
Mar 14 04:59:01 Finished compiler/encoders/arm8/proofs                         6m58s   1GB
Mar 14 04:59:01 Starting compiler/encoders/arm8_asl/proofs
Mar 14 05:15:01 Finished compiler/encoders/arm8_asl/proofs                    15m59s   2GB
Mar 14 05:15:02 Starting compiler/encoders/mips/proofs
Mar 14 05:25:51 Finished compiler/encoders/mips/proofs                        10m49s   2GB
Mar 14 05:25:51 Starting compiler/encoders/riscv/proofs
Mar 14 05:34:53 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Mar 14 05:34:53 Starting compiler/encoders/ag32/proofs
Mar 14 05:37:35 Finished compiler/encoders/ag32/proofs                         2m41s 949MB
Mar 14 05:37:35 Starting compiler/backend/x64/proofs
Mar 14 05:38:04 Finished compiler/backend/x64/proofs                             29s   2GB
Mar 14 05:38:04 Starting compiler/backend/arm7/proofs
Mar 14 05:38:37 Finished compiler/backend/arm7/proofs                            32s   2GB
Mar 14 05:38:37 Starting compiler/backend/arm8/proofs
Mar 14 05:39:07 Finished compiler/backend/arm8/proofs                            30s   1GB
Mar 14 05:39:07 Starting compiler/backend/arm8_asl
Mar 14 05:39:31 Finished compiler/backend/arm8_asl                               23s   1GB
Mar 14 05:39:32 Starting compiler/backend/mips/proofs
Mar 14 05:40:04 Finished compiler/backend/mips/proofs                            32s   1GB
Mar 14 05:40:04 Starting compiler/backend/riscv/proofs
Mar 14 05:40:37 Finished compiler/backend/riscv/proofs                           32s   1GB
Mar 14 05:40:37 Starting compiler/backend/ag32/proofs
Mar 14 05:54:14 Finished compiler/backend/ag32/proofs                         13m37s   3GB
Mar 14 05:54:14 Starting candle/set-theory
Mar 14 05:54:53 Finished candle/set-theory                                       38s   1GB
Mar 14 05:54:53 Starting candle/syntax-lib
Mar 14 05:54:55 Finished candle/syntax-lib                                        1s  20MB
Mar 14 05:54:55 Starting candle/standard/syntax
Mar 14 05:55:05 Finished candle/standard/syntax                                  10s 659MB
Mar 14 05:55:05 Starting candle/standard/semantics
Mar 14 05:57:01 Finished candle/standard/semantics                             1m55s   1GB
Mar 14 05:57:01 Starting candle/standard/monadic
Mar 14 05:57:03 Finished candle/standard/monadic                                  1s  21MB
Mar 14 05:57:03 Starting candle/standard/ml_kernel
Mar 14 05:58:39 Finished candle/standard/ml_kernel                             1m36s   3GB
Mar 14 05:58:39 Starting candle/overloading/syntax
Mar 14 06:01:57 Finished candle/overloading/syntax                             3m18s   1GB
Mar 14 06:01:57 Starting candle/overloading/semantics
Mar 14 06:13:58 Finished candle/overloading/semantics                         12m00s   2GB
Mar 14 06:13:58 Starting candle/overloading/monadic
Mar 14 06:16:41 Finished candle/overloading/monadic                            2m42s   1GB
Mar 14 06:16:41 Starting candle/overloading/ml_kernel
Mar 14 06:24:33 Finished candle/overloading/ml_kernel                          7m51s   4GB
Mar 14 06:24:33 Starting candle/overloading/ml_checker
Mar 14 06:27:05 Finished candle/overloading/ml_checker                         2m31s   3GB
Mar 14 06:27:05 Starting candle/prover
Mar 14 06:36:56 Finished candle/prover                                         9m50s   4GB
Mar 14 06:36:56 Starting pancake
Mar 14 06:40:23 Finished pancake                                               3m27s   4GB
Mar 14 06:40:23 Starting pancake/ffi
Mar 14 06:40:24 Finished pancake/ffi                                              0s  13MB
Mar 14 06:40:24 Starting pancake/semantics
Mar 14 06:42:51 Finished pancake/semantics                                     2m27s   1GB
Mar 14 06:42:51 Starting pancake/proofs
Mar 14 06:47:03 Finished pancake/proofs                                        4m12s   3GB
Mar 14 06:47:04 Starting characteristic/examples
Mar 14 06:48:46 Finished characteristic/examples                               1m42s   3GB
Mar 14 06:48:46 Starting tutorial/solutions
Mar 14 07:04:04 Finished tutorial/solutions                                   15m18s   8GB
Mar 14 07:04:05 Starting translator/monadic/examples
Mar 14 07:08:06 Finished translator/monadic/examples                           4m01s   3GB
Mar 14 07:08:06 Starting examples
Mar 14 07:24:32 Finished examples                                             16m23s   4GB
Mar 14 07:24:32 Starting examples/compilation/x64
Mar 14 09:26:08 Finished examples/compilation/x64                           2h01m34s  13GB
Mar 14 09:26:08 Starting examples/compilation/x64/proofs
Mar 14 09:29:04 Finished examples/compilation/x64/proofs                       2m55s   4GB
Mar 14 09:29:04 Starting examples/compilation/ag32
Mar 14 10:01:14 Finished examples/compilation/ag32                            32m10s   9GB
Mar 14 10:01:14 Starting examples/compilation/ag32/proofs
Mar 14 10:02:19 Finished examples/compilation/ag32/proofs                      1m04s   4GB
Mar 14 10:02:19 Starting examples/compilation/to_word
Mar 14 10:05:45 Finished examples/compilation/to_word                          3m26s   7GB
Mar 14 10:05:45 Starting examples/lpr_checker
Mar 14 10:06:51 Finished examples/lpr_checker                                  1m05s 892MB
Mar 14 10:06:51 Starting examples/lpr_checker/array
Mar 14 10:51:23 Finished examples/lpr_checker/array                           44m31s   6GB
Mar 14 10:51:23 Starting examples/lpr_checker/array/compilation
Mar 14 11:43:41 Finished examples/lpr_checker/array/compilation               52m17s  26GB
Mar 14 11:43:41 Starting examples/lpr_checker/array/compilation/proofs
Mar 14 11:45:44 Finished examples/lpr_checker/array/compilation/proofs         2m03s   3GB
Mar 14 11:45:44 Starting examples/opentheory
Mar 14 11:57:00 Finished examples/opentheory                                  11m13s   4GB
Mar 14 11:57:02 Starting examples/opentheory
Mar 14 11:57:04 Finished examples/opentheory                                      1s  26MB
Mar 14 11:57:04 Starting examples/opentheory/compilation
Mar 14 12:37:17 Finished examples/opentheory/compilation                      40m12s  25GB
Mar 14 12:37:17 Starting examples/opentheory/compilation/proofs
Mar 14 12:38:17 Finished examples/opentheory/compilation/proofs                  59s   5GB
Mar 14 12:38:17 Starting examples/opentheory/compilation/ag32
Mar 14 13:14:09 Finished examples/opentheory/compilation/ag32                 35m50s  23GB
Mar 14 13:14:09 Starting examples/opentheory/compilation/ag32/proofs
Mar 14 13:16:26 Finished examples/opentheory/compilation/ag32/proofs           2m16s   3GB
Mar 14 13:16:26 Starting examples/sat_encodings
Mar 14 13:18:29 Finished examples/sat_encodings                                2m02s 793MB
Mar 14 13:18:29 Starting examples/sat_encodings/case_studies
Mar 14 13:20:22 Finished examples/sat_encodings/case_studies                   1m52s   1GB
Mar 14 13:20:22 Starting examples/sat_encodings/translation
Mar 14 13:26:38 Finished examples/sat_encodings/translation                    6m15s   4GB
Mar 14 13:26:38 Starting examples/sat_encodings/translation/compilation
Mar 14 14:18:25 Finished examples/sat_encodings/translation/compilation       51m46s  19GB
Mar 14 14:18:25 Starting examples/deflate
Mar 14 14:19:49 Finished examples/deflate                                      1m24s 804MB
Mar 14 14:19:49 Starting examples/deflate/translation
Mar 14 14:22:27 Finished examples/deflate/translation                          2m37s   3GB
Mar 14 14:22:27 Starting examples/deflate/translation/compilation
Mar 14 14:51:02 Finished examples/deflate/translation/compilation             28m35s   5GB
Mar 14 14:51:02 Starting translator/okasaki-examples
Mar 14 14:56:18 Finished translator/okasaki-examples                           5m15s   2GB
Mar 14 14:56:18 Starting translator/other-examples
Mar 14 14:57:14 Finished translator/other-examples                               55s   1GB
Mar 14 14:57:14 Starting compiler/parsing/tests
Mar 14 14:57:47 Finished compiler/parsing/tests                                  32s 743MB
Mar 14 14:57:47 Starting compiler/inference/tests
Mar 14 15:06:34 Finished compiler/inference/tests                              8m47s   5GB
Mar 14 15:06:34 Starting compiler/printing/test
Mar 14 15:11:02 Finished compiler/printing/test                                4m26s   3GB
Mar 14 15:11:02 Starting icing/flover
Mar 14 15:55:17 Finished icing/flover                                         44m14s   1GB
Mar 14 15:55:17 Starting icing/
Mar 14 17:12:31 Finished icing/                                             1h17m12s   8GB
Mar 14 17:12:31 Starting icing/examples
Mar 14 17:14:38 Finished icing/examples                                        2m07s   6GB
Mar 14 17:14:39 Starting compiler/repl
Mar 14 17:24:10 Finished compiler/repl                                         9m31s   4GB
Mar 14 17:24:10 Starting unverified/sexpr-bootstrap/x64/64
Mar 14 17:37:42 Finished unverified/sexpr-bootstrap/x64/64                    13m32s  13GB
Mar 14 17:37:43 Starting unverified/sexpr-bootstrap/x64/32
Mar 14 17:48:42 Finished unverified/sexpr-bootstrap/x64/32                    10m59s  11GB
Mar 14 17:48:42 Starting compiler/benchmarks
Mar 14 17:48:47 Finished compiler/benchmarks                                      4s  37MB
Mar 14 17:48:47 Starting compiler/bootstrap/compilation/x64/64
Mar 15 06:26:11 Finished compiler/bootstrap/compilation/x64/64             12h37m23s  42GB
Mar 15 06:26:11 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 15 06:45:51 Finished compiler/bootstrap/compilation/x64/64/proofs         19m39s  31GB
Mar 15 06:45:52 Starting compiler/bootstrap/compilation/x64/32
Mar 15 13:18:46 Finished compiler/bootstrap/compilation/x64/32              6h32m53s  64GB
Mar 15 13:18:46 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 15 13:21:32 Finished compiler/bootstrap/compilation/x64/32/proofs          2m45s  17GB
Mar 15 13:21:32 Starting compiler/bootstrap/compilation/ag32/32
Mar 15 19:59:29 Finished compiler/bootstrap/compilation/ag32/32             6h37m55s  64GB
Mar 15 19:59:29 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 15 20:05:38 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m09s  23GB
Mar 15 20:05:38 SUCCESS