Job 666

CakeML:1e78b6f2c23f0458b33ff988bcbdfca5a06f24b6
  Fix manual eval_rel proof in monad translator. [Jan 04 13:31:13]
#595 (local)
Merging into:371799ef0611090c155463ddcb642a80085152d7
  Work around a parsing bug in HOL [Jan 07 13:35:47]
HOL:05a6c64e4b3f9b7d262ed7f1704dd9333bbde1c7
  Merge pull request #612 from HOL-Theorem-Prover/HOL-RL [Jan 04 02:04:01]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 07 14:05:09 Claimed job
Jan 07 14:05:32 Building HOL
Jan 07 14:14:50 Starting developers
Jan 07 14:14:52 Finished developers                                               2s  21MB
Jan 07 14:14:53 Starting developers/bin
Jan 07 14:16:03 Finished developers/bin                                        1m09s 916MB
Jan 07 14:16:03 Starting semantics/ffi
Jan 07 14:16:42 Finished semantics/ffi                                           38s 375MB
Jan 07 14:16:43 Starting semantics
Jan 07 14:18:23 Finished semantics                                             1m39s   1GB
Jan 07 14:18:24 Starting semantics/proofs
Jan 07 14:21:48 Finished semantics/proofs                                      3m23s   1GB
Jan 07 14:21:49 Starting basis/pure
Jan 07 14:25:30 Finished basis/pure                                            3m40s 685MB
Jan 07 14:25:31 Starting translator
Jan 07 14:27:13 Finished translator                                            1m41s   1GB
Jan 07 14:27:14 Starting compiler/parsing
Jan 07 14:28:19 Finished compiler/parsing                                      1m04s   2GB
Jan 07 14:28:20 Starting characteristic
Jan 07 14:31:42 Finished characteristic                                        3m21s   1GB
Jan 07 14:31:42 Starting translator/monadic
Jan 07 14:33:11 Finished translator/monadic                                    1m27s   1GB
Jan 07 14:33:11 Starting basis
Jan 07 14:49:18 Finished basis                                                16m05s   2GB
Jan 07 14:49:19 Starting compiler/inference
Jan 07 14:51:19 Finished compiler/inference                                    1m59s   1GB
Jan 07 14:51:19 Starting compiler/backend/reg_alloc
Jan 07 14:52:16 Finished compiler/backend/reg_alloc                              55s   1GB
Jan 07 14:52:16 Starting compiler/backend/gc
Jan 07 15:01:46 Finished compiler/backend/gc                                   9m28s   1GB
Jan 07 15:01:47 Starting compiler/backend
Jan 07 15:01:50 Finished compiler/backend                                         2s  19MB
Jan 07 15:01:50 Starting compiler/encoders/asm
Jan 07 15:01:52 Finished compiler/encoders/asm                                    1s  18MB
Jan 07 15:01:53 Starting compiler/encoders/x64
Jan 07 15:02:55 Finished compiler/encoders/x64                                 1m01s 958MB
Jan 07 15:02:56 Starting compiler/encoders/arm6
Jan 07 15:04:54 Finished compiler/encoders/arm6                                1m57s   1GB
Jan 07 15:04:55 Starting compiler/encoders/arm8
Jan 07 15:05:28 Finished compiler/encoders/arm8                                  32s 587MB
Jan 07 15:05:29 Starting compiler/encoders/mips
Jan 07 15:06:34 Finished compiler/encoders/mips                                1m05s 969MB
Jan 07 15:06:35 Starting compiler/encoders/riscv
Jan 07 15:07:44 Finished compiler/encoders/riscv                               1m08s 806MB
Jan 07 15:07:45 Starting compiler/encoders/ag32
Jan 07 15:08:03 Finished compiler/encoders/ag32                                  17s 626MB
Jan 07 15:08:03 Starting compiler/backend/x64
Jan 07 15:08:21 Finished compiler/backend/x64                                    17s   1GB
Jan 07 15:08:22 Starting compiler/backend/arm6
Jan 07 15:08:42 Finished compiler/backend/arm6                                   19s   1GB
Jan 07 15:08:42 Starting compiler/backend/arm8
Jan 07 15:09:01 Finished compiler/backend/arm8                                   18s   1GB
Jan 07 15:09:02 Starting compiler/backend/mips
Jan 07 15:09:22 Finished compiler/backend/mips                                   19s   1GB
Jan 07 15:09:23 Starting compiler/backend/riscv
Jan 07 15:09:41 Finished compiler/backend/riscv                                  17s 979MB
Jan 07 15:09:42 Starting compiler/backend/ag32
Jan 07 15:10:55 Finished compiler/backend/ag32                                 1m12s 839MB
Jan 07 15:10:56 Starting compiler/parsing/proofs
Jan 07 15:17:15 Finished compiler/parsing/proofs                               6m18s 834MB
Jan 07 15:17:16 Starting compiler/inference/proofs
Jan 07 15:20:11 Finished compiler/inference/proofs                             2m54s 997MB
Jan 07 15:20:12 Starting compiler/backend/semantics
Jan 07 15:27:44 Finished compiler/backend/semantics                            7m30s   1GB
Jan 07 15:27:44 Starting compiler/backend/reg_alloc/proofs
Jan 07 15:30:31 Finished compiler/backend/reg_alloc/proofs                     2m46s   1GB
Jan 07 15:30:31 Starting compiler/backend/proofs
Jan 07 16:09:02 Finished compiler/backend/proofs                              38m29s   4GB
Jan 07 16:09:02 Starting compiler/encoders/x64/proofs
Jan 07 16:19:45 Finished compiler/encoders/x64/proofs                         10m42s   6GB
Jan 07 16:19:46 Starting compiler/encoders/arm6/proofs
Jan 07 16:34:47 Finished compiler/encoders/arm6/proofs                        15m00s   4GB
Jan 07 16:34:47 Starting compiler/encoders/arm8/proofs
Jan 07 16:40:54 Finished compiler/encoders/arm8/proofs                         6m06s   1GB
Jan 07 16:40:55 Starting compiler/encoders/mips/proofs
Jan 07 16:51:55 Finished compiler/encoders/mips/proofs                        10m59s   2GB
Jan 07 16:51:56 Starting compiler/encoders/riscv/proofs
Jan 07 16:59:56 Finished compiler/encoders/riscv/proofs                        7m59s   1GB
Jan 07 16:59:57 Starting compiler/encoders/ag32/proofs
Jan 07 17:02:40 Finished compiler/encoders/ag32/proofs                         2m42s 651MB
Jan 07 17:02:41 Starting compiler/backend/x64/proofs
Jan 07 17:03:01 Finished compiler/backend/x64/proofs                             20s   1GB
Jan 07 17:03:02 Starting compiler/backend/arm6/proofs
Jan 07 17:03:25 Finished compiler/backend/arm6/proofs                            22s   1GB
Jan 07 17:03:25 Starting compiler/backend/arm8/proofs
Jan 07 17:03:46 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 07 17:03:47 Starting compiler/backend/mips/proofs
Jan 07 17:04:09 Finished compiler/backend/mips/proofs                            21s   1GB
Jan 07 17:04:09 Starting compiler/backend/riscv/proofs
Jan 07 17:04:30 Finished compiler/backend/riscv/proofs                           20s   1GB
Jan 07 17:04:31 Starting compiler/backend/ag32/proofs
Jan 07 17:13:49 Finished compiler/backend/ag32/proofs                          9m17s   2GB
Jan 07 17:13:50 Starting compiler/proofs
Jan 07 17:15:13 Finished compiler/proofs                                       1m22s   3GB
Jan 07 17:15:14 Starting candle/set-theory
Jan 07 17:15:41 Finished candle/set-theory                                       26s 716MB
Jan 07 17:15:41 Starting candle/syntax-lib
Jan 07 17:15:53 Finished candle/syntax-lib                                       10s 678MB
Jan 07 17:15:53 Starting candle/standard/syntax
Jan 07 17:17:45 Finished candle/standard/syntax                                1m51s   1GB
Jan 07 17:17:46 Starting candle/standard/semantics
Jan 07 17:19:29 Finished candle/standard/semantics                             1m42s   1GB
Jan 07 17:19:30 Starting candle/standard/monadic
Jan 07 17:21:14 Finished candle/standard/monadic                               1m43s   1GB
Jan 07 17:21:14 Starting candle/standard/ml_kernel
Jan 07 17:25:07 Finished candle/standard/ml_kernel                             3m51s   3GB
Jan 07 17:25:07 Starting candle/standard/opentheory
Jan 07 17:33:56 Finished candle/standard/opentheory                            8m47s   5GB
Jan 07 17:33:56 Starting candle/standard/opentheory/compilation
Jan 07 18:02:53 Finished candle/standard/opentheory/compilation               28m56s  29GB
Jan 07 18:02:54 Starting candle/standard/opentheory/compilation/proofs
Jan 07 18:03:46 Finished candle/standard/opentheory/compilation/proofs           51s   6GB
Jan 07 18:03:47 Starting characteristic/examples
Jan 07 18:05:15 Finished characteristic/examples                               1m27s   2GB
Jan 07 18:05:16 Starting tutorial/solutions
Jan 07 18:18:18 Finished tutorial/solutions                                   13m01s   6GB
Jan 07 18:18:18 Starting translator/monadic/examples
Jan 07 18:20:30 Finished translator/monadic/examples                           2m10s   2GB
Jan 07 18:20:30 Starting examples
Jan 07 18:28:07 Finished examples                                              7m35s   3GB
Jan 07 18:28:08 Starting examples/compilation/x64
Jan 07 20:28:59 Finished examples/compilation/x64                           2h00m50s   9GB
Jan 07 20:28:59 Starting examples/compilation/x64/proofs
Jan 07 20:30:48 Finished examples/compilation/x64/proofs                       1m47s   4GB
Jan 07 20:30:48 Starting examples/compilation/ag32
Jan 07 20:58:40 Finished examples/compilation/ag32                            27m51s   5GB
Jan 07 20:58:40 Starting examples/compilation/ag32/proofs
Jan 07 20:59:29 Finished examples/compilation/ag32/proofs                        47s   4GB
Jan 07 20:59:29 Starting translator/okasaki-examples
Jan 07 21:03:31 Finished translator/okasaki-examples                           4m01s   1GB
Jan 07 21:03:32 Starting translator/other-examples
Jan 07 21:07:07 Finished translator/other-examples                             3m34s   1GB
Jan 07 21:07:08 Starting compiler/parsing/tests
Jan 07 21:07:36 Finished compiler/parsing/tests                                  27s 614MB
Jan 07 21:07:36 Starting compiler/inference/tests
Jan 07 21:11:34 Finished compiler/inference/tests                              3m57s   4GB
Jan 07 21:11:35 Starting compiler/bootstrap/translation
Jan 07 23:42:21 Finished compiler/bootstrap/translation                     2h30m44s  57GB
Jan 07 23:42:21 Starting unverified/sexpr-bootstrap/x64/64
Jan 07 23:50:40 Finished unverified/sexpr-bootstrap/x64/64                     8m17s  15GB
Jan 07 23:50:41 Starting unverified/sexpr-bootstrap/x64/32
Jan 07 23:55:30 Finished unverified/sexpr-bootstrap/x64/32                     4m48s  20GB
Jan 07 23:55:31 Starting compiler/bootstrap/compilation/x64/64
Jan 08 09:48:08 Finished compiler/bootstrap/compilation/x64/64              9h52m36s  64GB
Jan 08 09:48:09 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 08 09:54:18 Finished compiler/bootstrap/compilation/x64/64/proofs          6m08s  31GB
Jan 08 09:54:18 Starting compiler/bootstrap/compilation/x64/32
Jan 08 18:46:17 Finished compiler/bootstrap/compilation/x64/32              8h51m57s  64GB
Jan 08 18:46:18 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 08 18:52:04 Finished compiler/bootstrap/compilation/x64/32/proofs          5m46s  27GB
Jan 08 18:52:05 SUCCESS