Job 702

CakeML:a8381c3cc50bed5d12b330b985c3f4fdc53405e9
  Merge pull request #610 from CakeML/build-benchmarks [Jan 26 15:05:54]
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
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 26 15:18:23 Claimed job
Jan 26 15:18:30 Reusing HOL
Jan 26 15:18:43 Starting developers
Jan 26 15:18:45 Finished developers                                               0s  25MB
Jan 26 15:18:45 Starting developers/bin
Jan 26 15:19:22 Finished developers/bin                                          36s 142MB
Jan 26 15:19:23 Starting semantics/ffi
Jan 26 15:19:32 Finished semantics/ffi                                            7s 210MB
Jan 26 15:19:32 Starting semantics
Jan 26 15:20:53 Finished semantics                                             1m19s   1GB
Jan 26 15:20:54 Starting semantics/proofs
Jan 26 15:24:09 Finished semantics/proofs                                      3m14s   1GB
Jan 26 15:24:10 Starting basis/pure
Jan 26 15:24:55 Finished basis/pure                                              44s 606MB
Jan 26 15:24:56 Starting translator
Jan 26 15:26:36 Finished translator                                            1m39s   1GB
Jan 26 15:26:37 Starting compiler/parsing
Jan 26 15:27:40 Finished compiler/parsing                                      1m02s   2GB
Jan 26 15:27:41 Starting characteristic
Jan 26 15:32:02 Finished characteristic                                        4m19s   1GB
Jan 26 15:32:02 Starting translator/monadic
Jan 26 15:33:29 Finished translator/monadic                                    1m25s   1GB
Jan 26 15:33:29 Starting basis
Jan 26 15:50:28 Finished basis                                                16m57s   3GB
Jan 26 15:50:29 Starting compiler/inference
Jan 26 15:52:06 Finished compiler/inference                                    1m36s   1GB
Jan 26 15:52:07 Starting compiler/backend/reg_alloc
Jan 26 15:52:58 Finished compiler/backend/reg_alloc                              49s   1GB
Jan 26 15:52:59 Starting compiler/backend/gc
Jan 26 16:00:48 Finished compiler/backend/gc                                   7m48s   2GB
Jan 26 16:00:48 Starting compiler/backend
Jan 26 16:00:51 Finished compiler/backend                                         1s  23MB
Jan 26 16:00:51 Starting compiler/encoders/asm
Jan 26 16:00:53 Finished compiler/encoders/asm                                    0s  16MB
Jan 26 16:00:54 Starting compiler/encoders/x64
Jan 26 16:01:18 Finished compiler/encoders/x64                                   23s 924MB
Jan 26 16:01:19 Starting compiler/encoders/arm6
Jan 26 16:02:10 Finished compiler/encoders/arm6                                  50s   1GB
Jan 26 16:02:11 Starting compiler/encoders/arm8
Jan 26 16:02:24 Finished compiler/encoders/arm8                                  12s 847MB
Jan 26 16:02:25 Starting compiler/encoders/mips
Jan 26 16:02:42 Finished compiler/encoders/mips                                  16s   1GB
Jan 26 16:02:43 Starting compiler/encoders/riscv
Jan 26 16:02:57 Finished compiler/encoders/riscv                                 13s 865MB
Jan 26 16:02:58 Starting compiler/encoders/ag32
Jan 26 16:03:14 Finished compiler/encoders/ag32                                  15s 807MB
Jan 26 16:03:15 Starting compiler/backend/x64
Jan 26 16:03:32 Finished compiler/backend/x64                                    16s   1GB
Jan 26 16:03:33 Starting compiler/backend/arm6
Jan 26 16:03:53 Finished compiler/backend/arm6                                   18s   1GB
Jan 26 16:03:53 Starting compiler/backend/arm8
Jan 26 16:04:12 Finished compiler/backend/arm8                                   17s 897MB
Jan 26 16:04:13 Starting compiler/backend/mips
Jan 26 16:04:32 Finished compiler/backend/mips                                   18s   1GB
Jan 26 16:04:32 Starting compiler/backend/riscv
Jan 26 16:04:50 Finished compiler/backend/riscv                                  16s   1GB
Jan 26 16:04:50 Starting compiler/backend/ag32
Jan 26 16:06:03 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 26 16:06:04 Starting compiler/parsing/proofs
Jan 26 16:11:54 Finished compiler/parsing/proofs                               5m48s 850MB
Jan 26 16:11:54 Starting compiler/inference/proofs
Jan 26 16:14:49 Finished compiler/inference/proofs                             2m53s   1GB
Jan 26 16:14:50 Starting compiler/backend/semantics
Jan 26 16:22:27 Finished compiler/backend/semantics                            7m36s   1GB
Jan 26 16:22:28 Starting compiler/backend/reg_alloc/proofs
Jan 26 16:25:13 Finished compiler/backend/reg_alloc/proofs                     2m44s   1GB
Jan 26 16:25:14 Starting compiler/backend/proofs
Jan 26 17:04:28 Finished compiler/backend/proofs                              39m12s   3GB
Jan 26 17:04:29 Starting compiler/encoders/x64/proofs
Jan 26 17:14:24 Finished compiler/encoders/x64/proofs                          9m54s   5GB
Jan 26 17:14:25 Starting compiler/encoders/arm6/proofs
Jan 26 17:28:33 Finished compiler/encoders/arm6/proofs                        14m07s   3GB
Jan 26 17:28:34 Starting compiler/encoders/arm8/proofs
Jan 26 17:34:32 Finished compiler/encoders/arm8/proofs                         5m57s   1GB
Jan 26 17:34:33 Starting compiler/encoders/mips/proofs
Jan 26 17:45:09 Finished compiler/encoders/mips/proofs                        10m35s   2GB
Jan 26 17:45:10 Starting compiler/encoders/riscv/proofs
Jan 26 17:53:11 Finished compiler/encoders/riscv/proofs                        8m00s   1GB
Jan 26 17:53:12 Starting compiler/encoders/ag32/proofs
Jan 26 17:55:56 Finished compiler/encoders/ag32/proofs                         2m42s 888MB
Jan 26 17:55:56 Starting compiler/backend/x64/proofs
Jan 26 17:56:16 Finished compiler/backend/x64/proofs                             19s   1GB
Jan 26 17:56:17 Starting compiler/backend/arm6/proofs
Jan 26 17:56:38 Finished compiler/backend/arm6/proofs                            20s   1GB
Jan 26 17:56:39 Starting compiler/backend/arm8/proofs
Jan 26 17:56:57 Finished compiler/backend/arm8/proofs                            17s 889MB
Jan 26 17:56:58 Starting compiler/backend/mips/proofs
Jan 26 17:57:18 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 26 17:57:19 Starting compiler/backend/riscv/proofs
Jan 26 17:57:38 Finished compiler/backend/riscv/proofs                           18s   1GB
Jan 26 17:57:39 Starting compiler/backend/ag32/proofs
Jan 26 18:07:08 Finished compiler/backend/ag32/proofs                          9m27s   1GB
Jan 26 18:07:08 Starting compiler/proofs
Jan 26 18:08:29 Finished compiler/proofs                                       1m20s   3GB
Jan 26 18:08:30 Starting candle/set-theory
Jan 26 18:08:55 Finished candle/set-theory                                       24s 747MB
Jan 26 18:08:56 Starting candle/syntax-lib
Jan 26 18:09:06 Finished candle/syntax-lib                                        9s 673MB
Jan 26 18:09:07 Starting candle/standard/syntax
Jan 26 18:10:55 Finished candle/standard/syntax                                1m47s 896MB
Jan 26 18:10:56 Starting candle/standard/semantics
Jan 26 18:12:34 Finished candle/standard/semantics                             1m37s   1GB
Jan 26 18:12:35 Starting candle/standard/monadic
Jan 26 18:14:17 Finished candle/standard/monadic                               1m40s   1GB
Jan 26 18:14:18 Starting candle/standard/ml_kernel
Jan 26 18:18:24 Finished candle/standard/ml_kernel                             4m05s   6GB
Jan 26 18:18:25 Starting candle/standard/opentheory
Jan 26 18:27:19 Finished candle/standard/opentheory                            8m52s   5GB
Jan 26 18:27:20 Starting candle/standard/opentheory/compilation
Jan 26 18:56:38 Finished candle/standard/opentheory/compilation               29m17s  13GB
Jan 26 18:56:39 Starting candle/standard/opentheory/compilation/proofs
Jan 26 18:57:21 Finished candle/standard/opentheory/compilation/proofs           41s   4GB
Jan 26 18:57:21 Starting characteristic/examples
Jan 26 18:58:49 Finished characteristic/examples                               1m26s   3GB
Jan 26 18:58:49 Starting tutorial/solutions
Jan 26 19:12:03 Finished tutorial/solutions                                   13m12s   6GB
Jan 26 19:12:04 Starting translator/monadic/examples
Jan 26 19:14:16 Finished translator/monadic/examples                           2m11s   3GB
Jan 26 19:14:17 Starting examples
Jan 26 19:22:13 Finished examples                                              7m55s   4GB
Jan 26 19:22:14 Starting examples/compilation/x64
Jan 26 21:14:50 Finished examples/compilation/x64                           1h52m35s  17GB
Jan 26 21:14:51 Starting examples/compilation/x64/proofs
Jan 26 21:16:33 Finished examples/compilation/x64/proofs                       1m41s   4GB
Jan 26 21:16:34 Starting examples/compilation/ag32
Jan 26 21:44:18 Finished examples/compilation/ag32                            27m42s   6GB
Jan 26 21:44:18 Starting examples/compilation/ag32/proofs
Jan 26 21:45:06 Finished examples/compilation/ag32/proofs                        46s   4GB
Jan 26 21:45:07 Starting translator/okasaki-examples
Jan 26 21:49:17 Finished translator/okasaki-examples                           4m08s   2GB
Jan 26 21:49:17 Starting translator/other-examples
Jan 26 21:49:58 Finished translator/other-examples                               39s   1GB
Jan 26 21:49:59 Starting compiler/parsing/tests
Jan 26 21:50:25 Finished compiler/parsing/tests                                  25s 648MB
Jan 26 21:50:25 Starting compiler/inference/tests
Jan 26 21:54:33 Finished compiler/inference/tests                              4m07s   6GB
Jan 26 21:54:34 Starting compiler/bootstrap/translation
Jan 27 00:27:07 Finished compiler/bootstrap/translation                     2h32m31s  39GB
Jan 27 00:27:08 Starting unverified/sexpr-bootstrap/x64/64
Jan 27 00:35:37 Finished unverified/sexpr-bootstrap/x64/64                     8m27s  13GB
Jan 27 00:35:38 Starting unverified/sexpr-bootstrap/x64/32
Jan 27 00:41:00 Finished unverified/sexpr-bootstrap/x64/32                     5m21s  21GB
Jan 27 00:41:01 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Jan 27 00:41:32 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            30s   1GB
Jan 27 00:41:33 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Jan 27 00:42:20 Finished compiler/benchmarks/mlton_benchmarks/cakeml             46s   1GB
Jan 27 00:42:21 Starting compiler/bootstrap/compilation/x64/64
Jan 27 10:44:50 Finished compiler/bootstrap/compilation/x64/64             10h02m26s  64GB
Jan 27 10:44:51 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 27 10:51:33 Finished compiler/bootstrap/compilation/x64/64/proofs          6m41s  35GB
Jan 27 10:51:33 Starting compiler/bootstrap/compilation/x64/32
Jan 27 19:58:47 Finished compiler/bootstrap/compilation/x64/32              9h07m10s  64GB
Jan 27 19:58:47 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 27 20:04:34 Finished compiler/bootstrap/compilation/x64/32/proofs          5m46s  31GB
Jan 27 20:04:35 SUCCESS