Job 613

CakeML:0870034efc52ecc4e47b0ce23c876eeb648f440c
  Merge pull request #572 from CakeML/cleanup [Dec 05 08:29:36]
HOL:e1f96c8c7ba8d5d3db5d3ed3bbed3d5ec3a309a6
  Fix bug in proof (18934f7cf gave 2 theorems same name) [Dec 04 10:59:11]
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

Dec 05 10:30:37 Claimed job
Dec 05 10:30:45 Reusing HOL
Dec 05 10:31:36 Starting developers
Dec 05 10:31:39 Finished developers                                               2s  20MB
Dec 05 10:31:40 Starting developers/bin
Dec 05 10:33:00 Finished developers/bin                                        1m19s 916MB
Dec 05 10:33:00 Starting semantics/ffi
Dec 05 10:33:11 Finished semantics/ffi                                           10s 224MB
Dec 05 10:33:12 Starting semantics
Dec 05 10:34:31 Finished semantics                                             1m17s 843MB
Dec 05 10:34:31 Starting semantics/proofs
Dec 05 10:37:31 Finished semantics/proofs                                      2m58s   1GB
Dec 05 10:37:31 Starting basis/pure
Dec 05 10:38:24 Finished basis/pure                                              51s 658MB
Dec 05 10:38:25 Starting translator
Dec 05 10:39:40 Finished translator                                            1m15s 974MB
Dec 05 10:39:41 Starting compiler/parsing
Dec 05 10:40:58 Finished compiler/parsing                                      1m16s   1GB
Dec 05 10:40:58 Starting characteristic
Dec 05 10:43:35 Finished characteristic                                        2m35s   1GB
Dec 05 10:43:35 Starting translator/monadic
Dec 05 10:45:04 Finished translator/monadic                                    1m28s   1GB
Dec 05 10:45:05 Starting basis
Dec 05 11:01:16 Finished basis                                                16m10s   3GB
Dec 05 11:01:17 Starting compiler/inference
Dec 05 11:03:00 Finished compiler/inference                                    1m42s   1GB
Dec 05 11:03:00 Starting compiler/backend/reg_alloc
Dec 05 11:03:47 Finished compiler/backend/reg_alloc                              46s   1GB
Dec 05 11:03:48 Starting compiler/backend/gc
Dec 05 11:10:10 Finished compiler/backend/gc                                   6m21s   1GB
Dec 05 11:10:11 Starting compiler/backend
Dec 05 11:10:14 Finished compiler/backend                                         2s  22MB
Dec 05 11:10:14 Starting compiler/encoders/asm
Dec 05 11:10:16 Finished compiler/encoders/asm                                    1s  14MB
Dec 05 11:10:17 Starting compiler/encoders/x64
Dec 05 11:10:32 Finished compiler/encoders/x64                                   14s 382MB
Dec 05 11:10:33 Starting compiler/encoders/arm6
Dec 05 11:11:15 Finished compiler/encoders/arm6                                  41s 407MB
Dec 05 11:11:16 Starting compiler/encoders/arm8
Dec 05 11:11:25 Finished compiler/encoders/arm8                                   8s 430MB
Dec 05 11:11:26 Starting compiler/encoders/mips
Dec 05 11:11:36 Finished compiler/encoders/mips                                   9s 441MB
Dec 05 11:11:36 Starting compiler/encoders/riscv
Dec 05 11:11:46 Finished compiler/encoders/riscv                                  8s 420MB
Dec 05 11:11:46 Starting compiler/encoders/ag32
Dec 05 11:12:04 Finished compiler/encoders/ag32                                  17s 835MB
Dec 05 11:12:05 Starting compiler/backend/x64
Dec 05 11:12:24 Finished compiler/backend/x64                                    18s   1GB
Dec 05 11:12:24 Starting compiler/backend/arm6
Dec 05 11:12:46 Finished compiler/backend/arm6                                   20s   1GB
Dec 05 11:12:46 Starting compiler/backend/arm8
Dec 05 11:13:06 Finished compiler/backend/arm8                                   18s   1GB
Dec 05 11:13:06 Starting compiler/backend/mips
Dec 05 11:13:26 Finished compiler/backend/mips                                   18s   1GB
Dec 05 11:13:26 Starting compiler/backend/riscv
Dec 05 11:13:45 Finished compiler/backend/riscv                                  17s 943MB
Dec 05 11:13:45 Starting compiler/backend/ag32
Dec 05 11:14:58 Finished compiler/backend/ag32                                 1m11s   1GB
Dec 05 11:14:58 Starting compiler/parsing/proofs
Dec 05 11:21:04 Finished compiler/parsing/proofs                               6m05s 815MB
Dec 05 11:21:05 Starting compiler/inference/proofs
Dec 05 11:23:58 Finished compiler/inference/proofs                             2m52s 998MB
Dec 05 11:23:59 Starting compiler/backend/semantics
Dec 05 11:32:45 Finished compiler/backend/semantics                            8m45s   2GB
Dec 05 11:32:45 Starting compiler/backend/reg_alloc/proofs
Dec 05 11:35:30 Finished compiler/backend/reg_alloc/proofs                     2m43s 544MB
Dec 05 11:35:31 Starting compiler/backend/proofs
Dec 05 12:17:33 Finished compiler/backend/proofs                              42m01s   3GB
Dec 05 12:17:34 Starting compiler/encoders/x64/proofs
Dec 05 12:26:44 Finished compiler/encoders/x64/proofs                          9m10s 850MB
Dec 05 12:26:45 Starting compiler/encoders/arm6/proofs
Dec 05 12:40:21 Finished compiler/encoders/arm6/proofs                        13m35s   1GB
Dec 05 12:40:22 Starting compiler/encoders/arm8/proofs
Dec 05 12:46:13 Finished compiler/encoders/arm8/proofs                         5m50s   1GB
Dec 05 12:46:14 Starting compiler/encoders/mips/proofs
Dec 05 12:56:05 Finished compiler/encoders/mips/proofs                         9m50s   1GB
Dec 05 12:56:05 Starting compiler/encoders/riscv/proofs
Dec 05 13:03:56 Finished compiler/encoders/riscv/proofs                        7m49s 733MB
Dec 05 13:03:57 Starting compiler/encoders/ag32/proofs
Dec 05 13:06:39 Finished compiler/encoders/ag32/proofs                         2m41s 702MB
Dec 05 13:06:39 Starting compiler/backend/x64/proofs
Dec 05 13:07:00 Finished compiler/backend/x64/proofs                             20s   1GB
Dec 05 13:07:01 Starting compiler/backend/arm6/proofs
Dec 05 13:07:26 Finished compiler/backend/arm6/proofs                            24s   1GB
Dec 05 13:07:27 Starting compiler/backend/arm8/proofs
Dec 05 13:07:47 Finished compiler/backend/arm8/proofs                            19s 765MB
Dec 05 13:07:48 Starting compiler/backend/mips/proofs
Dec 05 13:08:09 Finished compiler/backend/mips/proofs                            20s   1GB
Dec 05 13:08:09 Starting compiler/backend/riscv/proofs
Dec 05 13:08:31 Finished compiler/backend/riscv/proofs                           20s   1GB
Dec 05 13:08:32 Starting compiler/backend/ag32/proofs
Dec 05 13:17:49 Finished compiler/backend/ag32/proofs                          9m16s   2GB
Dec 05 13:17:49 Starting compiler/proofs
Dec 05 13:19:10 Finished compiler/proofs                                       1m19s   2GB
Dec 05 13:19:10 Starting candle/set-theory
Dec 05 13:19:38 Finished candle/set-theory                                       26s 622MB
Dec 05 13:19:38 Starting candle/syntax-lib
Dec 05 13:19:49 Finished candle/syntax-lib                                       10s 670MB
Dec 05 13:19:50 Starting candle/standard/syntax
Dec 05 13:21:24 Finished candle/standard/syntax                                1m33s 831MB
Dec 05 13:21:25 Starting candle/standard/semantics
Dec 05 13:22:47 Finished candle/standard/semantics                             1m21s 798MB
Dec 05 13:22:47 Starting candle/standard/monadic
Dec 05 13:24:19 Finished candle/standard/monadic                               1m31s 974MB
Dec 05 13:24:20 Starting candle/standard/ml_kernel
Dec 05 13:39:27 Finished candle/standard/ml_kernel                            15m06s   4GB
Dec 05 13:39:28 Starting candle/standard/opentheory
Dec 05 13:47:18 Finished candle/standard/opentheory                            7m49s   3GB
Dec 05 13:47:19 Starting candle/standard/opentheory/compilation
Dec 05 14:17:09 Finished candle/standard/opentheory/compilation               29m49s  16GB
Dec 05 14:17:10 Starting candle/standard/opentheory/compilation/proofs
Dec 05 14:17:49 Finished candle/standard/opentheory/compilation/proofs           38s   4GB
Dec 05 14:17:49 Starting characteristic/examples
Dec 05 14:19:22 Finished characteristic/examples                               1m31s   2GB
Dec 05 14:19:22 Starting tutorial/solutions
Dec 05 14:32:24 Finished tutorial/solutions                                   13m00s   6GB
Dec 05 14:32:24 Starting translator/monadic/examples
Dec 05 14:34:11 Finished translator/monadic/examples                           1m46s   2GB
Dec 05 14:34:12 Starting examples
Dec 05 14:40:27 Finished examples                                              6m14s   2GB
Dec 05 14:40:28 Starting examples/compilation/x64
Dec 05 16:35:24 Finished examples/compilation/x64                           1h54m54s  11GB
Dec 05 16:35:24 Starting examples/compilation/x64/proofs
Dec 05 16:37:21 Finished examples/compilation/x64/proofs                       1m56s   3GB
Dec 05 16:37:22 Starting examples/compilation/ag32
Dec 05 17:03:27 Finished examples/compilation/ag32                            26m04s   3GB
Dec 05 17:03:28 Starting examples/compilation/ag32/proofs
Dec 05 17:03:54 Finished examples/compilation/ag32/proofs                        25s   1GB
Dec 05 17:03:54 Starting compiler/benchmarks
Dec 05 17:03:56 Finished compiler/benchmarks                                      0s   5MB
Dec 05 17:03:56 Starting translator/okasaki-examples
Dec 05 17:07:24 Finished translator/okasaki-examples                           3m27s   1GB
Dec 05 17:07:25 Starting translator/other-examples
Dec 05 17:07:56 Finished translator/other-examples                               30s 733MB
Dec 05 17:07:57 Starting compiler/parsing/tests
Dec 05 17:08:23 Finished compiler/parsing/tests                                  25s 322MB
Dec 05 17:08:23 Starting compiler/inference/tests
Dec 05 17:12:20 Finished compiler/inference/tests                              3m55s   4GB
Dec 05 17:12:20 Starting compiler/bootstrap/translation
Dec 05 20:21:40 Finished compiler/bootstrap/translation                     3h09m18s  49GB
Dec 05 20:21:40 Starting unverified/sexpr-bootstrap/x64/64
Dec 05 20:29:37 Finished unverified/sexpr-bootstrap/x64/64                     7m55s  12GB
Dec 05 20:29:38 Starting unverified/sexpr-bootstrap/x64/32
Dec 05 20:35:00 Finished unverified/sexpr-bootstrap/x64/32                     5m20s  17GB
Dec 05 20:35:01 Starting compiler/bootstrap/compilation/x64/64
Dec 06 14:12:08 Finished compiler/bootstrap/compilation/x64/64             17h37m05s  64GB
Dec 06 14:12:08 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 06 14:16:27 Finished compiler/bootstrap/compilation/x64/64/proofs          4m17s  24GB
Dec 06 14:16:27 Starting compiler/bootstrap/compilation/x64/32
Dec 07 01:37:02 Finished compiler/bootstrap/compilation/x64/32             11h20m32s  63GB
Dec 07 01:37:03 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 07 01:40:23 Finished compiler/bootstrap/compilation/x64/32/proofs          3m19s  23GB
Dec 07 01:40:23 SUCCESS