Job 649

CakeML:d52367872019adae2f534beada039ced30000748
  Remove unverified/benchmarks and tweak Holmakefile [Dec 25 14:17:52]
HOL:89daca206b2ad7a8e43f3a59c20a178cc04d7748
  Fix bug: TypeBase.simpls_of not being filled in on load [Dec 21 04:04:45]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 25 17:00:02 Claimed job
Dec 25 17:00:12 Reusing HOL
Dec 25 17:01:02 Starting developers
Dec 25 17:01:05 Finished developers                                               2s  20MB
Dec 25 17:01:06 Starting developers/bin
Dec 25 17:02:13 Finished developers/bin                                        1m05s 916MB
Dec 25 17:02:13 Starting semantics/ffi
Dec 25 17:02:24 Finished semantics/ffi                                           10s 233MB
Dec 25 17:02:25 Starting semantics
Dec 25 17:03:50 Finished semantics                                             1m24s   1GB
Dec 25 17:03:50 Starting semantics/proofs
Dec 25 17:07:13 Finished semantics/proofs                                      3m22s   1GB
Dec 25 17:07:14 Starting basis/pure
Dec 25 17:08:09 Finished basis/pure                                              53s 643MB
Dec 25 17:08:09 Starting translator
Dec 25 17:09:50 Finished translator                                            1m39s   1GB
Dec 25 17:09:51 Starting compiler/parsing
Dec 25 17:10:55 Finished compiler/parsing                                      1m03s   1GB
Dec 25 17:10:56 Starting characteristic
Dec 25 17:14:19 Finished characteristic                                        3m22s   1GB
Dec 25 17:14:20 Starting translator/monadic
Dec 25 17:15:48 Finished translator/monadic                                    1m28s   1GB
Dec 25 17:15:49 Starting basis
Dec 25 17:32:09 Finished basis                                                16m19s   3GB
Dec 25 17:32:10 Starting compiler/inference
Dec 25 17:33:50 Finished compiler/inference                                    1m39s   1GB
Dec 25 17:33:50 Starting compiler/backend/reg_alloc
Dec 25 17:34:44 Finished compiler/backend/reg_alloc                              52s   1GB
Dec 25 17:34:44 Starting compiler/backend/gc
Dec 25 17:42:48 Finished compiler/backend/gc                                   8m02s   1GB
Dec 25 17:42:49 Starting compiler/backend
Dec 25 17:42:52 Finished compiler/backend                                         2s  16MB
Dec 25 17:42:52 Starting compiler/encoders/asm
Dec 25 17:42:54 Finished compiler/encoders/asm                                    1s  25MB
Dec 25 17:42:55 Starting compiler/encoders/x64
Dec 25 17:43:21 Finished compiler/encoders/x64                                   25s 931MB
Dec 25 17:43:22 Starting compiler/encoders/arm6
Dec 25 17:44:20 Finished compiler/encoders/arm6                                  57s 804MB
Dec 25 17:44:21 Starting compiler/encoders/arm8
Dec 25 17:44:35 Finished compiler/encoders/arm8                                  13s 860MB
Dec 25 17:44:36 Starting compiler/encoders/mips
Dec 25 17:44:54 Finished compiler/encoders/mips                                  17s   1GB
Dec 25 17:44:55 Starting compiler/encoders/riscv
Dec 25 17:45:10 Finished compiler/encoders/riscv                                 14s 778MB
Dec 25 17:45:11 Starting compiler/encoders/ag32
Dec 25 17:45:29 Finished compiler/encoders/ag32                                  17s 576MB
Dec 25 17:45:29 Starting compiler/backend/x64
Dec 25 17:45:47 Finished compiler/backend/x64                                    16s 788MB
Dec 25 17:45:48 Starting compiler/backend/arm6
Dec 25 17:46:08 Finished compiler/backend/arm6                                   19s   1GB
Dec 25 17:46:09 Starting compiler/backend/arm8
Dec 25 17:46:28 Finished compiler/backend/arm8                                   18s   1GB
Dec 25 17:46:28 Starting compiler/backend/mips
Dec 25 17:46:49 Finished compiler/backend/mips                                   19s   1GB
Dec 25 17:46:49 Starting compiler/backend/riscv
Dec 25 17:47:09 Finished compiler/backend/riscv                                  19s   1GB
Dec 25 17:47:10 Starting compiler/backend/ag32
Dec 25 17:48:23 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 25 17:48:24 Starting compiler/parsing/proofs
Dec 25 17:54:40 Finished compiler/parsing/proofs                               6m15s 950MB
Dec 25 17:54:40 Starting compiler/inference/proofs
Dec 25 17:57:36 Finished compiler/inference/proofs                             2m55s   1GB
Dec 25 17:57:37 Starting compiler/backend/semantics
Dec 25 18:05:10 Finished compiler/backend/semantics                            7m32s   1GB
Dec 25 18:05:11 Starting compiler/backend/reg_alloc/proofs
Dec 25 18:07:57 Finished compiler/backend/reg_alloc/proofs                     2m46s 747MB
Dec 25 18:07:58 Starting compiler/backend/proofs
Dec 25 18:46:28 Finished compiler/backend/proofs                              38m28s   3GB
Dec 25 18:46:28 Starting compiler/encoders/x64/proofs
Dec 25 18:56:21 Finished compiler/encoders/x64/proofs                          9m52s   4GB
Dec 25 18:56:22 Starting compiler/encoders/arm6/proofs
Dec 25 19:10:28 Finished compiler/encoders/arm6/proofs                        14m05s   3GB
Dec 25 19:10:29 Starting compiler/encoders/arm8/proofs
Dec 25 19:16:27 Finished compiler/encoders/arm8/proofs                         5m57s   1GB
Dec 25 19:16:28 Starting compiler/encoders/mips/proofs
Dec 25 19:27:00 Finished compiler/encoders/mips/proofs                        10m31s   2GB
Dec 25 19:27:01 Starting compiler/encoders/riscv/proofs
Dec 25 19:34:42 Finished compiler/encoders/riscv/proofs                        7m41s   1GB
Dec 25 19:34:43 Starting compiler/encoders/ag32/proofs
Dec 25 19:37:27 Finished compiler/encoders/ag32/proofs                         2m43s 710MB
Dec 25 19:37:28 Starting compiler/backend/x64/proofs
Dec 25 19:37:48 Finished compiler/backend/x64/proofs                             19s 815MB
Dec 25 19:37:49 Starting compiler/backend/arm6/proofs
Dec 25 19:38:12 Finished compiler/backend/arm6/proofs                            22s   1GB
Dec 25 19:38:13 Starting compiler/backend/arm8/proofs
Dec 25 19:38:32 Finished compiler/backend/arm8/proofs                            18s 834MB
Dec 25 19:38:32 Starting compiler/backend/mips/proofs
Dec 25 19:38:55 Finished compiler/backend/mips/proofs                            21s 898MB
Dec 25 19:38:55 Starting compiler/backend/riscv/proofs
Dec 25 19:39:17 Finished compiler/backend/riscv/proofs                           20s   1GB
Dec 25 19:39:17 Starting compiler/backend/ag32/proofs
Dec 25 19:48:34 Finished compiler/backend/ag32/proofs                          9m15s   2GB
Dec 25 19:48:35 Starting compiler/proofs
Dec 25 19:49:57 Finished compiler/proofs                                       1m21s   3GB
Dec 25 19:49:58 Starting candle/set-theory
Dec 25 19:50:26 Finished candle/set-theory                                       27s 693MB
Dec 25 19:50:26 Starting candle/syntax-lib
Dec 25 19:50:37 Finished candle/syntax-lib                                       10s 455MB
Dec 25 19:50:38 Starting candle/standard/syntax
Dec 25 19:52:30 Finished candle/standard/syntax                                1m51s   1GB
Dec 25 19:52:31 Starting candle/standard/semantics
Dec 25 19:54:14 Finished candle/standard/semantics                             1m42s   1GB
Dec 25 19:54:15 Starting candle/standard/monadic
Dec 25 19:56:00 Finished candle/standard/monadic                               1m44s   1GB
Dec 25 19:56:01 Starting candle/standard/ml_kernel
Dec 25 20:11:23 Finished candle/standard/ml_kernel                            15m21s   3GB
Dec 25 20:11:24 Starting candle/standard/opentheory
Dec 25 20:20:24 Finished candle/standard/opentheory                            8m59s   5GB
Dec 25 20:20:24 Starting candle/standard/opentheory/compilation
Dec 25 20:49:17 Finished candle/standard/opentheory/compilation               28m51s  14GB
Dec 25 20:49:17 Starting candle/standard/opentheory/compilation/proofs
Dec 25 20:50:07 Finished candle/standard/opentheory/compilation/proofs           49s   5GB
Dec 25 20:50:08 Starting characteristic/examples
Dec 25 20:51:42 Finished characteristic/examples                               1m33s   2GB
Dec 25 20:51:42 Starting tutorial/solutions
Dec 25 21:05:13 Finished tutorial/solutions                                   13m29s   6GB
Dec 25 21:05:14 Starting translator/monadic/examples
Dec 25 21:07:27 Finished translator/monadic/examples                           2m12s   3GB
Dec 25 21:07:27 Starting examples
Dec 25 21:15:18 Finished examples                                              7m49s   3GB
Dec 25 21:15:18 Starting examples/compilation/x64
Dec 25 23:17:18 Finished examples/compilation/x64                           2h01m58s  11GB
Dec 25 23:17:19 Starting examples/compilation/x64/proofs
Dec 25 23:19:08 Finished examples/compilation/x64/proofs                       1m48s   4GB
Dec 25 23:19:09 Starting examples/compilation/ag32
Dec 25 23:46:29 Finished examples/compilation/ag32                            27m20s   6GB
Dec 25 23:46:30 Starting examples/compilation/ag32/proofs
Dec 25 23:47:20 Finished examples/compilation/ag32/proofs                        48s   4GB
Dec 25 23:47:20 Starting translator/okasaki-examples
Dec 25 23:51:22 Finished translator/okasaki-examples                           4m01s   1GB
Dec 25 23:51:23 Starting translator/other-examples
Dec 25 23:52:06 Finished translator/other-examples                               42s   1GB
Dec 25 23:52:06 Starting compiler/parsing/tests
Dec 25 23:52:34 Finished compiler/parsing/tests                                  26s 570MB
Dec 25 23:52:34 Starting compiler/inference/tests
Dec 25 23:56:33 Finished compiler/inference/tests                              3m57s   4GB
Dec 25 23:56:33 Starting compiler/bootstrap/translation
Dec 26 03:26:33 Finished compiler/bootstrap/translation                     3h29m58s  47GB
Dec 26 03:26:34 Starting unverified/sexpr-bootstrap/x64/64
Dec 26 03:29:11 Finished unverified/sexpr-bootstrap/x64/64                     2m37s  22GB
Dec 26 03:29:12 Starting unverified/sexpr-bootstrap/x64/32
Dec 26 03:31:31 Finished unverified/sexpr-bootstrap/x64/32                     2m18s  19GB
Dec 26 03:31:31 Starting compiler/bootstrap/compilation/x64/64
Dec 26 13:25:38 Finished compiler/bootstrap/compilation/x64/64              9h54m05s  63GB
Dec 26 13:25:38 Starting compiler/bootstrap/compilation/x64/64/proofs
Dec 26 13:32:12 Finished compiler/bootstrap/compilation/x64/64/proofs          6m32s  31GB
Dec 26 13:32:13 Starting compiler/bootstrap/compilation/x64/32
Dec 26 22:18:34 Finished compiler/bootstrap/compilation/x64/32              8h46m21s  64GB
Dec 26 22:18:35 Starting compiler/bootstrap/compilation/x64/32/proofs
Dec 26 22:24:12 Finished compiler/bootstrap/compilation/x64/32/proofs          5m36s  27GB
Dec 26 22:24:13 SUCCESS