Job 701

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
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 01:44:10 Claimed job
Jan 26 01:44:18 Reusing HOL
Jan 26 01:45:08 Starting developers
Jan 26 01:45:11 Finished developers                                               2s  20MB
Jan 26 01:45:12 Starting developers/bin
Jan 26 01:46:25 Finished developers/bin                                        1m12s 918MB
Jan 26 01:46:25 Starting semantics/ffi
Jan 26 01:46:36 Finished semantics/ffi                                           10s 232MB
Jan 26 01:46:37 Starting semantics
Jan 26 01:48:00 Finished semantics                                             1m22s   1GB
Jan 26 01:48:01 Starting semantics/proofs
Jan 26 01:51:17 Finished semantics/proofs                                      3m15s   1GB
Jan 26 01:51:17 Starting basis/pure
Jan 26 01:52:05 Finished basis/pure                                              46s 645MB
Jan 26 01:52:05 Starting translator
Jan 26 01:53:47 Finished translator                                            1m41s   1GB
Jan 26 01:53:48 Starting compiler/parsing
Jan 26 01:54:51 Finished compiler/parsing                                      1m02s   1GB
Jan 26 01:54:51 Starting characteristic
Jan 26 01:59:18 Finished characteristic                                        4m26s   1GB
Jan 26 01:59:19 Starting translator/monadic
Jan 26 02:00:48 Finished translator/monadic                                    1m28s   1GB
Jan 26 02:00:49 Starting basis
Jan 26 02:17:58 Finished basis                                                17m07s   2GB
Jan 26 02:17:58 Starting compiler/inference
Jan 26 02:19:39 Finished compiler/inference                                    1m40s   1GB
Jan 26 02:19:40 Starting compiler/backend/reg_alloc
Jan 26 02:20:32 Finished compiler/backend/reg_alloc                              51s   1GB
Jan 26 02:20:32 Starting compiler/backend/gc
Jan 26 02:28:29 Finished compiler/backend/gc                                   7m56s   1GB
Jan 26 02:28:30 Starting compiler/backend
Jan 26 02:28:33 Finished compiler/backend                                         2s  23MB
Jan 26 02:28:34 Starting compiler/encoders/asm
Jan 26 02:28:35 Finished compiler/encoders/asm                                    1s  16MB
Jan 26 02:28:36 Starting compiler/encoders/x64
Jan 26 02:29:02 Finished compiler/encoders/x64                                   25s 941MB
Jan 26 02:29:03 Starting compiler/encoders/arm6
Jan 26 02:29:55 Finished compiler/encoders/arm6                                  51s 746MB
Jan 26 02:29:55 Starting compiler/encoders/arm8
Jan 26 02:30:09 Finished compiler/encoders/arm8                                  13s 900MB
Jan 26 02:30:10 Starting compiler/encoders/mips
Jan 26 02:30:28 Finished compiler/encoders/mips                                  17s 874MB
Jan 26 02:30:29 Starting compiler/encoders/riscv
Jan 26 02:30:44 Finished compiler/encoders/riscv                                 14s 707MB
Jan 26 02:30:44 Starting compiler/encoders/ag32
Jan 26 02:31:03 Finished compiler/encoders/ag32                                  17s 849MB
Jan 26 02:31:03 Starting compiler/backend/x64
Jan 26 02:31:21 Finished compiler/backend/x64                                    17s 813MB
Jan 26 02:31:22 Starting compiler/backend/arm6
Jan 26 02:31:42 Finished compiler/backend/arm6                                   19s   1GB
Jan 26 02:31:43 Starting compiler/backend/arm8
Jan 26 02:32:00 Finished compiler/backend/arm8                                   16s 900MB
Jan 26 02:32:01 Starting compiler/backend/mips
Jan 26 02:32:20 Finished compiler/backend/mips                                   18s 824MB
Jan 26 02:32:20 Starting compiler/backend/riscv
Jan 26 02:32:40 Finished compiler/backend/riscv                                  18s 754MB
Jan 26 02:32:40 Starting compiler/backend/ag32
Jan 26 02:33:53 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 26 02:33:53 Starting compiler/parsing/proofs
Jan 26 02:39:47 Finished compiler/parsing/proofs                               5m52s   1GB
Jan 26 02:39:48 Starting compiler/inference/proofs
Jan 26 02:42:41 Finished compiler/inference/proofs                             2m53s   1GB
Jan 26 02:42:42 Starting compiler/backend/semantics
Jan 26 02:50:12 Finished compiler/backend/semantics                            7m28s   2GB
Jan 26 02:50:12 Starting compiler/backend/reg_alloc/proofs
Jan 26 02:52:59 Finished compiler/backend/reg_alloc/proofs                     2m46s 802MB
Jan 26 02:53:00 Starting compiler/backend/proofs
Jan 26 03:31:20 Finished compiler/backend/proofs                              38m19s   3GB
Jan 26 03:31:20 Starting compiler/encoders/x64/proofs
Jan 26 03:41:06 Finished compiler/encoders/x64/proofs                          9m44s   5GB
Jan 26 03:41:06 Starting compiler/encoders/arm6/proofs
Jan 26 03:55:04 Finished compiler/encoders/arm6/proofs                        13m56s   3GB
Jan 26 03:55:05 Starting compiler/encoders/arm8/proofs
Jan 26 04:00:59 Finished compiler/encoders/arm8/proofs                         5m53s   1GB
Jan 26 04:01:00 Starting compiler/encoders/mips/proofs
Jan 26 04:11:32 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Jan 26 04:11:33 Starting compiler/encoders/riscv/proofs
Jan 26 04:19:26 Finished compiler/encoders/riscv/proofs                        7m52s   1GB
Jan 26 04:19:26 Starting compiler/encoders/ag32/proofs
Jan 26 04:22:09 Finished compiler/encoders/ag32/proofs                         2m42s 603MB
Jan 26 04:22:10 Starting compiler/backend/x64/proofs
Jan 26 04:22:31 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 26 04:22:31 Starting compiler/backend/arm6/proofs
Jan 26 04:22:53 Finished compiler/backend/arm6/proofs                            21s 894MB
Jan 26 04:22:54 Starting compiler/backend/arm8/proofs
Jan 26 04:23:14 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 26 04:23:15 Starting compiler/backend/mips/proofs
Jan 26 04:23:36 Finished compiler/backend/mips/proofs                            20s   1GB
Jan 26 04:23:37 Starting compiler/backend/riscv/proofs
Jan 26 04:23:58 Finished compiler/backend/riscv/proofs                           20s   1GB
Jan 26 04:23:59 Starting compiler/backend/ag32/proofs
Jan 26 04:33:16 Finished compiler/backend/ag32/proofs                          9m16s   3GB
Jan 26 04:33:17 Starting compiler/proofs
Jan 26 04:34:43 Finished compiler/proofs                                       1m25s   3GB
Jan 26 04:34:43 Starting candle/set-theory
Jan 26 04:35:10 Finished candle/set-theory                                       26s 841MB
Jan 26 04:35:11 Starting candle/syntax-lib
Jan 26 04:35:22 Finished candle/syntax-lib                                       10s 525MB
Jan 26 04:35:23 Starting candle/standard/syntax
Jan 26 04:37:13 Finished candle/standard/syntax                                1m50s 947MB
Jan 26 04:37:14 Starting candle/standard/semantics
Jan 26 04:38:55 Finished candle/standard/semantics                             1m40s   1GB
Jan 26 04:38:56 Starting candle/standard/monadic
Jan 26 04:40:39 Finished candle/standard/monadic                               1m42s   1GB
Jan 26 04:40:40 Starting candle/standard/ml_kernel
Jan 26 04:44:37 Finished candle/standard/ml_kernel                             3m56s   3GB
Jan 26 04:44:38 Starting candle/standard/opentheory
Jan 26 04:53:36 Finished candle/standard/opentheory                            8m57s   4GB
Jan 26 04:53:37 Starting candle/standard/opentheory/compilation
Jan 26 05:22:46 Finished candle/standard/opentheory/compilation               29m08s  15GB
Jan 26 05:22:46 Starting candle/standard/opentheory/compilation/proofs
Jan 26 05:23:31 Finished candle/standard/opentheory/compilation/proofs           43s   4GB
Jan 26 05:23:32 Starting characteristic/examples
Jan 26 05:25:02 Finished characteristic/examples                               1m30s   2GB
Jan 26 05:25:03 Starting tutorial/solutions
Jan 26 05:38:27 Finished tutorial/solutions                                   13m23s   6GB
Jan 26 05:38:28 Starting translator/monadic/examples
Jan 26 05:40:45 Finished translator/monadic/examples                           2m15s   2GB
Jan 26 05:40:45 Starting examples
Jan 26 05:48:42 Finished examples                                              7m56s   4GB
Jan 26 05:48:43 Starting examples/compilation/x64
Jan 26 07:42:06 Finished examples/compilation/x64                           1h53m22s  10GB
Jan 26 07:42:07 Starting examples/compilation/x64/proofs
Jan 26 07:43:52 Finished examples/compilation/x64/proofs                       1m44s   4GB
Jan 26 07:43:53 Starting examples/compilation/ag32
Jan 26 08:11:49 Finished examples/compilation/ag32                            27m55s   5GB
Jan 26 08:11:49 Starting examples/compilation/ag32/proofs
Jan 26 08:12:38 Finished examples/compilation/ag32/proofs                        48s   4GB
Jan 26 08:12:39 Starting translator/okasaki-examples
Jan 26 08:16:43 Finished translator/okasaki-examples                           4m03s   1GB
Jan 26 08:16:44 Starting translator/other-examples
Jan 26 08:17:27 Finished translator/other-examples                               42s   1GB
Jan 26 08:17:27 Starting compiler/parsing/tests
Jan 26 08:17:55 Finished compiler/parsing/tests                                  27s 675MB
Jan 26 08:17:56 Starting compiler/inference/tests
Jan 26 08:21:59 Finished compiler/inference/tests                              4m02s   4GB
Jan 26 08:21:59 Starting compiler/bootstrap/translation
Jan 26 10:52:03 Finished compiler/bootstrap/translation                     2h30m03s  40GB
Jan 26 10:52:04 Starting unverified/sexpr-bootstrap/x64/64
Jan 26 11:00:49 Finished unverified/sexpr-bootstrap/x64/64                     8m43s  15GB
Jan 26 11:00:50 Starting unverified/sexpr-bootstrap/x64/32
Jan 26 11:06:21 Finished unverified/sexpr-bootstrap/x64/32                     5m29s  20GB
Jan 26 11:06:22 Starting compiler/bootstrap/compilation/x64/64
Jan 26 21:18:55 Finished compiler/bootstrap/compilation/x64/64             10h12m32s  64GB
Jan 26 21:18:56 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 26 21:25:14 Finished compiler/bootstrap/compilation/x64/64/proofs          6m17s  31GB
Jan 26 21:25:15 Starting compiler/bootstrap/compilation/x64/32
Jan 27 06:40:34 Finished compiler/bootstrap/compilation/x64/32              9h15m17s  64GB
Jan 27 06:40:35 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 27 06:46:17 Finished compiler/bootstrap/compilation/x64/32/proofs          5m41s  27GB
Jan 27 06:46:18 SUCCESS