Job 1559

CakeML:76ed0b05089a77059dee72d197fc56c3dae661e8
  Merge pull request #829 from CakeML/help [Jun 18 08:39:57]
HOL:da1da5d92ca33777c3fd5f1e31dad3b5e954534c
  Removed wrongly added TABs (unicode violations) in the previous commit [Jul 27 03:02:16]
Machine:oven3 4.19.67.1.amd64-smp

Jul 29 05:07:53 Claimed job
Jul 29 05:08:08 Building HOL
Jul 29 05:40:43 Starting developers
Jul 29 05:40:51 Finished developers                                               8s 112MB
Jul 29 05:40:51 Starting developers/bin
Jul 29 05:41:04 Finished developers/bin                                          12s   1GB
Jul 29 05:41:04 Starting semantics/ffi
Jul 29 05:41:29 Finished semantics/ffi                                           25s 259MB
Jul 29 05:41:30 Starting semantics
Jul 29 05:44:38 Finished semantics                                             3m08s   1GB
Jul 29 05:44:38 Starting semantics/proofs
Jul 29 05:52:30 Finished semantics/proofs                                      7m50s   1GB
Jul 29 05:52:30 Starting semantics/alt_semantics
Jul 29 05:52:51 Finished semantics/alt_semantics                                 21s 358MB
Jul 29 05:52:52 Starting semantics/alt_semantics/proofs
Jul 29 05:57:38 Finished semantics/alt_semantics/proofs                        4m46s   1GB
Jul 29 05:57:38 Starting basis/pure
Jul 29 06:03:43 Finished basis/pure                                            6m04s 821MB
Jul 29 06:03:43 Starting translator
Jul 29 06:10:30 Finished translator                                            6m46s   1GB
Jul 29 06:10:30 Starting compiler/parsing
Jul 29 06:13:03 Finished compiler/parsing                                      2m33s   3GB
Jul 29 06:13:04 Starting characteristic
Jul 29 06:25:26 Finished characteristic                                       12m22s   1GB
Jul 29 06:25:27 Starting translator/monadic
Jul 29 06:28:55 Finished translator/monadic                                    3m28s   1GB
Jul 29 06:28:55 Starting basis
Jul 29 08:04:04 Finished basis                                              1h35m08s  22GB
Jul 29 08:04:05 Starting compiler/inference
Jul 29 08:06:48 Finished compiler/inference                                    2m42s   1GB
Jul 29 08:06:48 Starting compiler/backend/reg_alloc
Jul 29 08:08:56 Finished compiler/backend/reg_alloc                            2m07s   1GB
Jul 29 08:08:56 Starting compiler/backend/gc
Jul 29 08:15:52 Finished compiler/backend/gc                                   6m55s   2GB
Jul 29 08:15:52 Starting compiler/backend
Jul 29 08:25:22 Finished compiler/backend                                      9m29s   4GB
Jul 29 08:25:22 Starting compiler/encoders/asm
Jul 29 08:26:11 Finished compiler/encoders/asm                                   48s 718MB
Jul 29 08:26:11 Starting compiler/encoders/x64
Jul 29 08:28:29 Finished compiler/encoders/x64                                 2m17s 801MB
Jul 29 08:28:29 Starting compiler/encoders/arm7
Jul 29 08:33:15 Finished compiler/encoders/arm7                                4m46s   1GB
Jul 29 08:33:16 Starting compiler/encoders/arm8
Jul 29 08:34:42 Finished compiler/encoders/arm8                                1m26s 709MB
Jul 29 08:34:42 Starting compiler/encoders/mips
Jul 29 08:37:55 Finished compiler/encoders/mips                                3m12s   1GB
Jul 29 08:37:55 Starting compiler/encoders/riscv
Jul 29 08:41:45 Finished compiler/encoders/riscv                               3m50s 911MB
Jul 29 08:41:46 Starting compiler/encoders/ag32
Jul 29 08:42:24 Finished compiler/encoders/ag32                                  37s 704MB
Jul 29 08:42:24 Starting compiler/backend/x64
Jul 29 08:43:01 Finished compiler/backend/x64                                    36s   1GB
Jul 29 08:43:01 Starting compiler/backend/arm7
Jul 29 08:43:42 Finished compiler/backend/arm7                                   41s   1GB
Jul 29 08:43:43 Starting compiler/backend/arm8
Jul 29 08:44:26 Finished compiler/backend/arm8                                   42s   1GB
Jul 29 08:44:26 Starting compiler/backend/mips
Jul 29 08:45:08 Finished compiler/backend/mips                                   41s   1GB
Jul 29 08:45:08 Starting compiler/backend/riscv
Jul 29 08:45:53 Finished compiler/backend/riscv                                  44s   1GB
Jul 29 08:45:53 Starting compiler/backend/ag32
Jul 29 08:48:19 Finished compiler/backend/ag32                                 2m25s   1GB
Jul 29 08:48:20 Starting compiler/parsing/proofs
Jul 29 09:01:05 Finished compiler/parsing/proofs                              12m45s   1GB
Jul 29 09:01:06 Starting compiler/inference/proofs
Jul 29 09:06:38 Finished compiler/inference/proofs                             5m32s   1GB
Jul 29 09:06:39 Starting compiler/backend/semantics
Jul 29 10:08:38 Finished compiler/backend/semantics                         1h01m57s   2GB
Jul 29 10:08:38 Starting compiler/backend/reg_alloc/proofs
Jul 29 10:16:16 Finished compiler/backend/reg_alloc/proofs                     7m37s   1GB
Jul 29 10:16:16 Starting compiler/backend/proofs
Jul 29 11:58:24 Finished compiler/backend/proofs                            1h42m07s  25GB
Jul 29 11:58:24 Starting compiler/encoders/x64/proofs
Jul 29 12:20:14 Finished compiler/encoders/x64/proofs                         21m49s   4GB
Jul 29 12:20:14 Starting compiler/encoders/arm7/proofs
Jul 29 12:49:55 Finished compiler/encoders/arm7/proofs                        29m40s   6GB
Jul 29 12:49:55 Starting compiler/encoders/arm8/proofs
Jul 29 13:05:27 Finished compiler/encoders/arm8/proofs                        15m30s   1GB
Jul 29 13:05:27 Starting compiler/encoders/mips/proofs
Jul 29 13:27:43 Finished compiler/encoders/mips/proofs                        22m16s   2GB
Jul 29 13:27:44 Starting compiler/encoders/riscv/proofs
Jul 29 13:47:41 Finished compiler/encoders/riscv/proofs                       19m57s   1GB
Jul 29 13:47:41 Starting compiler/encoders/ag32/proofs
Jul 29 13:53:17 Finished compiler/encoders/ag32/proofs                         5m35s 955MB
Jul 29 13:53:17 Starting compiler/backend/x64/proofs
Jul 29 13:54:06 Finished compiler/backend/x64/proofs                             48s   1GB
Jul 29 13:54:06 Starting compiler/backend/arm7/proofs
Jul 29 13:54:56 Finished compiler/backend/arm7/proofs                            49s   1GB
Jul 29 13:54:56 Starting compiler/backend/arm8/proofs
Jul 29 13:55:45 Finished compiler/backend/arm8/proofs                            48s   1GB
Jul 29 13:55:46 Starting compiler/backend/mips/proofs
Jul 29 13:56:34 Finished compiler/backend/mips/proofs                            47s   1GB
Jul 29 13:56:34 Starting compiler/backend/riscv/proofs
Jul 29 13:57:22 Finished compiler/backend/riscv/proofs                           47s   1GB
Jul 29 13:57:22 Starting compiler/backend/ag32/proofs
Jul 29 14:25:50 Finished compiler/backend/ag32/proofs                         28m27s   2GB
Jul 29 14:25:50 Starting compiler/proofs
Jul 29 14:29:55 Finished compiler/proofs                                       4m04s   3GB
Jul 29 14:29:55 Starting candle/set-theory
Jul 29 14:30:55 Finished candle/set-theory                                     1m00s 880MB
Jul 29 14:30:56 Starting candle/syntax-lib
Jul 29 14:31:18 Finished candle/syntax-lib                                       22s 713MB
Jul 29 14:31:18 Starting candle/standard/syntax
Jul 29 14:35:11 Finished candle/standard/syntax                                3m52s   1GB
Jul 29 14:35:12 Starting candle/standard/semantics
Jul 29 14:39:02 Finished candle/standard/semantics                             3m49s   1GB
Jul 29 14:39:02 Starting candle/standard/monadic
Jul 29 14:42:42 Finished candle/standard/monadic                               3m39s   1GB
Jul 29 14:42:42 Starting candle/standard/ml_kernel
Jul 29 14:54:59 Finished candle/standard/ml_kernel                            12m16s   3GB
Jul 29 14:54:59 Starting candle/overloading/syntax
Jul 29 15:01:50 Finished candle/overloading/syntax                             6m50s   1GB
Jul 29 15:01:50 Starting candle/overloading/semantics
Jul 29 15:27:54 Finished candle/overloading/semantics                         26m03s   5GB
Jul 29 15:27:54 Starting characteristic/examples
Jul 29 15:30:41 Finished characteristic/examples                               2m46s   2GB
Jul 29 15:30:42 Starting tutorial/solutions
Jul 29 16:05:00 Finished tutorial/solutions                                   34m17s   8GB
Jul 29 16:05:00 Starting translator/monadic/examples
Jul 29 16:10:38 Finished translator/monadic/examples                           5m38s   3GB
Jul 29 16:10:39 Starting examples
Jul 29 16:27:22 Finished examples                                             16m43s   3GB
Jul 29 16:27:22 Starting examples/compilation/x64
Jul 29 21:49:57 Finished examples/compilation/x64                           5h22m33s  15GB
Jul 29 21:49:57 Starting examples/compilation/x64/proofs
Jul 29 21:53:20 Finished examples/compilation/x64/proofs                       3m23s   3GB
Jul 29 21:53:20 Starting examples/compilation/ag32
Jul 29 23:12:11 Finished examples/compilation/ag32                          1h18m50s   7GB
Jul 29 23:12:11 Starting examples/compilation/ag32/proofs
Jul 29 23:14:00 Finished examples/compilation/ag32/proofs                      1m48s   4GB
Jul 29 23:14:00 Starting examples/cost
Jul 30 01:06:58 Finished examples/cost                                      1h52m56s   8GB
Jul 30 01:06:58 Starting examples/lpr_checker
Jul 30 01:15:21 Finished examples/lpr_checker                                  8m22s   3GB
Jul 30 01:15:21 Starting examples/lpr_checker/compilation
Jul 30 01:51:26 Finished examples/lpr_checker/compilation                     36m04s   9GB
Jul 30 01:51:26 Starting examples/lpr_checker/compilation/proofs
Jul 30 01:52:49 Finished examples/lpr_checker/compilation/proofs               1m22s   3GB
Jul 30 01:52:49 Starting examples/lpr_checker/array
Jul 30 02:25:26 Finished examples/lpr_checker/array                           32m36s   5GB
Jul 30 02:25:26 Starting examples/lpr_checker/array/compilation
Jul 30 03:08:54 Finished examples/lpr_checker/array/compilation               43m27s  12GB
Jul 30 03:08:54 Starting examples/lpr_checker/array/compilation/proofs
Jul 30 03:10:41 Finished examples/lpr_checker/array/compilation/proofs         1m46s   3GB
Jul 30 03:10:41 Starting examples/opentheory
Jul 30 03:31:54 Finished examples/opentheory                                  21m12s   4GB
Jul 30 03:31:54 Starting examples/opentheory
Jul 30 03:31:57 Finished examples/opentheory                                      2s  33MB
Jul 30 03:31:57 Starting examples/opentheory/compilation
Jul 30 04:41:39 Finished examples/opentheory/compilation                    1h09m41s  16GB
Jul 30 04:41:39 Starting examples/opentheory/compilation/proofs
Jul 30 04:43:09 Finished examples/opentheory/compilation/proofs                1m29s   4GB
Jul 30 04:43:10 Starting examples/opentheory/compilation/ag32
Jul 30 05:55:29 Finished examples/opentheory/compilation/ag32               1h12m19s  14GB
Jul 30 05:55:30 Starting examples/opentheory/compilation/ag32/proofs
Jul 30 05:58:52 Finished examples/opentheory/compilation/ag32/proofs           3m21s   5GB
Jul 30 05:58:52 Starting examples/sat_encodings
Jul 30 06:02:45 Finished examples/sat_encodings                                3m53s   1GB
Jul 30 06:02:45 Starting examples/sat_encodings/case_studies
Jul 30 06:06:01 Finished examples/sat_encodings/case_studies                   3m14s 795MB
Jul 30 06:06:01 Starting examples/sat_encodings/translation
Jul 30 06:17:29 Finished examples/sat_encodings/translation                   11m27s   3GB
Jul 30 06:17:29 Starting examples/sat_encodings/translation/compilation
Jul 30 07:36:05 Finished examples/sat_encodings/translation/compilation     1h18m34s  11GB
Jul 30 07:36:05 Starting translator/okasaki-examples
Jul 30 07:45:13 Finished translator/okasaki-examples                           9m07s   1GB
Jul 30 07:45:13 Starting translator/other-examples
Jul 30 07:49:14 Finished translator/other-examples                             4m00s   1GB
Jul 30 07:49:14 Starting compiler/parsing/tests
Jul 30 07:50:14 Finished compiler/parsing/tests                                1m00s 660MB
Jul 30 07:50:15 Starting compiler/inference/tests
Jul 30 08:05:59 Finished compiler/inference/tests                             15m44s   3GB
Jul 30 08:05:59 Starting compiler/bootstrap/translation
Jul 30 13:34:12 Finished compiler/bootstrap/translation                     5h28m12s  53GB
Jul 30 13:34:12 Starting unverified/sexpr-bootstrap/x64/64
Jul 30 13:58:18 Finished unverified/sexpr-bootstrap/x64/64                    24m01s   8GB
Jul 30 13:58:18 Starting unverified/sexpr-bootstrap/x64/32
Jul 30 14:19:12 Finished unverified/sexpr-bootstrap/x64/32                    20m50s   8GB
Jul 30 14:19:12 Starting compiler/benchmarks
Jul 30 14:19:16 Finished compiler/benchmarks                                      3s  33MB
Jul 30 14:19:16 Starting compiler/bootstrap/compilation/x64/64
Jul 31 15:01:12 Finished compiler/bootstrap/compilation/x64/64             24h41m52s  84GB
Jul 31 15:01:12 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 31 15:08:00 Finished compiler/bootstrap/compilation/x64/64/proofs          6m47s  14GB
Jul 31 15:08:00 Starting compiler/bootstrap/compilation/x64/32
Aug 01 14:29:54 Finished compiler/bootstrap/compilation/x64/32             23h21m50s  78GB
Aug 01 14:29:54 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 01 14:34:02 Finished compiler/bootstrap/compilation/x64/32/proofs          4m08s  14GB
Aug 01 14:34:03 Starting compiler/bootstrap/compilation/ag32/32
Aug 02 16:08:23 Finished compiler/bootstrap/compilation/ag32/32            25h34m18s 110GB
Aug 02 16:08:24 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 02 16:32:36 Finished compiler/bootstrap/compilation/ag32/32/proofs        24m11s  51GB
Aug 02 16:32:36 SUCCESS