Job 700

CakeML:e0da950aff3cf0a203cd67071cad70e76e811c03
  Tweak benchmark Holmakefiles [Jan 24 20:48:33]
#610 (build-benchmarks)
Merging into:0f7cba8a996ac4784f5803db18f77a42edbea8ea
  Merge pull request #609 from CakeML/cf-div-io [Jan 25 07:53:49]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 25 09:03:00 Claimed job
Jan 25 09:03:07 Reusing HOL
Jan 25 09:03:18 Starting developers
Jan 25 09:03:19 Finished developers                                               0s  21MB
Jan 25 09:03:20 Starting developers/bin
Jan 25 09:03:53 Finished developers/bin                                          32s 142MB
Jan 25 09:03:54 Starting semantics/ffi
Jan 25 09:04:02 Finished semantics/ffi                                            7s 227MB
Jan 25 09:04:03 Starting semantics
Jan 25 09:05:23 Finished semantics                                             1m19s   1GB
Jan 25 09:05:24 Starting semantics/proofs
Jan 25 09:08:42 Finished semantics/proofs                                      3m17s   1GB
Jan 25 09:08:43 Starting basis/pure
Jan 25 09:09:29 Finished basis/pure                                              45s 749MB
Jan 25 09:09:30 Starting translator
Jan 25 09:11:08 Finished translator                                            1m36s   1GB
Jan 25 09:11:08 Starting compiler/parsing
Jan 25 09:12:12 Finished compiler/parsing                                      1m02s   2GB
Jan 25 09:12:13 Starting characteristic
Jan 25 09:16:36 Finished characteristic                                        4m22s   1GB
Jan 25 09:16:37 Starting translator/monadic
Jan 25 09:18:04 Finished translator/monadic                                    1m26s   1GB
Jan 25 09:18:05 Starting basis
Jan 25 09:35:04 Finished basis                                                16m58s   2GB
Jan 25 09:35:05 Starting compiler/inference
Jan 25 09:36:43 Finished compiler/inference                                    1m38s   1GB
Jan 25 09:36:44 Starting compiler/backend/reg_alloc
Jan 25 09:37:36 Finished compiler/backend/reg_alloc                              50s   1GB
Jan 25 09:37:37 Starting compiler/backend/gc
Jan 25 09:45:24 Finished compiler/backend/gc                                   7m46s   1GB
Jan 25 09:45:25 Starting compiler/backend
Jan 25 09:45:27 Finished compiler/backend                                         1s  17MB
Jan 25 09:45:28 Starting compiler/encoders/asm
Jan 25 09:45:30 Finished compiler/encoders/asm                                    0s  16MB
Jan 25 09:45:31 Starting compiler/encoders/x64
Jan 25 09:45:56 Finished compiler/encoders/x64                                   24s 830MB
Jan 25 09:45:57 Starting compiler/encoders/arm6
Jan 25 09:46:48 Finished compiler/encoders/arm6                                  50s 991MB
Jan 25 09:46:49 Starting compiler/encoders/arm8
Jan 25 09:47:02 Finished compiler/encoders/arm8                                  12s 875MB
Jan 25 09:47:02 Starting compiler/encoders/mips
Jan 25 09:47:19 Finished compiler/encoders/mips                                  16s   1GB
Jan 25 09:47:20 Starting compiler/encoders/riscv
Jan 25 09:47:34 Finished compiler/encoders/riscv                                 13s 746MB
Jan 25 09:47:35 Starting compiler/encoders/ag32
Jan 25 09:47:52 Finished compiler/encoders/ag32                                  15s 776MB
Jan 25 09:47:52 Starting compiler/backend/x64
Jan 25 09:48:10 Finished compiler/backend/x64                                    16s 809MB
Jan 25 09:48:10 Starting compiler/backend/arm6
Jan 25 09:48:29 Finished compiler/backend/arm6                                   17s   1GB
Jan 25 09:48:30 Starting compiler/backend/arm8
Jan 25 09:48:49 Finished compiler/backend/arm8                                   18s 997MB
Jan 25 09:48:49 Starting compiler/backend/mips
Jan 25 09:49:08 Finished compiler/backend/mips                                   18s   1GB
Jan 25 09:49:09 Starting compiler/backend/riscv
Jan 25 09:49:26 Finished compiler/backend/riscv                                  16s 938MB
Jan 25 09:49:27 Starting compiler/backend/ag32
Jan 25 09:50:39 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 25 09:50:40 Starting compiler/parsing/proofs
Jan 25 09:56:31 Finished compiler/parsing/proofs                               5m50s 859MB
Jan 25 09:56:32 Starting compiler/inference/proofs
Jan 25 09:59:27 Finished compiler/inference/proofs                             2m54s   1GB
Jan 25 09:59:28 Starting compiler/backend/semantics
Jan 25 10:06:57 Finished compiler/backend/semantics                            7m28s   2GB
Jan 25 10:06:58 Starting compiler/backend/reg_alloc/proofs
Jan 25 10:09:44 Finished compiler/backend/reg_alloc/proofs                     2m45s 799MB
Jan 25 10:09:45 Starting compiler/backend/proofs
Jan 25 10:48:35 Finished compiler/backend/proofs                              38m48s   3GB
Jan 25 10:48:35 Starting compiler/encoders/x64/proofs
Jan 25 10:58:27 Finished compiler/encoders/x64/proofs                          9m50s   7GB
Jan 25 10:58:28 Starting compiler/encoders/arm6/proofs
Jan 25 11:12:34 Finished compiler/encoders/arm6/proofs                        14m05s   3GB
Jan 25 11:12:35 Starting compiler/encoders/arm8/proofs
Jan 25 11:18:37 Finished compiler/encoders/arm8/proofs                         6m00s   1GB
Jan 25 11:18:38 Starting compiler/encoders/mips/proofs
Jan 25 11:29:20 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Jan 25 11:29:20 Starting compiler/encoders/riscv/proofs
Jan 25 11:37:18 Finished compiler/encoders/riscv/proofs                        7m56s 973MB
Jan 25 11:37:18 Starting compiler/encoders/ag32/proofs
Jan 25 11:40:01 Finished compiler/encoders/ag32/proofs                         2m41s 889MB
Jan 25 11:40:02 Starting compiler/backend/x64/proofs
Jan 25 11:40:21 Finished compiler/backend/x64/proofs                             17s 781MB
Jan 25 11:40:21 Starting compiler/backend/arm6/proofs
Jan 25 11:40:42 Finished compiler/backend/arm6/proofs                            19s   1GB
Jan 25 11:40:43 Starting compiler/backend/arm8/proofs
Jan 25 11:41:03 Finished compiler/backend/arm8/proofs                            19s 741MB
Jan 25 11:41:04 Starting compiler/backend/mips/proofs
Jan 25 11:41:24 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 25 11:41:25 Starting compiler/backend/riscv/proofs
Jan 25 11:41:45 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 25 11:41:45 Starting compiler/backend/ag32/proofs
Jan 25 11:51:15 Finished compiler/backend/ag32/proofs                          9m28s   3GB
Jan 25 11:51:16 Starting compiler/proofs
Jan 25 11:52:38 Finished compiler/proofs                                       1m21s   3GB
Jan 25 11:52:39 Starting candle/set-theory
Jan 25 11:53:05 Finished candle/set-theory                                       25s 654MB
Jan 25 11:53:06 Starting candle/syntax-lib
Jan 25 11:53:17 Finished candle/syntax-lib                                       10s 503MB
Jan 25 11:53:17 Starting candle/standard/syntax
Jan 25 11:55:07 Finished candle/standard/syntax                                1m48s   1GB
Jan 25 11:55:07 Starting candle/standard/semantics
Jan 25 11:56:46 Finished candle/standard/semantics                             1m37s   1GB
Jan 25 11:56:47 Starting candle/standard/monadic
Jan 25 11:58:32 Finished candle/standard/monadic                               1m43s   1GB
Jan 25 11:58:32 Starting candle/standard/ml_kernel
Jan 25 12:02:29 Finished candle/standard/ml_kernel                             3m55s   3GB
Jan 25 12:02:30 Starting candle/standard/opentheory
Jan 25 12:11:18 Finished candle/standard/opentheory                            8m47s   4GB
Jan 25 12:11:19 Starting candle/standard/opentheory/compilation
Jan 25 12:40:45 Finished candle/standard/opentheory/compilation               29m24s  15GB
Jan 25 12:40:46 Starting candle/standard/opentheory/compilation/proofs
Jan 25 12:41:32 Finished candle/standard/opentheory/compilation/proofs           45s   5GB
Jan 25 12:41:33 Starting characteristic/examples
Jan 25 12:43:01 Finished characteristic/examples                               1m27s   2GB
Jan 25 12:43:02 Starting tutorial/solutions
Jan 25 12:56:02 Finished tutorial/solutions                                   12m59s   6GB
Jan 25 12:56:03 Starting translator/monadic/examples
Jan 25 12:58:16 Finished translator/monadic/examples                           2m12s   3GB
Jan 25 12:58:16 Starting examples
Jan 25 13:06:16 Finished examples                                              7m58s   4GB
Jan 25 13:06:17 Starting examples/compilation/x64
Jan 25 14:58:24 Finished examples/compilation/x64                           1h52m05s  12GB
Jan 25 14:58:24 Starting examples/compilation/x64/proofs
Jan 25 15:00:11 Finished examples/compilation/x64/proofs                       1m45s   5GB
Jan 25 15:00:11 Starting examples/compilation/ag32
Jan 25 15:27:51 Finished examples/compilation/ag32                            27m38s   6GB
Jan 25 15:27:51 Starting examples/compilation/ag32/proofs
Jan 25 15:28:38 Finished examples/compilation/ag32/proofs                        45s   4GB
Jan 25 15:28:39 Starting translator/okasaki-examples
Jan 25 15:32:52 Finished translator/okasaki-examples                           4m12s   1GB
Jan 25 15:32:52 Starting translator/other-examples
Jan 25 15:33:33 Finished translator/other-examples                               40s   1GB
Jan 25 15:33:34 Starting compiler/parsing/tests
Jan 25 15:33:59 Finished compiler/parsing/tests                                  24s 545MB
Jan 25 15:34:00 Starting compiler/inference/tests
Jan 25 15:38:06 Finished compiler/inference/tests                              4m05s   5GB
Jan 25 15:38:07 Starting compiler/bootstrap/translation
Jan 25 18:11:25 Finished compiler/bootstrap/translation                     2h33m16s  45GB
Jan 25 18:11:26 Starting unverified/sexpr-bootstrap/x64/64
Jan 25 18:20:10 Finished unverified/sexpr-bootstrap/x64/64                     8m43s  16GB
Jan 25 18:20:11 Starting unverified/sexpr-bootstrap/x64/32
Jan 25 18:25:28 Finished unverified/sexpr-bootstrap/x64/32                     5m16s  19GB
Jan 25 18:25:29 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Jan 25 18:26:00 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            30s   1GB
Jan 25 18:26:01 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Jan 25 18:26:48 Finished compiler/benchmarks/mlton_benchmarks/cakeml             46s   1GB
Jan 25 18:26:49 Starting compiler/bootstrap/compilation/x64/64
Jan 26 04:38:53 Finished compiler/bootstrap/compilation/x64/64             10h12m03s  64GB
Jan 26 04:38:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 26 04:45:15 Finished compiler/bootstrap/compilation/x64/64/proofs          6m20s  31GB
Jan 26 04:45:16 Starting compiler/bootstrap/compilation/x64/32
Jan 26 13:52:32 Finished compiler/bootstrap/compilation/x64/32              9h07m15s  64GB
Jan 26 13:52:33 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 26 13:58:15 Finished compiler/bootstrap/compilation/x64/32/proofs          5m40s  28GB
Jan 26 13:58:16 SUCCESS