Job 2112

CakeML:ffffabde9be27eb1a7c05b72b15d4d3c99db7180
  Fix baby/bathwater ratio in grammar ancestry "cleanup" [Mar 14 07:56:36]
#934 (good_dimindex)
Merging into:c9a39b5fce675a57155fe86f1de7362fc51172a3
  Merge pull request #933 from hrutvik/pure-end-to-end [Mar 13 21:47:27]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Mar 20 11:28:32 Claimed job
Mar 20 11:28:34 Reusing HOL
Mar 20 11:29:14 Starting developers
Mar 20 11:29:19 Finished developers                                               5s 134MB
Mar 20 11:29:19 Starting developers/bin
Mar 20 11:29:25 Finished developers/bin                                           6s   1GB
Mar 20 11:29:25 Starting compiler/proofs
Mar 21 00:27:01 Resuming compiler/proofs
Mar 21 02:32:53 Finished compiler/proofs                                    2h05m49s  17GB
Mar 21 02:32:53 Starting compiler/bootstrap/translation
Mar 21 11:17:06 Finished compiler/bootstrap/translation                     8h44m12s  32GB
Mar 21 11:17:06 Starting semantics/ffi
Mar 21 11:17:12 Finished semantics/ffi                                            6s 213MB
Mar 21 11:17:13 Starting semantics
Mar 21 11:17:14 Finished semantics                                                1s  18MB
Mar 21 11:17:14 Starting semantics/proofs
Mar 21 11:17:49 Finished semantics/proofs                                        34s 722MB
Mar 21 11:17:49 Starting semantics/alt_semantics
Mar 21 11:18:22 Finished semantics/alt_semantics                                 33s 858MB
Mar 21 11:18:22 Starting semantics/alt_semantics/proofs
Mar 21 11:30:24 Finished semantics/alt_semantics/proofs                       12m01s   1GB
Mar 21 11:30:24 Starting basis/pure
Mar 21 11:30:25 Finished basis/pure                                               1s  20MB
Mar 21 11:30:25 Starting translator
Mar 21 11:32:19 Finished translator                                            1m53s   1GB
Mar 21 11:32:19 Starting compiler/parsing
Mar 21 11:32:20 Finished compiler/parsing                                         1s  21MB
Mar 21 11:32:20 Starting characteristic
Mar 21 11:32:22 Finished characteristic                                           1s  23MB
Mar 21 11:32:23 Starting translator/monadic
Mar 21 11:32:24 Finished translator/monadic                                       1s  26MB
Mar 21 11:32:25 Starting basis
Mar 21 11:36:37 Finished basis                                                 4m12s   2GB
Mar 21 11:36:37 Starting compiler/inference
Mar 21 11:36:39 Finished compiler/inference                                       1s  21MB
Mar 21 11:36:39 Starting compiler/backend/reg_alloc
Mar 21 11:36:41 Finished compiler/backend/reg_alloc                               1s  21MB
Mar 21 11:36:41 Starting compiler/backend/gc
Mar 21 11:36:43 Finished compiler/backend/gc                                      2s  21MB
Mar 21 11:36:43 Starting compiler/backend
Mar 21 11:36:56 Finished compiler/backend                                        12s 556MB
Mar 21 11:36:56 Starting compiler/encoders/asm
Mar 21 11:36:58 Finished compiler/encoders/asm                                    1s  23MB
Mar 21 11:36:58 Starting compiler/encoders/x64
Mar 21 11:37:00 Finished compiler/encoders/x64                                    1s  22MB
Mar 21 11:37:00 Starting compiler/encoders/arm7
Mar 21 11:37:02 Finished compiler/encoders/arm7                                   1s  20MB
Mar 21 11:37:02 Starting compiler/encoders/arm8
Mar 21 11:37:04 Finished compiler/encoders/arm8                                   1s  19MB
Mar 21 11:37:04 Starting compiler/encoders/arm8_asl
Mar 21 11:40:22 Finished compiler/encoders/arm8_asl                            3m17s   1GB
Mar 21 11:40:22 Starting compiler/encoders/mips
Mar 21 11:40:24 Finished compiler/encoders/mips                                   1s  20MB
Mar 21 11:40:24 Starting compiler/encoders/riscv
Mar 21 11:40:26 Finished compiler/encoders/riscv                                  1s  21MB
Mar 21 11:40:26 Starting compiler/encoders/ag32
Mar 21 11:40:27 Finished compiler/encoders/ag32                                   1s  20MB
Mar 21 11:40:28 Starting compiler/backend/x64
Mar 21 11:40:30 Finished compiler/backend/x64                                     2s  21MB
Mar 21 11:40:30 Starting compiler/backend/arm7
Mar 21 11:40:32 Finished compiler/backend/arm7                                    2s  22MB
Mar 21 11:40:32 Starting compiler/backend/arm8
Mar 21 11:40:35 Finished compiler/backend/arm8                                    2s  23MB
Mar 21 11:40:35 Starting compiler/backend/mips
Mar 21 11:40:37 Finished compiler/backend/mips                                    2s  27MB
Mar 21 11:40:37 Starting compiler/backend/riscv
Mar 21 11:40:39 Finished compiler/backend/riscv                                   2s  32MB
Mar 21 11:40:39 Starting compiler/backend/ag32
Mar 21 11:42:09 Finished compiler/backend/ag32                                 1m29s   1GB
Mar 21 11:42:09 Starting compiler/parsing/proofs
Mar 21 11:42:11 Finished compiler/parsing/proofs                                  1s  17MB
Mar 21 11:42:11 Starting compiler/inference/proofs
Mar 21 11:42:12 Finished compiler/inference/proofs                                1s  23MB
Mar 21 11:42:13 Starting compiler/backend/semantics
Mar 21 11:43:26 Finished compiler/backend/semantics                            1m13s   1GB
Mar 21 11:43:26 Starting compiler/backend/reg_alloc/proofs
Mar 21 11:43:28 Finished compiler/backend/reg_alloc/proofs                        1s  29MB
Mar 21 11:43:28 Starting compiler/backend/proofs
Mar 21 11:44:28 Finished compiler/backend/proofs                                 59s   2GB
Mar 21 11:44:28 Starting compiler/backend/serialiser
Mar 21 11:44:31 Finished compiler/backend/serialiser                              2s  35MB
Mar 21 11:44:31 Starting compiler/encoders/x64/proofs
Mar 21 11:54:28 Finished compiler/encoders/x64/proofs                          9m57s   6GB
Mar 21 11:54:29 Starting compiler/encoders/arm7/proofs
Mar 21 12:08:42 Finished compiler/encoders/arm7/proofs                        14m13s   3GB
Mar 21 12:08:42 Starting compiler/encoders/arm8/proofs
Mar 21 12:15:49 Finished compiler/encoders/arm8/proofs                         7m06s   1GB
Mar 21 12:15:49 Starting compiler/encoders/arm8_asl/proofs
Mar 21 12:32:05 Finished compiler/encoders/arm8_asl/proofs                    16m14s   2GB
Mar 21 12:32:05 Starting compiler/encoders/mips/proofs
Mar 21 12:42:58 Finished compiler/encoders/mips/proofs                        10m52s   2GB
Mar 21 12:42:58 Starting compiler/encoders/riscv/proofs
Mar 21 12:55:34 Finished compiler/encoders/riscv/proofs                       12m36s   1GB
Mar 21 12:55:34 Starting compiler/encoders/ag32/proofs
Mar 21 12:59:19 Finished compiler/encoders/ag32/proofs                         3m44s   1GB
Mar 21 12:59:20 Starting compiler/backend/x64/proofs
Mar 21 12:59:59 Finished compiler/backend/x64/proofs                             39s   1GB
Mar 21 12:59:59 Starting compiler/backend/arm7/proofs
Mar 21 13:00:43 Finished compiler/backend/arm7/proofs                            43s   1GB
Mar 21 13:00:43 Starting compiler/backend/arm8/proofs
Mar 21 13:01:18 Finished compiler/backend/arm8/proofs                            35s   1GB
Mar 21 13:01:19 Starting compiler/backend/arm8_asl
Mar 21 13:01:56 Finished compiler/backend/arm8_asl                               37s   1GB
Mar 21 13:01:56 Starting compiler/backend/mips/proofs
Mar 21 13:02:38 Finished compiler/backend/mips/proofs                            42s   2GB
Mar 21 13:02:39 Starting compiler/backend/riscv/proofs
Mar 21 13:03:29 Finished compiler/backend/riscv/proofs                           50s   2GB
Mar 21 13:03:29 Starting compiler/backend/ag32/proofs
Mar 21 13:22:36 Finished compiler/backend/ag32/proofs                         19m06s   2GB
Mar 21 13:22:36 Starting candle/set-theory
Mar 21 13:23:16 Finished candle/set-theory                                       39s   1GB
Mar 21 13:23:16 Starting candle/syntax-lib
Mar 21 13:23:17 Finished candle/syntax-lib                                        1s  24MB
Mar 21 13:23:17 Starting candle/standard/syntax
Mar 21 13:23:29 Finished candle/standard/syntax                                  11s 691MB
Mar 21 13:23:29 Starting candle/standard/semantics
Mar 21 13:26:41 Finished candle/standard/semantics                             3m12s   1GB
Mar 21 13:26:41 Starting candle/standard/monadic
Mar 21 13:26:43 Finished candle/standard/monadic                                  1s  27MB
Mar 21 13:26:43 Starting candle/standard/ml_kernel
Mar 21 13:28:27 Finished candle/standard/ml_kernel                             1m44s   2GB
Mar 21 13:28:28 Starting candle/overloading/syntax
Mar 21 13:31:58 Finished candle/overloading/syntax                             3m29s   1GB
Mar 21 13:31:58 Starting candle/overloading/semantics
Mar 21 13:45:47 Finished candle/overloading/semantics                         13m48s   3GB
Mar 21 13:45:47 Starting candle/overloading/monadic
Mar 21 13:48:36 Finished candle/overloading/monadic                            2m48s   1GB
Mar 21 13:48:36 Starting candle/overloading/ml_kernel
Mar 21 13:56:45 Finished candle/overloading/ml_kernel                          8m08s   3GB
Mar 21 13:56:45 Starting candle/overloading/ml_checker
Mar 21 13:59:24 Finished candle/overloading/ml_checker                         2m39s   2GB
Mar 21 13:59:24 Starting candle/prover
Mar 21 14:09:43 Finished candle/prover                                        10m18s   4GB
Mar 21 14:09:43 Starting pancake
Mar 21 14:13:20 Finished pancake                                               3m37s   5GB
Mar 21 14:13:21 Starting pancake/ffi
Mar 21 14:13:21 Finished pancake/ffi                                              0s  13MB
Mar 21 14:13:21 Starting pancake/semantics
Mar 21 14:16:04 Finished pancake/semantics                                     2m42s   1GB
Mar 21 14:16:04 Starting pancake/proofs
Mar 21 14:20:15 Finished pancake/proofs                                        4m11s   3GB
Mar 21 14:20:16 Starting characteristic/examples
Mar 21 14:22:02 Finished characteristic/examples                               1m45s   3GB
Mar 21 14:22:02 Starting tutorial/solutions
Mar 21 14:37:19 Finished tutorial/solutions                                   15m17s   8GB
Mar 21 14:37:19 Starting translator/monadic/examples
Mar 21 14:41:22 Finished translator/monadic/examples                           4m02s   2GB
Mar 21 14:41:22 Starting examples
Mar 21 14:58:23 Finished examples                                             17m00s   4GB
Mar 21 14:58:23 Starting examples/compilation/x64
Mar 21 17:12:24 Finished examples/compilation/x64                           2h13m59s  12GB
Mar 21 17:12:24 Starting examples/compilation/x64/proofs
Mar 21 17:15:49 Finished examples/compilation/x64/proofs                       3m24s   4GB
Mar 21 17:15:49 Starting examples/compilation/ag32
Mar 21 17:48:29 Finished examples/compilation/ag32                            32m40s   6GB
Mar 21 17:48:30 Starting examples/compilation/ag32/proofs
Mar 21 17:49:35 Finished examples/compilation/ag32/proofs                      1m04s   5GB
Mar 21 17:49:35 Starting examples/compilation/to_word
Mar 21 17:53:02 Finished examples/compilation/to_word                          3m27s   6GB
Mar 21 17:53:02 Starting examples/lpr_checker
Mar 21 17:54:08 Finished examples/lpr_checker                                  1m05s 867MB
Mar 21 17:54:08 Starting examples/lpr_checker/array
Mar 21 18:33:31 Finished examples/lpr_checker/array                           39m22s   5GB
Mar 21 18:33:32 Starting examples/lpr_checker/array/compilation
Mar 21 19:16:17 Finished examples/lpr_checker/array/compilation               42m45s  25GB
Mar 21 19:16:17 Starting examples/lpr_checker/array/compilation/proofs
Mar 21 19:18:20 Finished examples/lpr_checker/array/compilation/proofs         2m03s   3GB
Mar 21 19:18:20 Starting examples/opentheory
Mar 21 19:29:41 Finished examples/opentheory                                  11m20s   3GB
Mar 21 19:29:41 Starting examples/opentheory
Mar 21 19:29:43 Finished examples/opentheory                                      1s  31MB
Mar 21 19:29:43 Starting examples/opentheory/compilation
Mar 21 20:10:45 Finished examples/opentheory/compilation                      41m00s  29GB
Mar 21 20:10:45 Starting examples/opentheory/compilation/proofs
Mar 21 20:12:33 Finished examples/opentheory/compilation/proofs                1m47s   3GB
Mar 21 20:12:33 Starting examples/opentheory/compilation/ag32
Mar 21 21:02:39 Finished examples/opentheory/compilation/ag32                 50m05s  12GB
Mar 21 21:02:39 Starting examples/opentheory/compilation/ag32/proofs
Mar 21 21:05:29 Finished examples/opentheory/compilation/ag32/proofs           2m50s   3GB
Mar 21 21:05:29 Starting examples/sat_encodings
Mar 21 21:08:32 Finished examples/sat_encodings                                3m01s 917MB
Mar 21 21:08:32 Starting examples/sat_encodings/case_studies
Mar 21 21:10:34 Finished examples/sat_encodings/case_studies                   2m02s   1GB
Mar 21 21:10:34 Starting examples/sat_encodings/translation
Mar 21 21:16:56 Finished examples/sat_encodings/translation                    6m19s   5GB
Mar 21 21:16:56 Starting examples/sat_encodings/translation/compilation
Mar 21 22:06:55 Finished examples/sat_encodings/translation/compilation       49m58s  13GB
Mar 21 22:06:55 Starting examples/deflate
Mar 21 22:08:09 Finished examples/deflate                                      1m14s 966MB
Mar 21 22:08:09 Starting examples/deflate/translation
Mar 21 22:10:42 Finished examples/deflate/translation                          2m32s   3GB
Mar 21 22:10:42 Starting examples/deflate/translation/compilation
Mar 21 22:36:19 Finished examples/deflate/translation/compilation             25m35s  16GB
Mar 21 22:36:19 Starting translator/okasaki-examples
Mar 21 22:42:54 Finished translator/okasaki-examples                           6m34s   2GB
Mar 21 22:42:54 Starting translator/other-examples
Mar 21 22:44:13 Finished translator/other-examples                             1m18s   2GB
Mar 21 22:44:13 Starting compiler/parsing/tests
Mar 21 22:44:57 Finished compiler/parsing/tests                                  43s 331MB
Mar 21 22:44:57 Starting compiler/inference/tests
Mar 21 22:55:43 Finished compiler/inference/tests                             10m46s   5GB
Mar 21 22:55:43 Starting compiler/printing/test
Mar 21 23:00:16 Finished compiler/printing/test                                4m32s   4GB
Mar 21 23:00:16 Starting icing/flover
Mar 21 23:51:46 Finished icing/flover                                         51m28s   2GB
Mar 21 23:51:46 Starting icing/
Mar 22 01:16:55 Finished icing/                                             1h25m05s   8GB
Mar 22 01:16:55 Starting icing/examples
Mar 22 01:18:51 Finished icing/examples                                        1m56s   7GB
Mar 22 01:18:52 Starting compiler/repl
Mar 22 01:30:41 Finished compiler/repl                                        11m48s   6GB
Mar 22 01:30:41 Starting unverified/sexpr-bootstrap/x64/64
Mar 22 01:51:25 Finished unverified/sexpr-bootstrap/x64/64                    20m43s  10GB
Mar 22 01:51:25 Starting unverified/sexpr-bootstrap/x64/32
Mar 22 02:06:30 Finished unverified/sexpr-bootstrap/x64/32                    15m05s   8GB
Mar 22 02:06:30 Starting compiler/benchmarks
Mar 22 02:23:52 Finished compiler/benchmarks                                  17m19s   2GB
Mar 22 02:23:52 Starting compiler/bootstrap/compilation/x64/64
Mar 22 13:30:39 Finished compiler/bootstrap/compilation/x64/64             11h06m45s  64GB
Mar 22 13:30:40 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 22 13:50:40 Finished compiler/bootstrap/compilation/x64/64/proofs         20m00s  41GB
Mar 22 13:50:41 Starting compiler/bootstrap/compilation/x64/32
Mar 22 23:46:55 Resuming compiler/bootstrap/compilation/x64/32
Mar 23 04:51:28 Finished compiler/bootstrap/compilation/x64/32              5h04m32s  64GB
Mar 23 04:51:28 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 23 04:55:23 Finished compiler/bootstrap/compilation/x64/32/proofs          3m54s  12GB
Mar 23 04:55:23 Starting compiler/bootstrap/compilation/ag32/32
Mar 23 11:32:04 Finished compiler/bootstrap/compilation/ag32/32             6h36m38s  63GB
Mar 23 11:32:04 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 23 11:33:53 Resuming compiler/bootstrap/compilation/ag32/32/proofs
Mar 23 11:39:57 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m03s  37GB
Mar 23 11:39:57 SUCCESS