Job 2116

CakeML:da61472bef3d531cd3dcabd8872dcf60e7c544c5
  Finish proving safety of code for counting allocations [Mar 22 22:00:23]
#946 (count_allocations)
Merging into:4a59cb87727545e08ff4cf881911dcf91010657a
  Merge pull request #927 from CakeML/translation_update [Mar 20 11:33:19]
HOL:ff6e145992db7e75ae6798231ce09c3cc03538df
  Modernise a theorem's syntax [Feb 03 10:08:02]
Machine:oven2+4.15.0-34-generic+x86_64+GNU/Linux

Mar 22 22:06:12 Claimed job
Mar 22 22:06:24 Building+HOL
Mar 22 22:34:47 Starting+developers
Mar 22 22:34:48 Finished+developers++++++++++++++++++++++++++++++++++++++++0.19+37248
Mar 22 22:34:48 Starting+developers/bin
Mar 22 22:34:54 Finished+developers/bin++++++++++++++++++++++++++++++++++++6.12+1244324
Mar 22 22:34:54 Starting+compiler/proofs
Mar 23 02:05:51 Finished+compiler/proofs+++++++++++++++++++++++++++++++++++12656.51+29543344
Mar 23 02:05:51 Starting+compiler/bootstrap/translation
Mar 23 11:30:16 Finished compiler/bootstrap/translation                     9h24m24s  41GB
Mar 23 11:30:16 Starting semantics/ffi
Mar 23 11:30:25 Finished semantics/ffi                                            8s 567MB
Mar 23 11:30:25 Starting semantics
Mar 23 11:30:26 Finished semantics                                                0s  74MB
Mar 23 11:30:26 Starting semantics/proofs
Mar 23 11:31:03 Finished semantics/proofs                                        37s   1GB
Mar 23 11:31:03 Starting semantics/alt_semantics
Mar 23 11:31:47 Finished semantics/alt_semantics                                 43s   1GB
Mar 23 11:31:47 Starting semantics/alt_semantics/proofs
Mar 23 11:43:53 Finished semantics/alt_semantics/proofs                       12m05s   4GB
Mar 23 11:43:53 Starting basis/pure
Mar 23 11:43:54 Finished basis/pure                                               0s  82MB
Mar 23 11:43:54 Starting translator
Mar 23 11:45:54 Finished translator                                            1m59s   3GB
Mar 23 11:45:54 Starting compiler/parsing
Mar 23 11:45:55 Finished compiler/parsing                                         0s  82MB
Mar 23 11:45:55 Starting characteristic
Mar 23 11:45:56 Finished characteristic                                           1s 108MB
Mar 23 11:45:56 Starting translator/monadic
Mar 23 11:45:57 Finished translator/monadic                                       1s 103MB
Mar 23 11:45:58 Starting basis
Mar 23 11:50:29 Finished basis                                                 4m31s   5GB
Mar 23 11:50:29 Starting compiler/inference
Mar 23 11:50:30 Finished compiler/inference                                       0s  91MB
Mar 23 11:50:31 Starting compiler/backend/reg_alloc
Mar 23 11:50:31 Finished compiler/backend/reg_alloc                               0s  75MB
Mar 23 11:50:31 Starting compiler/backend/gc
Mar 23 11:50:33 Finished compiler/backend/gc                                      1s 150MB
Mar 23 11:50:33 Starting compiler/backend
Mar 23 11:50:53 Finished compiler/backend                                        18s   1GB
Mar 23 11:50:53 Starting compiler/encoders/asm
Mar 23 11:50:54 Finished compiler/encoders/asm                                    0s 103MB
Mar 23 11:50:54 Starting compiler/encoders/x64
Mar 23 11:50:55 Finished compiler/encoders/x64                                    1s 108MB
Mar 23 11:50:55 Starting compiler/encoders/arm7
Mar 23 11:50:56 Finished compiler/encoders/arm7                                   1s 109MB
Mar 23 11:50:57 Starting compiler/encoders/arm8
Mar 23 11:50:58 Finished compiler/encoders/arm8                                   0s 104MB
Mar 23 11:50:58 Starting compiler/encoders/arm8_asl
Mar 23 14:29:03 Finished compiler/encoders/arm8_asl                         2h38m04s  39GB
Mar 23 14:29:03 Starting compiler/encoders/mips
Mar 23 14:29:05 Finished compiler/encoders/mips                                   0s 103MB
Mar 23 14:29:05 Starting compiler/encoders/riscv
Mar 23 14:29:06 Finished compiler/encoders/riscv                                  0s  99MB
Mar 23 14:29:06 Starting compiler/encoders/ag32
Mar 23 14:29:07 Finished compiler/encoders/ag32                                   0s  98MB
Mar 23 14:29:07 Starting compiler/backend/x64
Mar 23 14:29:09 Finished compiler/backend/x64                                     1s 137MB
Mar 23 14:29:09 Starting compiler/backend/arm7
Mar 23 14:29:11 Finished compiler/backend/arm7                                    1s 136MB
Mar 23 14:29:11 Starting compiler/backend/arm8
Mar 23 14:29:13 Finished compiler/backend/arm8                                    1s 136MB
Mar 23 14:29:13 Starting compiler/backend/mips
Mar 23 14:29:14 Finished compiler/backend/mips                                    1s 136MB
Mar 23 14:29:15 Starting compiler/backend/riscv
Mar 23 14:29:16 Finished compiler/backend/riscv                                   1s 137MB
Mar 23 14:29:16 Starting compiler/backend/ag32
Mar 23 14:30:50 Finished compiler/backend/ag32                                 1m33s   2GB
Mar 23 14:30:50 Starting compiler/parsing/proofs
Mar 23 14:30:51 Finished compiler/parsing/proofs                                  0s  86MB
Mar 23 14:30:51 Starting compiler/inference/proofs
Mar 23 14:30:52 Finished compiler/inference/proofs                                0s  98MB
Mar 23 14:30:52 Starting compiler/backend/semantics
Mar 23 14:32:28 Finished compiler/backend/semantics                            1m35s   2GB
Mar 23 14:32:28 Starting compiler/backend/reg_alloc/proofs
Mar 23 14:32:29 Finished compiler/backend/reg_alloc/proofs                        1s 110MB
Mar 23 14:32:29 Starting compiler/backend/proofs
Mar 23 14:33:36 Finished compiler/backend/proofs                               1m05s   3GB
Mar 23 14:33:36 Starting compiler/backend/serialiser
Mar 23 14:33:38 Finished compiler/backend/serialiser                              2s 199MB
Mar 23 14:33:38 Starting compiler/encoders/x64/proofs
Mar 23 14:44:04 Finished compiler/encoders/x64/proofs                         10m24s   5GB
Mar 23 14:44:04 Starting compiler/encoders/arm7/proofs
Mar 23 14:58:09 Finished compiler/encoders/arm7/proofs                        14m04s   8GB
Mar 23 14:58:09 Starting compiler/encoders/arm8/proofs
Mar 23 15:05:34 Finished compiler/encoders/arm8/proofs                         7m24s   3GB
Mar 23 15:05:34 Starting compiler/encoders/arm8_asl/proofs
Mar 23 15:57:36 Finished compiler/encoders/arm8_asl/proofs                    52m02s  10GB
Mar 23 15:57:36 Starting compiler/encoders/mips/proofs
Mar 23 16:08:36 Finished compiler/encoders/mips/proofs                        10m59s   6GB
Mar 23 16:08:36 Starting compiler/encoders/riscv/proofs
Mar 23 16:17:42 Finished compiler/encoders/riscv/proofs                        9m05s   3GB
Mar 23 16:17:42 Starting compiler/encoders/ag32/proofs
Mar 23 16:20:18 Finished compiler/encoders/ag32/proofs                         2m36s   1GB
Mar 23 16:20:19 Starting compiler/backend/x64/proofs
Mar 23 16:21:03 Finished compiler/backend/x64/proofs                             44s   2GB
Mar 23 16:21:03 Starting compiler/backend/arm7/proofs
Mar 23 16:21:50 Finished compiler/backend/arm7/proofs                            46s   2GB
Mar 23 16:21:50 Starting compiler/backend/arm8/proofs
Mar 23 16:22:33 Finished compiler/backend/arm8/proofs                            43s   3GB
Mar 23 16:22:33 Starting compiler/backend/arm8_asl
Mar 23 16:23:06 Finished compiler/backend/arm8_asl                               32s   2GB
Mar 23 16:23:06 Starting compiler/backend/mips/proofs
Mar 23 16:23:55 Finished compiler/backend/mips/proofs                            48s   3GB
Mar 23 16:23:55 Starting compiler/backend/riscv/proofs
Mar 23 16:24:49 Finished compiler/backend/riscv/proofs                           54s   4GB
Mar 23 16:24:50 Starting compiler/backend/ag32/proofs
Mar 23 16:39:12 Finished compiler/backend/ag32/proofs                         14m22s   5GB
Mar 23 16:39:12 Starting candle/set-theory
Mar 23 16:40:04 Finished candle/set-theory                                       51s   1GB
Mar 23 16:40:04 Starting candle/syntax-lib
Mar 23 16:40:05 Finished candle/syntax-lib                                        0s  88MB
Mar 23 16:40:05 Starting candle/standard/syntax
Mar 23 16:40:22 Finished candle/standard/syntax                                  16s   1GB
Mar 23 16:40:22 Starting candle/standard/semantics
Mar 23 16:43:01 Finished candle/standard/semantics                             2m38s   2GB
Mar 23 16:43:01 Starting candle/standard/monadic
Mar 23 16:43:02 Finished candle/standard/monadic                                  1s 108MB
Mar 23 16:43:02 Starting candle/standard/ml_kernel
Mar 23 16:45:02 Finished candle/standard/ml_kernel                             1m59s   4GB
Mar 23 16:45:02 Starting candle/overloading/syntax
Mar 23 16:48:48 Finished candle/overloading/syntax                             3m46s   2GB
Mar 23 16:48:48 Starting candle/overloading/semantics
Mar 23 17:01:14 Finished candle/overloading/semantics                         12m25s   5GB
Mar 23 17:01:14 Starting candle/overloading/monadic
Mar 23 17:04:07 Finished candle/overloading/monadic                            2m52s   2GB
Mar 23 17:04:07 Starting candle/overloading/ml_kernel
Mar 23 17:12:36 Finished candle/overloading/ml_kernel                          8m28s   6GB
Mar 23 17:12:36 Starting candle/overloading/ml_checker
Mar 23 17:15:25 Finished candle/overloading/ml_checker                         2m49s   6GB
Mar 23 17:15:25 Starting candle/prover
Mar 23 17:26:20 Finished candle/prover                                        10m54s   5GB
Mar 23 17:26:20 Starting pancake
Mar 23 17:27:27 Finished pancake                                               1m06s   1GB
Mar 23 17:27:27 Starting pancake/ffi
Mar 23 17:27:27 Finished pancake/ffi                                              0s  24MB
Mar 23 17:27:27 Starting pancake/semantics
Mar 23 17:30:26 Finished pancake/semantics                                     2m58s   2GB
Mar 23 17:30:27 Starting pancake/proofs
Mar 23 17:35:26 Finished pancake/proofs                                        4m59s   5GB
Mar 23 17:35:26 Starting characteristic/examples
Mar 23 17:37:13 Finished characteristic/examples                               1m46s   6GB
Mar 23 17:37:13 Starting tutorial/solutions
Mar 23 17:54:49 Finished tutorial/solutions                                   17m35s  20GB
Mar 23 17:54:49 Starting translator/monadic/examples
Mar 23 18:00:22 Finished translator/monadic/examples                           5m33s   5GB
Mar 23 18:00:22 Starting examples
Mar 23 18:21:59 Finished examples                                             21m35s   7GB
Mar 23 18:21:59 Starting examples/compilation/x64
Mar 23 20:28:11 Finished examples/compilation/x64                           2h06m11s  19GB
Mar 23 20:28:11 Starting examples/compilation/x64/proofs
Mar 23 20:33:20 Finished examples/compilation/x64/proofs                       5m09s   5GB
Mar 23 20:33:21 Starting examples/compilation/ag32
Mar 23 21:05:34 Finished examples/compilation/ag32                            32m13s  12GB
Mar 23 21:05:35 Starting examples/compilation/ag32/proofs
Mar 23 21:07:25 Finished examples/compilation/ag32/proofs                      1m50s   6GB
Mar 23 21:07:25 Starting examples/compilation/to_word
Mar 23 21:11:50 Finished examples/compilation/to_word                          4m24s  11GB
Mar 23 21:11:50 Starting examples/lpr_checker
Mar 23 21:13:14 Finished examples/lpr_checker                                  1m24s   2GB
Mar 23 21:13:14 Starting examples/lpr_checker/array
Mar 23 22:05:49 Finished examples/lpr_checker/array                           52m33s   9GB
Mar 23 22:05:49 Starting examples/lpr_checker/array/compilation
Mar 23 23:14:31 Finished examples/lpr_checker/array/compilation             1h08m41s  34GB
Mar 23 23:14:31 Starting examples/lpr_checker/array/compilation/proofs
Mar 23 23:16:50 Finished examples/lpr_checker/array/compilation/proofs         2m18s  10GB
Mar 23 23:16:50 Starting examples/opentheory
Mar 23 23:28:47 Finished examples/opentheory                                  11m56s   7GB
Mar 23 23:28:47 Starting examples/opentheory
Mar 23 23:28:48 Finished examples/opentheory                                      1s 142MB
Mar 23 23:28:49 Starting examples/opentheory/compilation
Mar 24 00:12:44 Finished examples/opentheory/compilation                      43m55s  28GB
Mar 24 00:12:44 Starting examples/opentheory/compilation/proofs
Mar 24 00:15:54 Finished examples/opentheory/compilation/proofs                3m09s   6GB
Mar 24 00:15:55 Starting examples/opentheory/compilation/ag32
Mar 24 01:38:49 Finished examples/opentheory/compilation/ag32               1h22m53s  42GB
Mar 24 01:38:49 Starting examples/opentheory/compilation/ag32/proofs
Mar 24 01:43:48 Finished examples/opentheory/compilation/ag32/proofs           4m58s  11GB
Mar 24 01:43:48 Starting examples/sat_encodings
Mar 24 01:48:44 Finished examples/sat_encodings                                4m55s   1GB
Mar 24 01:48:44 Starting examples/sat_encodings/case_studies
Mar 24 01:52:26 Finished examples/sat_encodings/case_studies                   3m41s   2GB
Mar 24 01:52:26 Starting examples/sat_encodings/translation
Mar 24 02:03:15 Finished examples/sat_encodings/translation                   10m48s   7GB
Mar 24 02:03:15 Starting examples/sat_encodings/translation/compilation
Mar 24 03:12:30 Finished examples/sat_encodings/translation/compilation     1h09m14s  16GB
Mar 24 03:12:31 Starting examples/deflate
Mar 24 03:14:12 Finished examples/deflate                                      1m40s   1GB
Mar 24 03:14:12 Starting examples/deflate/translation
Mar 24 03:17:03 Finished examples/deflate/translation                          2m51s   7GB
Mar 24 03:17:03 Starting examples/deflate/translation/compilation
Mar 24 03:48:23 Finished examples/deflate/translation/compilation             31m20s  22GB
Mar 24 03:48:23 Starting translator/okasaki-examples
Mar 24 03:55:01 Finished translator/okasaki-examples                           6m37s   3GB
Mar 24 03:55:01 Starting translator/other-examples
Mar 24 04:00:29 Finished translator/other-examples                             5m27s   3GB
Mar 24 04:00:29 Starting compiler/parsing/tests
Mar 24 04:01:09 Finished compiler/parsing/tests                                  39s   1GB
Mar 24 04:01:09 Starting compiler/inference/tests
Mar 24 04:09:40 Finished compiler/inference/tests                              8m30s   6GB
Mar 24 04:09:40 Starting compiler/printing/test
Mar 24 04:13:35 Finished compiler/printing/test                                3m54s   6GB
Mar 24 04:13:35 Starting icing/flover
Mar 24 04:56:48 Finished icing/flover                                         43m13s   4GB
Mar 24 04:56:49 Starting icing/
Mar 24 06:01:04 Finished icing/                                             1h04m15s  21GB
Mar 24 06:01:04 Starting icing/examples
Mar 24 06:02:58 Finished icing/examples                                        1m53s   8GB
Mar 24 06:02:58 Starting compiler/repl
Mar 24 06:12:32 Finished compiler/repl                                         9m33s   9GB
Mar 24 06:12:32 Starting unverified/sexpr-bootstrap/x64/64
Mar 24 06:27:13 Finished unverified/sexpr-bootstrap/x64/64                    14m41s  15GB
Mar 24 06:27:13 Starting unverified/sexpr-bootstrap/x64/32
Mar 24 06:39:07 Finished unverified/sexpr-bootstrap/x64/32                    11m53s  14GB
Mar 24 06:39:07 Starting compiler/benchmarks
Mar 24 07:18:37 Finished compiler/benchmarks                                  39m29s   2GB
Mar 24 07:18:38 Starting compiler/bootstrap/compilation/x64/64
Mar 25 00:40:41 Finished compiler/bootstrap/compilation/x64/64             17h22m01s  54GB
Mar 25 00:40:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 25 01:02:22 Finished compiler/bootstrap/compilation/x64/64/proofs         21m40s  44GB
Mar 25 01:02:22 Starting compiler/bootstrap/compilation/x64/32
Mar 25 09:49:43 Finished compiler/bootstrap/compilation/x64/32              8h47m19s  54GB
Mar 25 09:49:43 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 25 09:53:32 Finished compiler/bootstrap/compilation/x64/32/proofs          3m48s  18GB
Mar 25 09:53:32 Starting compiler/bootstrap/compilation/ag32/32
Mar 25 18:46:00 Finished compiler/bootstrap/compilation/ag32/32             8h52m28s  54GB
Mar 25 18:46:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 25 18:54:03 Finished compiler/bootstrap/compilation/ag32/32/proofs         8m02s  47GB
Mar 25 18:54:03 SUCCESS