Job 1044

CakeML:880f818f08f12d69b750c9a9b81af72b37d64d92
  adjust to changes in regexpLib [Sep 28 01:50:23]
#691 (regexp_delta)
Merging into:30193e4df86fc6ee1df59c8baf4b125c84ba01d4
  Merge pull request #690 from CakeML/close-files [Sep 13 07:50:45]
HOL:fdba23b05ca01a36aa6d330d2adeb55601b76924
  Optimization of proof-based regexp compiler [Sep 27 22:31:07]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Oct 01 05:25:03 Claimed job
Oct 01 05:25:10 Building HOL
Oct 01 05:34:17 Starting developers
Oct 01 05:34:18 Finished developers                                               0s  21MB
Oct 01 05:34:18 Starting developers/bin
Oct 01 05:34:22 Finished developers/bin                                           3s 238MB
Oct 01 05:34:22 Starting semantics/ffi
Oct 01 05:34:55 Finished semantics/ffi                                           33s 473MB
Oct 01 05:34:56 Starting semantics
Oct 01 05:36:25 Finished semantics                                             1m28s   1GB
Oct 01 05:36:25 Starting semantics/proofs
Oct 01 05:39:16 Finished semantics/proofs                                      2m51s   1GB
Oct 01 05:39:17 Starting semantics/alt_semantics
Oct 01 05:39:23 Finished semantics/alt_semantics                                  5s 267MB
Oct 01 05:39:23 Starting semantics/alt_semantics/proofs
Oct 01 05:41:09 Finished semantics/alt_semantics/proofs                        1m45s 785MB
Oct 01 05:41:09 Starting basis/pure
Oct 01 05:44:56 Finished basis/pure                                            3m47s 690MB
Oct 01 05:44:57 Starting translator
Oct 01 05:46:41 Finished translator                                            1m44s   1GB
Oct 01 05:46:42 Starting compiler/parsing
Oct 01 05:47:39 Finished compiler/parsing                                        57s   2GB
Oct 01 05:47:39 Starting characteristic
Oct 01 05:52:50 Finished characteristic                                        5m09s   1GB
Oct 01 05:52:50 Starting translator/monadic
Oct 01 05:54:16 Finished translator/monadic                                    1m25s   1GB
Oct 01 05:54:16 Starting basis
Oct 01 06:13:37 Finished basis                                                19m20s   2GB
Oct 01 06:13:37 Starting compiler/inference
Oct 01 06:15:27 Finished compiler/inference                                    1m49s   1GB
Oct 01 06:15:28 Starting compiler/backend/reg_alloc
Oct 01 06:16:26 Finished compiler/backend/reg_alloc                              58s   1GB
Oct 01 06:16:26 Starting compiler/backend/gc
Oct 01 06:25:26 Finished compiler/backend/gc                                   8m58s   1GB
Oct 01 06:25:26 Starting compiler/backend
Oct 01 06:25:27 Finished compiler/backend                                         0s  45MB
Oct 01 06:25:27 Starting compiler/encoders/asm
Oct 01 19:12:39 Resuming compiler/encoders/asm
Oct 01 19:12:39 Finished compiler/encoders/asm                                    0s  35MB
Oct 01 19:12:39 Starting compiler/encoders/x64
Oct 01 19:13:35 Finished compiler/encoders/x64                                   55s 888MB
Oct 01 19:13:36 Starting compiler/encoders/arm7
Oct 01 19:15:16 Finished compiler/encoders/arm7                                1m39s   1GB
Oct 01 19:15:16 Starting compiler/encoders/arm8
Oct 01 19:15:47 Finished compiler/encoders/arm8                                  30s 565MB
Oct 01 19:15:48 Starting compiler/encoders/mips
Oct 01 19:17:03 Finished compiler/encoders/mips                                1m15s   1GB
Oct 01 19:17:03 Starting compiler/encoders/riscv
Oct 01 19:18:35 Finished compiler/encoders/riscv                               1m31s   1GB
Oct 01 19:18:35 Starting compiler/encoders/ag32
Oct 01 19:18:52 Finished compiler/encoders/ag32                                  16s 682MB
Oct 01 19:18:52 Starting compiler/backend/x64
Oct 01 19:19:09 Finished compiler/backend/x64                                    17s   1GB
Oct 01 19:19:09 Starting compiler/backend/arm7
Oct 01 19:19:28 Finished compiler/backend/arm7                                   18s   1GB
Oct 01 19:19:28 Starting compiler/backend/arm8
Oct 01 19:19:46 Finished compiler/backend/arm8                                   17s   1GB
Oct 01 19:19:46 Starting compiler/backend/mips
Oct 01 19:20:04 Finished compiler/backend/mips                                   17s 992MB
Oct 01 19:20:04 Starting compiler/backend/riscv
Oct 01 19:20:22 Finished compiler/backend/riscv                                  17s   1GB
Oct 01 19:20:22 Starting compiler/backend/ag32
Oct 01 19:21:31 Finished compiler/backend/ag32                                 1m08s 984MB
Oct 01 19:21:31 Starting compiler/parsing/proofs
Oct 01 19:27:17 Finished compiler/parsing/proofs                               5m45s 922MB
Oct 01 19:27:17 Starting compiler/inference/proofs
Oct 01 19:30:15 Finished compiler/inference/proofs                             2m57s 895MB
Oct 01 19:30:15 Starting compiler/backend/semantics
Oct 01 19:37:13 Finished compiler/backend/semantics                            6m57s   2GB
Oct 01 19:37:13 Starting compiler/backend/reg_alloc/proofs
Oct 01 19:40:39 Finished compiler/backend/reg_alloc/proofs                     3m25s 999MB
Oct 01 19:40:40 Starting compiler/backend/proofs
Oct 01 20:28:09 Finished compiler/backend/proofs                              47m28s   4GB
Oct 01 20:28:09 Starting compiler/encoders/x64/proofs
Oct 01 20:38:16 Finished compiler/encoders/x64/proofs                         10m06s   4GB
Oct 01 20:38:16 Starting compiler/encoders/arm7/proofs
Oct 01 20:51:53 Finished compiler/encoders/arm7/proofs                        13m36s   3GB
Oct 01 20:51:53 Starting compiler/encoders/arm8/proofs
Oct 01 20:58:36 Finished compiler/encoders/arm8/proofs                         6m42s   1GB
Oct 01 20:58:37 Starting compiler/encoders/mips/proofs
Oct 01 21:08:29 Finished compiler/encoders/mips/proofs                         9m51s   3GB
Oct 01 21:08:29 Starting compiler/encoders/riscv/proofs
Oct 01 21:16:52 Finished compiler/encoders/riscv/proofs                        8m22s   1GB
Oct 01 21:16:53 Starting compiler/encoders/ag32/proofs
Oct 01 21:19:19 Finished compiler/encoders/ag32/proofs                         2m26s 703MB
Oct 01 21:19:20 Starting compiler/backend/x64/proofs
Oct 01 21:19:37 Finished compiler/backend/x64/proofs                             17s   1GB
Oct 01 21:19:37 Starting compiler/backend/arm7/proofs
Oct 01 21:19:55 Finished compiler/backend/arm7/proofs                            17s   1GB
Oct 01 21:19:55 Starting compiler/backend/arm8/proofs
Oct 01 21:20:11 Finished compiler/backend/arm8/proofs                            15s 754MB
Oct 01 21:20:12 Starting compiler/backend/mips/proofs
Oct 01 21:20:29 Finished compiler/backend/mips/proofs                            17s   1GB
Oct 01 21:20:29 Starting compiler/backend/riscv/proofs
Oct 01 21:20:47 Finished compiler/backend/riscv/proofs                           17s   1GB
Oct 01 21:20:47 Starting compiler/backend/ag32/proofs
Oct 01 21:29:38 Finished compiler/backend/ag32/proofs                          8m50s   2GB
Oct 01 21:29:38 Starting compiler/proofs
Oct 01 21:30:51 Finished compiler/proofs                                       1m12s   3GB
Oct 01 21:30:51 Starting candle/set-theory
Oct 01 21:31:17 Finished candle/set-theory                                       25s 710MB
Oct 01 21:31:17 Starting candle/syntax-lib
Oct 01 21:31:27 Finished candle/syntax-lib                                        9s 478MB
Oct 01 21:31:27 Starting candle/standard/syntax
Oct 01 21:33:08 Finished candle/standard/syntax                                1m40s   1GB
Oct 01 21:33:08 Starting candle/standard/semantics
Oct 01 21:34:41 Finished candle/standard/semantics                             1m32s 940MB
Oct 01 21:34:41 Starting candle/standard/monadic
Oct 01 21:36:12 Finished candle/standard/monadic                               1m31s   1GB
Oct 01 21:36:13 Starting candle/standard/ml_kernel
Oct 01 21:39:59 Finished candle/standard/ml_kernel                             3m45s   5GB
Oct 01 21:39:59 Starting candle/standard/opentheory
Oct 01 21:48:31 Finished candle/standard/opentheory                            8m31s   3GB
Oct 01 21:48:31 Starting candle/standard/opentheory/compilation
Oct 01 22:19:29 Finished candle/standard/opentheory/compilation               30m57s  15GB
Oct 01 22:19:29 Starting candle/standard/opentheory/compilation/proofs
Oct 01 22:20:11 Finished candle/standard/opentheory/compilation/proofs           41s   2GB
Oct 01 22:20:11 Starting characteristic/examples
Oct 01 22:21:35 Finished characteristic/examples                               1m24s   2GB
Oct 01 22:21:35 Starting tutorial/solutions
Oct 01 22:34:46 Finished tutorial/solutions                                   13m09s   7GB
Oct 01 22:34:46 Starting translator/monadic/examples
Oct 01 22:37:36 Finished translator/monadic/examples                           2m50s   1GB
Oct 01 22:37:37 Starting examples
Oct 01 22:46:33 Finished examples                                              8m56s   4GB
Oct 01 22:46:34 Starting examples/compilation/x64
Oct 02 00:48:46 Finished examples/compilation/x64                           2h02m11s  12GB
Oct 02 00:48:46 Starting examples/compilation/x64/proofs
Oct 02 00:50:13 Finished examples/compilation/x64/proofs                       1m27s   2GB
Oct 02 00:50:14 Starting examples/compilation/ag32
Oct 02 01:18:36 Finished examples/compilation/ag32                            28m22s   5GB
Oct 02 01:18:36 Starting examples/compilation/ag32/proofs
Oct 02 01:19:21 Finished examples/compilation/ag32/proofs                        44s   3GB
Oct 02 01:19:22 Starting translator/okasaki-examples
Oct 02 01:23:23 Finished translator/okasaki-examples                           4m00s   1GB
Oct 02 01:23:23 Starting translator/other-examples
Oct 02 01:26:43 Finished translator/other-examples                             3m19s   1GB
Oct 02 01:26:44 Starting compiler/parsing/tests
Oct 02 01:27:09 Finished compiler/parsing/tests                                  24s 543MB
Oct 02 01:27:09 Starting compiler/inference/tests
Oct 02 01:31:24 Finished compiler/inference/tests                              4m15s   4GB
Oct 02 01:31:25 Starting compiler/bootstrap/translation
Oct 02 04:00:49 Finished compiler/bootstrap/translation                     2h29m23s  44GB
Oct 02 04:00:49 Starting unverified/sexpr-bootstrap/x64/64
Oct 02 04:13:49 Finished unverified/sexpr-bootstrap/x64/64                    13m00s   2GB
Oct 02 04:13:49 Starting unverified/sexpr-bootstrap/x64/32
Oct 02 04:23:12 Finished unverified/sexpr-bootstrap/x64/32                     9m22s   6GB
Oct 02 04:23:13 Starting compiler/benchmarks
Oct 02 05:01:19 Finished compiler/benchmarks                                  38m06s   2GB
Oct 02 05:01:20 Starting compiler/bootstrap/compilation/x64/64
Oct 02 18:39:59 Finished compiler/bootstrap/compilation/x64/64             13h38m38s  63GB
Oct 02 18:40:00 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 02 18:43:31 Finished compiler/bootstrap/compilation/x64/64/proofs          3m30s   5GB
Oct 02 18:43:31 Starting compiler/bootstrap/compilation/x64/32
Oct 03 06:32:18 Finished compiler/bootstrap/compilation/x64/32             11h48m46s  64GB
Oct 03 06:32:18 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 03 06:34:47 Finished compiler/bootstrap/compilation/x64/32/proofs          2m28s   9GB
Oct 03 06:34:48 Starting compiler/bootstrap/compilation/ag32/32
Oct 03 19:55:59 Finished compiler/bootstrap/compilation/ag32/32            13h21m11s  64GB
Oct 03 19:56:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 03 20:25:37 Finished compiler/bootstrap/compilation/ag32/32/proofs        29m37s  17GB
Oct 03 20:25:38 SUCCESS