Job 693

CakeML:9e7012bd41c6e8891986753f70e6c58f32cf2aff
  Merge pull request #606 from CakeML/basis-cleanup [Jan 20 10:00:43]
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 20 10:02:05 Claimed job
Jan 20 10:02:10 Reusing HOL
Jan 20 10:03:06 Starting developers
Jan 20 10:03:09 Finished developers                                               2s  21MB
Jan 20 10:03:09 Starting developers/bin
Jan 20 10:04:20 Finished developers/bin                                        1m09s 916MB
Jan 20 10:04:20 Starting semantics/ffi
Jan 20 10:04:31 Finished semantics/ffi                                            9s 234MB
Jan 20 10:04:31 Starting semantics
Jan 20 10:05:54 Finished semantics                                             1m21s   1GB
Jan 20 10:05:54 Starting semantics/proofs
Jan 20 10:09:14 Finished semantics/proofs                                      3m18s   1GB
Jan 20 10:09:15 Starting basis/pure
Jan 20 10:10:02 Finished basis/pure                                              46s 665MB
Jan 20 10:10:03 Starting translator
Jan 20 10:11:43 Finished translator                                            1m40s   1GB
Jan 20 10:11:44 Starting compiler/parsing
Jan 20 10:12:48 Finished compiler/parsing                                      1m03s   1GB
Jan 20 10:12:49 Starting characteristic
Jan 20 10:16:11 Finished characteristic                                        3m21s   1GB
Jan 20 10:16:12 Starting translator/monadic
Jan 20 10:17:41 Finished translator/monadic                                    1m28s   1GB
Jan 20 10:17:41 Starting basis
Jan 20 10:34:21 Finished basis                                                16m39s   3GB
Jan 20 10:34:22 Starting compiler/inference
Jan 20 10:36:02 Finished compiler/inference                                    1m39s   1GB
Jan 20 10:36:03 Starting compiler/backend/reg_alloc
Jan 20 10:36:55 Finished compiler/backend/reg_alloc                              51s   1GB
Jan 20 10:36:56 Starting compiler/backend/gc
Jan 20 10:44:53 Finished compiler/backend/gc                                   7m56s   1GB
Jan 20 10:44:54 Starting compiler/backend
Jan 20 10:44:57 Finished compiler/backend                                         2s  37MB
Jan 20 10:44:58 Starting compiler/encoders/asm
Jan 20 10:45:00 Finished compiler/encoders/asm                                    1s  14MB
Jan 20 10:45:00 Starting compiler/encoders/x64
Jan 20 10:45:26 Finished compiler/encoders/x64                                   25s 769MB
Jan 20 10:45:27 Starting compiler/encoders/arm6
Jan 20 10:46:19 Finished compiler/encoders/arm6                                  51s 685MB
Jan 20 10:46:20 Starting compiler/encoders/arm8
Jan 20 10:46:34 Finished compiler/encoders/arm8                                  13s 511MB
Jan 20 10:46:34 Starting compiler/encoders/mips
Jan 20 10:46:53 Finished compiler/encoders/mips                                  17s   1GB
Jan 20 10:46:53 Starting compiler/encoders/riscv
Jan 20 10:47:08 Finished compiler/encoders/riscv                                 14s 815MB
Jan 20 10:47:09 Starting compiler/encoders/ag32
Jan 20 10:47:27 Finished compiler/encoders/ag32                                  17s 512MB
Jan 20 10:47:27 Starting compiler/backend/x64
Jan 20 10:47:46 Finished compiler/backend/x64                                    18s   1GB
Jan 20 10:47:47 Starting compiler/backend/arm6
Jan 20 10:48:07 Finished compiler/backend/arm6                                   19s   1GB
Jan 20 10:48:08 Starting compiler/backend/arm8
Jan 20 10:48:26 Finished compiler/backend/arm8                                   17s 894MB
Jan 20 10:48:26 Starting compiler/backend/mips
Jan 20 10:48:46 Finished compiler/backend/mips                                   18s   1GB
Jan 20 10:48:47 Starting compiler/backend/riscv
Jan 20 10:49:05 Finished compiler/backend/riscv                                  17s 789MB
Jan 20 10:49:05 Starting compiler/backend/ag32
Jan 20 10:50:19 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 20 10:50:19 Starting compiler/parsing/proofs
Jan 20 10:56:19 Finished compiler/parsing/proofs                               5m58s 825MB
Jan 20 10:56:20 Starting compiler/inference/proofs
Jan 20 10:59:15 Finished compiler/inference/proofs                             2m54s   1GB
Jan 20 10:59:15 Starting compiler/backend/semantics
Jan 20 11:06:44 Finished compiler/backend/semantics                            7m27s   2GB
Jan 20 11:06:45 Starting compiler/backend/reg_alloc/proofs
Jan 20 11:09:30 Finished compiler/backend/reg_alloc/proofs                     2m44s   1GB
Jan 20 11:09:31 Starting compiler/backend/proofs
Jan 20 11:48:01 Finished compiler/backend/proofs                              38m29s   3GB
Jan 20 11:48:01 Starting compiler/encoders/x64/proofs
Jan 20 11:57:48 Finished compiler/encoders/x64/proofs                          9m46s   6GB
Jan 20 11:57:49 Starting compiler/encoders/arm6/proofs
Jan 20 12:11:42 Finished compiler/encoders/arm6/proofs                        13m52s   3GB
Jan 20 12:11:42 Starting compiler/encoders/arm8/proofs
Jan 20 12:17:45 Finished compiler/encoders/arm8/proofs                         6m01s   1GB
Jan 20 12:17:45 Starting compiler/encoders/mips/proofs
Jan 20 12:28:10 Finished compiler/encoders/mips/proofs                        10m24s   2GB
Jan 20 12:28:11 Starting compiler/encoders/riscv/proofs
Jan 20 12:36:08 Finished compiler/encoders/riscv/proofs                        7m56s   1GB
Jan 20 12:36:09 Starting compiler/encoders/ag32/proofs
Jan 20 12:38:51 Finished compiler/encoders/ag32/proofs                         2m41s 616MB
Jan 20 12:38:52 Starting compiler/backend/x64/proofs
Jan 20 12:39:13 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 20 12:39:13 Starting compiler/backend/arm6/proofs
Jan 20 12:39:36 Finished compiler/backend/arm6/proofs                            21s   1GB
Jan 20 12:39:36 Starting compiler/backend/arm8/proofs
Jan 20 12:39:57 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 20 12:39:57 Starting compiler/backend/mips/proofs
Jan 20 12:40:18 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 20 12:40:19 Starting compiler/backend/riscv/proofs
Jan 20 12:40:40 Finished compiler/backend/riscv/proofs                           20s   1GB
Jan 20 12:40:40 Starting compiler/backend/ag32/proofs
Jan 20 12:50:24 Finished compiler/backend/ag32/proofs                          9m43s   3GB
Jan 20 12:50:25 Starting compiler/proofs
Jan 20 12:51:48 Finished compiler/proofs                                       1m22s   2GB
Jan 20 12:51:49 Starting candle/set-theory
Jan 20 12:52:16 Finished candle/set-theory                                       26s 666MB
Jan 20 12:52:16 Starting candle/syntax-lib
Jan 20 12:52:28 Finished candle/syntax-lib                                       11s 516MB
Jan 20 12:52:29 Starting candle/standard/syntax
Jan 20 12:54:19 Finished candle/standard/syntax                                1m49s   1GB
Jan 20 12:54:20 Starting candle/standard/semantics
Jan 20 12:56:03 Finished candle/standard/semantics                             1m42s 995MB
Jan 20 12:56:04 Starting candle/standard/monadic
Jan 20 12:57:48 Finished candle/standard/monadic                               1m43s 969MB
Jan 20 12:57:48 Starting candle/standard/ml_kernel
Jan 20 13:01:34 Finished candle/standard/ml_kernel                             3m45s   5GB
Jan 20 19:52:14 Resuming candle/standard/opentheory
Jan 20 20:01:07 Finished candle/standard/opentheory                            8m52s   4GB
Jan 20 20:01:08 Starting candle/standard/opentheory/compilation
Jan 20 20:30:50 Finished candle/standard/opentheory/compilation               29m41s  13GB
Jan 20 20:30:51 Starting candle/standard/opentheory/compilation/proofs
Jan 20 20:31:41 Finished candle/standard/opentheory/compilation/proofs           49s   5GB
Jan 20 20:31:42 Starting characteristic/examples
Jan 20 20:33:10 Finished characteristic/examples                               1m27s   2GB
Jan 20 20:33:11 Starting tutorial/solutions
Jan 20 20:46:28 Finished tutorial/solutions                                   13m16s   8GB
Jan 20 20:46:28 Starting translator/monadic/examples
Jan 20 20:48:39 Finished translator/monadic/examples                           2m10s   2GB
Jan 20 20:48:40 Starting examples
Jan 20 20:56:11 Finished examples                                              7m30s   3GB
Jan 20 20:56:12 Starting examples/compilation/x64
Jan 20 22:49:41 Finished examples/compilation/x64                           1h53m28s  10GB
Jan 20 22:49:41 Starting examples/compilation/x64/proofs
Jan 20 22:51:27 Finished examples/compilation/x64/proofs                       1m45s   5GB
Jan 20 22:51:28 Starting examples/compilation/ag32
Jan 20 23:19:05 Finished examples/compilation/ag32                            27m36s   7GB
Jan 20 23:19:06 Starting examples/compilation/ag32/proofs
Jan 20 23:19:54 Finished examples/compilation/ag32/proofs                        47s   4GB
Jan 20 23:19:54 Starting translator/okasaki-examples
Jan 20 23:23:59 Finished translator/okasaki-examples                           4m03s   1GB
Jan 20 23:23:59 Starting translator/other-examples
Jan 20 23:24:43 Finished translator/other-examples                               42s   1GB
Jan 20 23:24:44 Starting compiler/parsing/tests
Jan 20 23:25:10 Finished compiler/parsing/tests                                  25s 574MB
Jan 20 23:25:10 Starting compiler/inference/tests
Jan 20 23:29:12 Finished compiler/inference/tests                              4m00s   4GB
Jan 20 23:29:13 Starting compiler/bootstrap/translation
Jan 21 01:59:03 Finished compiler/bootstrap/translation                     2h29m49s  34GB
Jan 21 01:59:04 Starting unverified/sexpr-bootstrap/x64/64
Jan 21 02:07:34 Finished unverified/sexpr-bootstrap/x64/64                     8m27s  15GB
Jan 21 02:07:35 Starting unverified/sexpr-bootstrap/x64/32
Jan 21 02:12:56 Finished unverified/sexpr-bootstrap/x64/32                     5m20s  21GB
Jan 21 02:12:57 Starting compiler/bootstrap/compilation/x64/64
Jan 21 12:30:41 Finished compiler/bootstrap/compilation/x64/64             10h17m42s  64GB
Jan 21 12:30:41 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 21 12:37:04 Finished compiler/bootstrap/compilation/x64/64/proofs          6m21s  31GB
Jan 21 12:37:04 Starting compiler/bootstrap/compilation/x64/32
Jan 21 21:54:30 Finished compiler/bootstrap/compilation/x64/32              9h17m24s  64GB
Jan 21 21:54:31 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 21 22:00:40 Finished compiler/bootstrap/compilation/x64/32/proofs          6m08s  31GB
Jan 21 22:00:41 SUCCESS