Job 2120

CakeML:e01d7cba0d4231707653d1df65b33061e9c0ddcb
  Make \ddd handling code actually translate [Apr 26 23:40:05]
#948 (lex-decimal-chars)
Merging into:b4b2e5dbd632063b2f838fadc54d14291ec0b530
  Merge pull request #946 from CakeML/count_allocations [Mar 23 09:59:25]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

May 01 10:29:33 Claimed job
May 01 10:29:37 Reusing HOL
May 01 10:30:17 Starting developers
May 01 10:30:22 Finished developers                                               5s 116MB
May 01 10:30:22 Starting developers/bin
May 01 10:30:28 Finished developers/bin                                           5s   1GB
May 01 10:30:29 Starting compiler/proofs
May 01 12:20:03 Finished compiler/proofs                                    1h49m32s  28GB
May 01 12:20:05 Starting compiler/bootstrap/translation
May 01 20:24:07 Finished compiler/bootstrap/translation                     8h04m01s  33GB
May 01 20:24:07 Starting semantics/ffi
May 01 20:24:13 Finished semantics/ffi                                            6s 219MB
May 01 20:24:13 Starting semantics
May 01 20:24:15 Finished semantics                                                1s  19MB
May 01 20:24:15 Starting semantics/proofs
May 01 20:24:47 Finished semantics/proofs                                        32s 730MB
May 01 20:24:47 Starting semantics/alt_semantics
May 01 20:25:19 Finished semantics/alt_semantics                                 32s 794MB
May 01 20:25:19 Starting semantics/alt_semantics/proofs
May 01 20:37:06 Finished semantics/alt_semantics/proofs                       11m46s   3GB
May 01 20:37:06 Starting basis/pure
May 01 20:37:08 Finished basis/pure                                               1s  24MB
May 01 20:37:08 Starting translator
May 01 20:38:59 Finished translator                                            1m51s   1GB
May 01 20:38:59 Starting compiler/parsing
May 01 20:39:01 Finished compiler/parsing                                         1s  17MB
May 01 20:39:01 Starting characteristic
May 01 20:39:03 Finished characteristic                                           1s  19MB
May 01 20:39:03 Starting translator/monadic
May 01 20:39:05 Finished translator/monadic                                       1s  23MB
May 01 20:39:05 Starting basis
May 01 20:43:04 Finished basis                                                 3m58s   3GB
May 01 20:43:04 Starting compiler/inference
May 01 20:43:06 Finished compiler/inference                                       1s  23MB
May 01 20:43:06 Starting compiler/backend/reg_alloc
May 01 20:43:08 Finished compiler/backend/reg_alloc                               1s  20MB
May 01 20:43:08 Starting compiler/backend/gc
May 01 20:43:10 Finished compiler/backend/gc                                      2s  26MB
May 01 20:43:10 Starting compiler/backend
May 01 20:43:22 Finished compiler/backend                                        11s 759MB
May 01 20:43:22 Starting compiler/encoders/asm
May 01 20:43:24 Finished compiler/encoders/asm                                    1s  19MB
May 01 20:43:24 Starting compiler/encoders/x64
May 01 20:43:26 Finished compiler/encoders/x64                                    1s  22MB
May 01 20:43:26 Starting compiler/encoders/arm7
May 01 20:43:28 Finished compiler/encoders/arm7                                   1s  20MB
May 01 20:43:28 Starting compiler/encoders/arm8
May 01 20:43:29 Finished compiler/encoders/arm8                                   1s  25MB
May 01 20:43:30 Starting compiler/encoders/arm8_asl
May 01 20:46:46 Finished compiler/encoders/arm8_asl                            3m15s   1GB
May 01 20:46:46 Starting compiler/encoders/mips
May 01 20:46:48 Finished compiler/encoders/mips                                   1s  19MB
May 01 20:46:48 Starting compiler/encoders/riscv
May 01 20:46:49 Finished compiler/encoders/riscv                                  1s  22MB
May 01 20:46:50 Starting compiler/encoders/ag32
May 01 20:46:51 Finished compiler/encoders/ag32                                   1s  21MB
May 01 20:46:51 Starting compiler/backend/x64
May 01 20:46:54 Finished compiler/backend/x64                                     2s  23MB
May 01 20:46:54 Starting compiler/backend/arm7
May 01 20:46:56 Finished compiler/backend/arm7                                    2s  24MB
May 01 20:46:56 Starting compiler/backend/arm8
May 01 20:46:58 Finished compiler/backend/arm8                                    2s  26MB
May 01 20:46:58 Starting compiler/backend/mips
May 01 20:47:01 Finished compiler/backend/mips                                    2s  22MB
May 01 20:47:01 Starting compiler/backend/riscv
May 01 20:47:03 Finished compiler/backend/riscv                                   2s  28MB
May 01 20:47:03 Starting compiler/backend/ag32
May 01 20:48:31 Finished compiler/backend/ag32                                 1m27s   1GB
May 01 20:48:31 Starting compiler/parsing/proofs
May 01 20:48:32 Finished compiler/parsing/proofs                                  1s  21MB
May 01 20:48:33 Starting compiler/inference/proofs
May 01 20:48:34 Finished compiler/inference/proofs                                1s  22MB
May 01 20:48:35 Starting compiler/backend/semantics
May 01 20:49:46 Finished compiler/backend/semantics                            1m11s   1GB
May 01 20:49:47 Starting compiler/backend/reg_alloc/proofs
May 01 20:49:49 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
May 01 20:49:49 Starting compiler/backend/proofs
May 01 20:50:48 Finished compiler/backend/proofs                                 59s   3GB
May 01 20:50:48 Starting compiler/backend/serialiser
May 01 20:50:51 Finished compiler/backend/serialiser                              2s  33MB
May 01 20:50:51 Starting compiler/encoders/x64/proofs
May 01 21:00:42 Finished compiler/encoders/x64/proofs                          9m50s   6GB
May 01 21:00:42 Starting compiler/encoders/arm7/proofs
May 01 21:14:29 Finished compiler/encoders/arm7/proofs                        13m46s   4GB
May 01 21:14:29 Starting compiler/encoders/arm8/proofs
May 01 21:21:25 Finished compiler/encoders/arm8/proofs                         6m55s   1GB
May 01 21:21:25 Starting compiler/encoders/arm8_asl/proofs
May 01 21:37:10 Finished compiler/encoders/arm8_asl/proofs                    15m44s   2GB
May 01 21:37:10 Starting compiler/encoders/mips/proofs
May 01 21:48:01 Finished compiler/encoders/mips/proofs                        10m49s   2GB
May 01 21:48:01 Starting compiler/encoders/riscv/proofs
May 01 21:56:57 Finished compiler/encoders/riscv/proofs                        8m56s   2GB
May 01 21:56:57 Starting compiler/encoders/ag32/proofs
May 01 21:59:37 Finished compiler/encoders/ag32/proofs                         2m40s 916MB
May 01 21:59:37 Starting compiler/backend/x64/proofs
May 01 22:00:06 Finished compiler/backend/x64/proofs                             28s   1GB
May 01 22:00:06 Starting compiler/backend/arm7/proofs
May 01 22:00:39 Finished compiler/backend/arm7/proofs                            32s   2GB
May 01 22:00:39 Starting compiler/backend/arm8/proofs
May 01 22:01:09 Finished compiler/backend/arm8/proofs                            30s   1GB
May 01 22:01:09 Starting compiler/backend/arm8_asl
May 01 22:01:33 Finished compiler/backend/arm8_asl                               23s   1GB
May 01 22:01:33 Starting compiler/backend/mips/proofs
May 01 22:02:04 Finished compiler/backend/mips/proofs                            30s   1GB
May 01 22:02:04 Starting compiler/backend/riscv/proofs
May 01 22:02:38 Finished compiler/backend/riscv/proofs                           33s   2GB
May 01 22:02:38 Starting compiler/backend/ag32/proofs
May 01 22:16:23 Finished compiler/backend/ag32/proofs                         13m44s   3GB
May 01 22:16:23 Starting candle/set-theory
May 01 22:17:03 Finished candle/set-theory                                       39s   1GB
May 01 22:17:03 Starting candle/syntax-lib
May 01 22:17:04 Finished candle/syntax-lib                                        1s  20MB
May 01 22:17:05 Starting candle/standard/syntax
May 01 22:17:15 Finished candle/standard/syntax                                  10s 712MB
May 01 22:17:15 Starting candle/standard/semantics
May 01 22:19:13 Finished candle/standard/semantics                             1m57s   1GB
May 01 22:19:13 Starting candle/standard/monadic
May 01 22:19:15 Finished candle/standard/monadic                                  1s  28MB
May 01 22:19:15 Starting candle/standard/ml_kernel
May 01 22:20:54 Finished candle/standard/ml_kernel                             1m38s   2GB
May 01 22:20:54 Starting candle/overloading/syntax
May 01 22:24:15 Finished candle/overloading/syntax                             3m20s   1GB
May 01 22:24:15 Starting candle/overloading/semantics
May 01 22:36:24 Finished candle/overloading/semantics                         12m08s   2GB
May 01 22:36:24 Starting candle/overloading/monadic
May 01 22:39:04 Finished candle/overloading/monadic                            2m39s   1GB
May 01 22:39:04 Starting candle/overloading/ml_kernel
May 01 22:46:53 Finished candle/overloading/ml_kernel                          7m48s   3GB
May 01 22:46:53 Starting candle/overloading/ml_checker
May 01 22:49:30 Finished candle/overloading/ml_checker                         2m37s   2GB
May 01 22:49:30 Starting candle/prover
May 01 22:59:23 Finished candle/prover                                         9m53s   4GB
May 01 22:59:24 Starting pancake
May 01 23:00:08 Finished pancake                                                 43s 904MB
May 01 23:00:08 Starting pancake/ffi
May 01 23:00:08 Finished pancake/ffi                                              0s  12MB
May 01 23:00:08 Starting pancake/semantics
May 01 23:02:38 Finished pancake/semantics                                     2m29s   1GB
May 01 23:02:38 Starting pancake/proofs
May 01 23:06:49 Finished pancake/proofs                                        4m10s   2GB
May 01 23:06:49 Starting characteristic/examples
May 01 23:08:19 Finished characteristic/examples                               1m29s   2GB
May 01 23:08:19 Starting tutorial/solutions
May 01 23:23:26 Finished tutorial/solutions                                   15m07s  10GB
May 01 23:23:26 Starting translator/monadic/examples
May 01 23:27:29 Finished translator/monadic/examples                           4m02s   3GB
May 01 23:27:29 Starting examples
May 01 23:43:29 Finished examples                                             15m58s   4GB
May 01 23:43:29 Starting examples/compilation/x64
May 02 01:43:52 Finished examples/compilation/x64                           2h00m19s  14GB
May 02 01:43:52 Starting examples/compilation/x64/proofs
May 02 01:46:20 Finished examples/compilation/x64/proofs                       2m27s   4GB
May 02 01:46:20 Starting examples/compilation/ag32
May 02 02:17:18 Finished examples/compilation/ag32                            30m57s   7GB
May 02 02:17:18 Starting examples/compilation/ag32/proofs
May 02 02:18:22 Finished examples/compilation/ag32/proofs                      1m03s   5GB
May 02 02:18:22 Starting examples/compilation/to_word
May 02 02:21:44 Finished examples/compilation/to_word                          3m21s   6GB
May 02 02:21:44 Starting examples/lpr_checker
May 02 02:22:49 Finished examples/lpr_checker                                  1m04s   1GB
May 02 02:22:49 Starting examples/lpr_checker/array
May 02 02:59:42 Finished examples/lpr_checker/array                           36m52s   9GB
May 02 02:59:42 Starting examples/lpr_checker/array/compilation
May 02 03:39:31 Finished examples/lpr_checker/array/compilation               39m48s  25GB
May 02 03:39:31 Starting examples/lpr_checker/array/compilation/proofs
May 02 03:40:59 Finished examples/lpr_checker/array/compilation/proofs         1m27s   5GB
May 02 03:40:59 Starting examples/opentheory
May 02 03:51:53 Finished examples/opentheory                                  10m54s   4GB
May 02 03:51:53 Starting examples/opentheory
May 02 03:51:55 Finished examples/opentheory                                      1s  23MB
May 02 03:51:55 Starting examples/opentheory/compilation
May 02 04:28:41 Finished examples/opentheory/compilation                      36m43s  29GB
May 02 04:28:42 Starting examples/opentheory/compilation/proofs
May 02 04:29:41 Finished examples/opentheory/compilation/proofs                  58s   4GB
May 02 04:29:41 Starting examples/opentheory/compilation/ag32
May 02 05:02:03 Finished examples/opentheory/compilation/ag32                 32m21s  27GB
May 02 05:02:03 Starting examples/opentheory/compilation/ag32/proofs
May 02 05:03:57 Finished examples/opentheory/compilation/ag32/proofs           1m54s   7GB
May 02 05:03:58 Starting examples/sat_encodings
May 02 05:05:58 Finished examples/sat_encodings                                2m00s 969MB
May 02 05:05:58 Starting examples/sat_encodings/case_studies
May 02 05:07:48 Finished examples/sat_encodings/case_studies                   1m49s   1GB
May 02 05:07:48 Starting examples/sat_encodings/translation
May 02 05:13:56 Finished examples/sat_encodings/translation                    6m07s   4GB
May 02 05:13:56 Starting examples/sat_encodings/translation/compilation
May 02 05:59:59 Finished examples/sat_encodings/translation/compilation       46m01s  19GB
May 02 05:59:59 Starting examples/deflate
May 02 06:00:59 Finished examples/deflate                                      1m00s 776MB
May 02 06:00:59 Starting examples/deflate/translation
May 02 06:02:56 Finished examples/deflate/translation                          1m56s   3GB
May 02 06:02:56 Starting examples/deflate/translation/compilation
May 02 06:22:56 Finished examples/deflate/translation/compilation             20m00s  12GB
May 02 06:22:56 Starting translator/okasaki-examples
May 02 06:28:10 Finished translator/okasaki-examples                           5m13s   1GB
May 02 06:28:10 Starting translator/other-examples
May 02 06:29:04 Finished translator/other-examples                               53s   1GB
May 02 06:29:05 Starting compiler/parsing/tests
May 02 06:29:37 Finished compiler/parsing/tests                                  32s 784MB
May 02 06:29:37 Starting compiler/inference/tests
May 02 06:38:01 Finished compiler/inference/tests                              8m24s   4GB
May 02 06:38:01 Starting compiler/printing/test
May 02 06:41:51 Finished compiler/printing/test                                3m49s   3GB
May 02 06:41:51 Starting icing/flover
May 02 07:25:00 Finished icing/flover                                         43m07s   2GB
May 02 07:25:00 Starting icing/
May 02 08:21:07 Finished icing/                                               56m06s   7GB
May 02 08:21:07 Starting icing/examples
May 02 08:22:37 Finished icing/examples                                        1m30s   5GB
May 02 08:22:37 Starting compiler/repl
May 02 08:31:14 Finished compiler/repl                                         8m34s   5GB
May 02 08:31:14 Starting unverified/sexpr-bootstrap/x64/64
May 02 08:44:38 Finished unverified/sexpr-bootstrap/x64/64                    13m24s  16GB
May 02 08:44:38 Starting unverified/sexpr-bootstrap/x64/32
May 02 08:55:25 Finished unverified/sexpr-bootstrap/x64/32                    10m46s  13GB
May 02 08:55:25 Starting compiler/benchmarks
May 02 09:10:46 Finished compiler/benchmarks                                  15m20s   2GB
May 02 09:10:46 Starting compiler/bootstrap/compilation/x64/64
May 02 21:18:32 Finished compiler/bootstrap/compilation/x64/64             12h07m44s  64GB
May 02 21:18:32 Starting compiler/bootstrap/compilation/x64/64/proofs
May 02 21:38:55 Finished compiler/bootstrap/compilation/x64/64/proofs         20m22s  39GB
May 02 21:38:56 Starting compiler/bootstrap/compilation/x64/32
May 03 04:33:18 Finished compiler/bootstrap/compilation/x64/32              6h54m21s  63GB
May 03 04:33:18 Starting compiler/bootstrap/compilation/x64/32/proofs
May 03 04:36:38 Finished compiler/bootstrap/compilation/x64/32/proofs          3m19s  20GB
May 03 04:36:38 Starting compiler/bootstrap/compilation/ag32/32
May 03 11:37:49 Finished compiler/bootstrap/compilation/ag32/32             7h01m10s  64GB
May 03 11:37:50 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 03 11:44:34 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m44s  38GB
May 03 11:44:34 SUCCESS