Job 403

CakeML:bbffbd53135d21d194e39e8ddfb3192a64b5013a
  Update translator for new length check [Aug 06 10:25:49]
#508 (topic/pmatch-length)
Merging into:a5d4955acaa92d5009b6e204828a2d73467eb540
  Add various theorems [Aug 02 14:15:10]
HOL:2abaf720bc88c75a793eac0e280e392479d1745e
  Let ANSI colouring happen on screen terminals [Aug 02 11:53:04]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Aug 06 11:38:40 Claimed job
Aug 06 11:38:45 Building HOL
Aug 06 11:45:57 Starting developers/bin
Aug 06 11:46:01 Finished developers/bin                                           3s 217MB
Aug 06 11:46:02 Starting semantics/ffi
Aug 06 11:46:37 Finished semantics/ffi                                           33s 356MB
Aug 06 11:46:37 Starting semantics
Aug 06 11:47:56 Finished semantics                                             1m17s 962MB
Aug 06 11:47:57 Starting semantics/proofs
Aug 06 11:50:36 Finished semantics/proofs                                      2m39s   1GB
Aug 06 11:50:37 Starting basis/pure
Aug 06 11:54:04 Finished basis/pure                                            3m26s 784MB
Aug 06 11:54:05 Starting translator
Aug 06 11:55:37 Finished translator                                            1m31s 880MB
Aug 06 11:55:38 Starting compiler/parsing
Aug 06 11:57:11 Finished compiler/parsing                                      1m32s   2GB
Aug 06 11:57:12 Starting characteristic
Aug 06 11:59:32 Finished characteristic                                        2m18s   1GB
Aug 06 11:59:32 Starting translator/monadic
Aug 06 12:00:56 Finished translator/monadic                                    1m22s   1GB
Aug 06 12:00:57 Starting basis
Aug 06 12:16:37 Finished basis                                                15m40s   3GB
Aug 06 12:16:38 Starting compiler/inference
Aug 06 12:17:59 Finished compiler/inference                                    1m19s   1GB
Aug 06 12:17:59 Starting compiler/backend/reg_alloc
Aug 06 12:18:31 Finished compiler/backend/reg_alloc                              31s 923MB
Aug 06 12:18:32 Starting compiler/backend/gc
Aug 06 12:27:14 Finished compiler/backend/gc                                   8m41s   2GB
Aug 06 12:27:15 Starting compiler/backend
Aug 06 12:27:18 Finished compiler/backend                                         2s  17MB
Aug 06 12:27:19 Starting compiler/encoders/asm
Aug 06 12:27:20 Finished compiler/encoders/asm                                    0s  16MB
Aug 06 12:27:21 Starting compiler/encoders/x64
Aug 06 12:28:10 Finished compiler/encoders/x64                                   48s 595MB
Aug 06 12:28:10 Starting compiler/encoders/arm6
Aug 06 12:29:52 Finished compiler/encoders/arm6                                1m40s   1GB
Aug 06 12:29:53 Starting compiler/encoders/arm8
Aug 06 12:30:16 Finished compiler/encoders/arm8                                  22s 400MB
Aug 06 12:30:17 Starting compiler/encoders/mips
Aug 06 12:31:12 Finished compiler/encoders/mips                                  54s 867MB
Aug 06 12:31:13 Starting compiler/encoders/riscv
Aug 06 12:32:12 Finished compiler/encoders/riscv                                 58s 867MB
Aug 06 12:32:13 Starting compiler/backend/x64
Aug 06 12:32:31 Finished compiler/backend/x64                                    17s   1GB
Aug 06 12:32:31 Starting compiler/backend/arm6
Aug 06 12:32:52 Finished compiler/backend/arm6                                   19s   1GB
Aug 06 12:32:52 Starting compiler/backend/arm8
Aug 06 12:33:11 Finished compiler/backend/arm8                                   17s   1GB
Aug 06 12:33:12 Starting compiler/backend/mips
Aug 06 12:33:29 Finished compiler/backend/mips                                   16s 990MB
Aug 06 12:33:30 Starting compiler/backend/riscv
Aug 06 12:33:48 Finished compiler/backend/riscv                                  17s   1GB
Aug 06 12:33:49 Starting compiler/parsing/proofs
Aug 06 12:39:56 Finished compiler/parsing/proofs                               6m06s 817MB
Aug 06 12:39:57 Starting compiler/inference/proofs
Aug 06 12:42:20 Finished compiler/inference/proofs                             2m23s   1GB
Aug 06 12:42:21 Starting compiler/backend/semantics
Aug 06 12:51:13 Finished compiler/backend/semantics                            8m51s   2GB
Aug 06 12:51:14 Starting compiler/backend/reg_alloc/proofs
Aug 06 12:52:01 Finished compiler/backend/reg_alloc/proofs                       46s 587MB
Aug 06 12:52:01 Starting compiler/backend/proofs
Aug 06 13:27:33 Finished compiler/backend/proofs                              35m30s   3GB
Aug 06 13:27:34 Starting compiler/encoders/x64/proofs
Aug 06 15:12:53 Resuming compiler/encoders/x64/proofs
Aug 06 15:19:01 Finished compiler/encoders/x64/proofs                          6m07s   1GB
Aug 06 15:19:02 Starting compiler/encoders/arm6/proofs
Aug 06 15:26:27 Finished compiler/encoders/arm6/proofs                         7m24s   3GB
Aug 06 15:26:28 Starting compiler/encoders/arm8/proofs
Aug 06 15:31:43 Finished compiler/encoders/arm8/proofs                         5m14s   1GB
Aug 06 15:31:44 Starting compiler/encoders/mips/proofs
Aug 06 15:39:07 Finished compiler/encoders/mips/proofs                         7m22s   2GB
Aug 06 15:39:07 Starting compiler/encoders/riscv/proofs
Aug 06 15:47:05 Finished compiler/encoders/riscv/proofs                        7m57s 833MB
Aug 06 15:47:06 Starting compiler/backend/x64/proofs
Aug 06 15:47:25 Finished compiler/backend/x64/proofs                             18s   1GB
Aug 06 15:47:26 Starting compiler/backend/arm6/proofs
Aug 06 15:47:48 Finished compiler/backend/arm6/proofs                            21s 835MB
Aug 06 15:47:48 Starting compiler/backend/arm8/proofs
Aug 06 15:48:07 Finished compiler/backend/arm8/proofs                            18s 758MB
Aug 06 15:48:08 Starting compiler/backend/mips/proofs
Aug 06 15:48:29 Finished compiler/backend/mips/proofs                            20s   1GB
Aug 06 15:48:30 Starting compiler/backend/riscv/proofs
Aug 06 15:48:49 Finished compiler/backend/riscv/proofs                           18s   1GB
Aug 06 15:48:50 Starting compiler/proofs
Aug 06 15:50:03 Finished compiler/proofs                                       1m12s   2GB
Aug 06 15:50:04 Starting candle/set-theory
Aug 06 15:50:32 Finished candle/set-theory                                       27s 600MB
Aug 06 15:50:32 Starting candle/syntax-lib
Aug 06 15:50:42 Finished candle/syntax-lib                                        9s 571MB
Aug 06 15:50:43 Starting candle/standard/syntax
Aug 06 15:52:13 Finished candle/standard/syntax                                1m29s 627MB
Aug 06 15:52:14 Starting candle/standard/semantics
Aug 06 15:53:34 Finished candle/standard/semantics                             1m19s 870MB
Aug 06 15:53:35 Starting candle/standard/monadic
Aug 06 15:54:59 Finished candle/standard/monadic                               1m23s 750MB
Aug 06 15:55:00 Starting candle/standard/ml_kernel
Aug 06 15:58:29 Finished candle/standard/ml_kernel                             3m28s   2GB
Aug 06 15:58:30 Starting candle/standard/opentheory
Aug 06 15:58:44 Finished candle/standard/opentheory                              13s 648MB
Aug 06 15:58:45 Starting characteristic/examples
Aug 06 16:00:15 Finished characteristic/examples                               1m29s   2GB
Aug 06 16:00:16 Starting tutorial/solutions
Aug 06 16:13:47 Finished tutorial/solutions                                   13m29s   7GB
Aug 06 16:13:47 Starting translator/monadic/examples
Aug 06 16:15:31 Finished translator/monadic/examples                           1m43s   2GB
Aug 06 16:15:32 Starting examples
Aug 06 16:21:03 Finished examples                                              5m29s   6GB
Aug 06 16:21:03 Starting examples/compilation
Aug 06 18:15:48 Finished examples/compilation                               1h54m44s  11GB
Aug 06 18:15:49 Starting examples/compilation/proofs
Aug 06 18:17:37 Finished examples/compilation/proofs                           1m47s   3GB
Aug 06 18:17:37 Starting compiler/benchmarks
Aug 06 18:17:38 Finished compiler/benchmarks                                      0s   4MB
Aug 06 18:17:39 Starting translator/okasaki-examples
Aug 06 18:21:13 Finished translator/okasaki-examples                           3m33s   1GB
Aug 06 18:21:13 Starting translator/other-examples
Aug 06 18:24:33 Finished translator/other-examples                             3m19s   1GB
Aug 06 18:24:34 Starting compiler/parsing/tests
Aug 06 18:24:58 Finished compiler/parsing/tests                                  23s 327MB
Aug 06 18:24:59 Starting compiler/inference/tests
Aug 06 18:29:07 Finished compiler/inference/tests                              4m06s   3GB
Aug 06 18:29:07 Starting compiler/bootstrap/translation
Aug 07 01:22:39 Finished compiler/bootstrap/translation                     6h53m31s  46GB
Aug 07 01:22:40 Starting unverified/sexpr-bootstrap/x64/64
Aug 07 01:25:36 Finished unverified/sexpr-bootstrap/x64/64                     2m55s  15GB
Aug 07 01:25:37 Starting unverified/sexpr-bootstrap/x64/32
Aug 07 01:28:05 Finished unverified/sexpr-bootstrap/x64/32                     2m27s  14GB
Aug 07 01:28:05 Starting compiler/bootstrap/compilation/x64/64 Aug 07 01:28:05 2643s