Job 699

CakeML:f15fc331b263bceb940dc8e8a6c766d48f25d09d
  Make build-sequence include compiling the benchmarks [Jan 24 17:45:51]
#610 (build-benchmarks)
Merging into:132124a020e9f4e4bb00fb0274f9505461195904
  Merge pull request #608 from CakeML/cheats [Jan 21 17:46:50]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 24 20:20:23 Claimed job
Jan 24 20:20:33 Reusing HOL
Jan 24 20:21:23 Starting developers
Jan 24 20:21:26 Finished developers                                               2s  20MB
Jan 24 20:21:27 Starting developers/bin
Jan 24 20:22:36 Finished developers/bin                                        1m07s 918MB
Jan 24 20:22:36 Starting semantics/ffi
Jan 24 20:22:47 Finished semantics/ffi                                           10s 234MB
Jan 24 20:22:47 Starting semantics
Jan 24 20:24:10 Finished semantics                                             1m21s   1GB
Jan 24 20:24:11 Starting semantics/proofs
Jan 24 20:27:28 Finished semantics/proofs                                      3m16s   1GB
Jan 24 20:27:28 Starting basis/pure
Jan 24 20:28:17 Finished basis/pure                                              47s 683MB
Jan 24 20:28:17 Starting translator
Jan 24 20:30:00 Finished translator                                            1m42s   1GB
Jan 24 20:30:01 Starting compiler/parsing
Jan 24 20:31:05 Finished compiler/parsing                                      1m03s   1GB
Jan 24 20:31:06 Starting characteristic
Jan 24 20:34:26 Finished characteristic                                        3m19s   1GB
Jan 24 20:34:27 Starting translator/monadic
Jan 24 20:35:56 Finished translator/monadic                                    1m28s   1GB
Jan 24 20:35:57 Starting basis
Jan 24 20:52:44 Finished basis                                                16m46s   3GB
Jan 24 20:52:44 Starting compiler/inference
Jan 24 20:54:24 Finished compiler/inference                                    1m38s   1GB
Jan 24 20:54:25 Starting compiler/backend/reg_alloc
Jan 24 20:55:18 Finished compiler/backend/reg_alloc                              52s   1GB
Jan 24 20:55:19 Starting compiler/backend/gc
Jan 24 21:03:18 Finished compiler/backend/gc                                   7m58s   1GB
Jan 24 21:03:19 Starting compiler/backend
Jan 24 21:03:22 Finished compiler/backend                                         2s  22MB
Jan 24 21:03:22 Starting compiler/encoders/asm
Jan 24 21:03:24 Finished compiler/encoders/asm                                    1s  19MB
Jan 24 21:03:25 Starting compiler/encoders/x64
Jan 24 21:03:51 Finished compiler/encoders/x64                                   25s 981MB
Jan 24 21:03:52 Starting compiler/encoders/arm6
Jan 24 21:04:44 Finished compiler/encoders/arm6                                  51s 681MB
Jan 24 21:04:45 Starting compiler/encoders/arm8
Jan 24 21:04:59 Finished compiler/encoders/arm8                                  13s 512MB
Jan 24 21:05:00 Starting compiler/encoders/mips
Jan 24 21:05:17 Finished compiler/encoders/mips                                  17s 746MB
Jan 24 21:05:18 Starting compiler/encoders/riscv
Jan 24 21:05:33 Finished compiler/encoders/riscv                                 14s 709MB
Jan 24 21:05:34 Starting compiler/encoders/ag32
Jan 24 21:05:51 Finished compiler/encoders/ag32                                  17s 744MB
Jan 24 21:05:52 Starting compiler/backend/x64
Jan 24 21:06:10 Finished compiler/backend/x64                                    17s 820MB
Jan 24 21:06:11 Starting compiler/backend/arm6
Jan 24 21:06:32 Finished compiler/backend/arm6                                   20s   1GB
Jan 24 21:06:33 Starting compiler/backend/arm8
Jan 24 21:06:51 Finished compiler/backend/arm8                                   17s   1GB
Jan 24 21:06:52 Starting compiler/backend/mips
Jan 24 21:07:11 Finished compiler/backend/mips                                   18s   1GB
Jan 24 21:07:12 Starting compiler/backend/riscv
Jan 24 21:07:31 Finished compiler/backend/riscv                                  19s   1GB
Jan 24 21:07:32 Starting compiler/backend/ag32
Jan 24 21:08:45 Finished compiler/backend/ag32                                 1m12s 916MB
Jan 24 21:08:46 Starting compiler/parsing/proofs
Jan 24 21:14:36 Finished compiler/parsing/proofs                               5m50s 875MB
Jan 24 21:14:37 Starting compiler/inference/proofs
Jan 24 21:17:33 Finished compiler/inference/proofs                             2m55s 953MB
Jan 24 21:17:34 Starting compiler/backend/semantics
Jan 24 21:25:04 Finished compiler/backend/semantics                            7m29s   2GB
Jan 24 21:25:05 Starting compiler/backend/reg_alloc/proofs
Jan 24 21:27:50 Finished compiler/backend/reg_alloc/proofs                     2m44s 771MB
Jan 24 21:27:51 Starting compiler/backend/proofs
Jan 24 22:06:50 Finished compiler/backend/proofs                              38m58s   3GB
Jan 24 22:06:50 Starting compiler/encoders/x64/proofs
Jan 24 22:16:42 Finished compiler/encoders/x64/proofs                          9m50s   4GB
Jan 24 22:16:42 Starting compiler/encoders/arm6/proofs
Jan 24 22:30:34 Finished compiler/encoders/arm6/proofs                        13m51s   3GB
Jan 24 22:30:35 Starting compiler/encoders/arm8/proofs
Jan 24 22:36:33 Finished compiler/encoders/arm8/proofs                         5m57s   1GB
Jan 24 22:36:33 Starting compiler/encoders/mips/proofs
Jan 24 22:47:16 Finished compiler/encoders/mips/proofs                        10m41s   2GB
Jan 24 22:47:16 Starting compiler/encoders/riscv/proofs
Jan 24 22:55:12 Finished compiler/encoders/riscv/proofs                        7m54s 990MB
Jan 24 22:55:12 Starting compiler/encoders/ag32/proofs
Jan 24 22:57:54 Finished compiler/encoders/ag32/proofs                         2m41s 656MB
Jan 24 22:57:55 Starting compiler/backend/x64/proofs
Jan 24 22:58:16 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 24 22:58:16 Starting compiler/backend/arm6/proofs
Jan 24 22:58:39 Finished compiler/backend/arm6/proofs                            21s 931MB
Jan 24 22:58:40 Starting compiler/backend/arm8/proofs
Jan 24 22:58:59 Finished compiler/backend/arm8/proofs                            18s   1GB
Jan 24 22:59:00 Starting compiler/backend/mips/proofs
Jan 24 22:59:21 Finished compiler/backend/mips/proofs                            21s   1GB
Jan 24 22:59:22 Starting compiler/backend/riscv/proofs
Jan 24 22:59:43 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 24 22:59:44 Starting compiler/backend/ag32/proofs
Jan 24 23:08:58 Finished compiler/backend/ag32/proofs                          9m13s   2GB
Jan 24 23:08:59 Starting compiler/proofs
Jan 24 23:10:21 Finished compiler/proofs                                       1m21s   3GB
Jan 24 23:10:22 Starting candle/set-theory
Jan 24 23:10:50 Finished candle/set-theory                                       27s 682MB
Jan 24 23:10:51 Starting candle/syntax-lib
Jan 24 23:11:02 Finished candle/syntax-lib                                       10s 627MB
Jan 24 23:11:02 Starting candle/standard/syntax
Jan 24 23:12:53 Finished candle/standard/syntax                                1m49s 933MB
Jan 24 23:12:53 Starting candle/standard/semantics
Jan 24 23:14:35 Finished candle/standard/semantics                             1m41s   1GB
Jan 24 23:14:36 Starting candle/standard/monadic
Jan 24 23:16:19 Finished candle/standard/monadic                               1m41s   1GB
Jan 24 23:16:19 Starting candle/standard/ml_kernel
Jan 24 23:20:12 Finished candle/standard/ml_kernel                             3m51s   3GB
Jan 24 23:20:12 Starting candle/standard/opentheory
Jan 24 23:29:02 Finished candle/standard/opentheory                            8m48s   4GB
Jan 24 23:29:03 Starting candle/standard/opentheory/compilation
Jan 24 23:57:57 Finished candle/standard/opentheory/compilation               28m53s  15GB
Jan 24 23:57:57 Starting candle/standard/opentheory/compilation/proofs
Jan 24 23:58:46 Finished candle/standard/opentheory/compilation/proofs           47s   5GB
Jan 24 23:58:46 Starting characteristic/examples
Jan 25 00:00:15 Finished characteristic/examples                               1m28s   2GB
Jan 25 00:00:16 Starting tutorial/solutions
Jan 25 00:13:39 Finished tutorial/solutions                                   13m22s   7GB
Jan 25 00:13:39 Starting translator/monadic/examples
Jan 25 00:15:56 Finished translator/monadic/examples                           2m16s   2GB
Jan 25 00:15:57 Starting examples
Jan 25 00:23:32 Finished examples                                              7m34s   4GB
Jan 25 00:23:33 Starting examples/compilation/x64
Jan 25 02:16:12 Finished examples/compilation/x64                           1h52m38s  12GB
Jan 25 02:16:13 Starting examples/compilation/x64/proofs
Jan 25 02:18:01 Finished examples/compilation/x64/proofs                       1m47s   4GB
Jan 25 02:18:01 Starting examples/compilation/ag32
Jan 25 02:46:10 Finished examples/compilation/ag32                            28m07s   5GB
Jan 25 02:46:11 Starting examples/compilation/ag32/proofs
Jan 25 02:46:59 Finished examples/compilation/ag32/proofs                        47s   3GB
Jan 25 02:46:59 Starting translator/okasaki-examples
Jan 25 02:51:04 Finished translator/okasaki-examples                           4m03s   1GB
Jan 25 02:51:04 Starting translator/other-examples
Jan 25 02:51:48 Finished translator/other-examples                               43s   1GB
Jan 25 02:51:49 Starting compiler/parsing/tests
Jan 25 02:52:15 Finished compiler/parsing/tests                                  25s 779MB
Jan 25 02:52:16 Starting compiler/inference/tests
Jan 25 02:56:19 Finished compiler/inference/tests                              4m03s   3GB
Jan 25 02:56:20 Starting compiler/bootstrap/translation
Jan 25 05:27:51 Finished compiler/bootstrap/translation                     2h31m29s  39GB
Jan 25 05:27:52 Starting unverified/sexpr-bootstrap/x64/64
Jan 25 05:36:41 Finished unverified/sexpr-bootstrap/x64/64                     8m48s  15GB
Jan 25 05:36:42 Starting unverified/sexpr-bootstrap/x64/32
Jan 25 05:42:11 Finished unverified/sexpr-bootstrap/x64/32                     5m28s  22GB
Jan 25 05:42:12 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Jan 25 05:42:45 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            32s   1GB
Jan 25 05:42:45 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Jan 25 05:43:36 Finished compiler/benchmarks/mlton_benchmarks/cakeml             49s   1GB
Jan 25 05:43:37 Starting compiler/bootstrap/compilation/x64/64
Jan 25 16:18:35 Finished compiler/bootstrap/compilation/x64/64             10h34m57s  64GB
Jan 25 16:18:36 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 25 16:25:23 Finished compiler/bootstrap/compilation/x64/64/proofs          6m46s  34GB
Jan 25 16:25:24 Starting compiler/bootstrap/compilation/x64/32
Jan 26 01:38:18 Finished compiler/bootstrap/compilation/x64/32              9h12m53s  64GB
Jan 26 01:38:19 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 26 01:44:07 Finished compiler/bootstrap/compilation/x64/32/proofs          5m47s  31GB
Jan 26 01:44:07 SUCCESS