Job 667

CakeML: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:oven2 4.13.0-37-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 07 13:48:58 Claimed job
Jan 07 13:49:04 Reusing HOL
Jan 07 13:49:12 Starting developers
Jan 07 13:49:13 Finished developers                                               0s  38MB
Jan 07 13:49:14 Starting developers/bin
Jan 07 13:49:48 Finished developers/bin                                          33s 140MB
Jan 07 13:49:49 Starting semantics/ffi
Jan 07 13:49:58 Finished semantics/ffi                                            8s 225MB
Jan 07 13:49:59 Starting semantics
Jan 07 13:51:29 Finished semantics                                             1m29s   1GB
Jan 07 13:51:30 Starting semantics/proofs
Jan 07 13:54:58 Finished semantics/proofs                                      3m26s   1GB
Jan 07 13:54:59 Starting basis/pure
Jan 07 13:55:53 Finished basis/pure                                              53s 670MB
Jan 07 13:55:54 Starting translator
Jan 07 13:57:45 Finished translator                                            1m50s 979MB
Jan 07 13:57:46 Starting compiler/parsing
Jan 07 13:59:18 Finished compiler/parsing                                      1m30s   1GB
Jan 07 13:59:18 Starting characteristic
Jan 07 14:02:41 Finished characteristic                                        3m21s   1GB
Jan 07 14:02:42 Starting translator/monadic
Jan 07 14:04:10 Finished translator/monadic                                    1m27s   1GB
Jan 07 14:04:11 Starting basis
Jan 07 14:21:12 Finished basis                                                17m01s   2GB
Jan 07 14:21:13 Starting compiler/inference
Jan 07 14:22:53 Finished compiler/inference                                    1m39s   1GB
Jan 07 14:22:54 Starting compiler/backend/reg_alloc
Jan 07 14:23:55 Finished compiler/backend/reg_alloc                            1m00s   1GB
Jan 07 14:23:56 Starting compiler/backend/gc
Jan 07 14:35:30 Finished compiler/backend/gc                                  11m33s   1GB
Jan 07 14:35:31 Starting compiler/backend
Jan 07 14:35:33 Finished compiler/backend                                         1s  16MB
Jan 07 14:35:34 Starting compiler/encoders/asm
Jan 07 14:35:35 Finished compiler/encoders/asm                                    0s  16MB
Jan 07 14:35:36 Starting compiler/encoders/x64
Jan 07 14:36:09 Finished compiler/encoders/x64                                   31s 531MB
Jan 07 14:36:10 Starting compiler/encoders/arm6
Jan 07 14:37:12 Finished compiler/encoders/arm6                                1m01s 908MB
Jan 07 14:37:13 Starting compiler/encoders/arm8
Jan 07 14:37:31 Finished compiler/encoders/arm8                                  16s 541MB
Jan 07 14:37:32 Starting compiler/encoders/mips
Jan 07 14:37:55 Finished compiler/encoders/mips                                  22s   1GB
Jan 07 14:37:55 Starting compiler/encoders/riscv
Jan 07 14:38:14 Finished compiler/encoders/riscv                                 18s 943MB
Jan 07 14:38:15 Starting compiler/encoders/ag32
Jan 07 14:38:37 Finished compiler/encoders/ag32                                  21s 501MB
Jan 07 14:38:38 Starting compiler/backend/x64
Jan 07 14:39:00 Finished compiler/backend/x64                                    21s 794MB
Jan 07 14:39:01 Starting compiler/backend/arm6
Jan 07 14:39:26 Finished compiler/backend/arm6                                   24s   1GB
Jan 07 14:39:27 Starting compiler/backend/arm8
Jan 07 14:39:52 Finished compiler/backend/arm8                                   23s   1GB
Jan 07 14:39:52 Starting compiler/backend/mips
Jan 07 14:40:18 Finished compiler/backend/mips                                   24s   1GB
Jan 07 14:40:19 Starting compiler/backend/riscv
Jan 07 14:40:45 Finished compiler/backend/riscv                                  25s   1GB
Jan 07 14:40:46 Starting compiler/backend/ag32
Jan 07 14:42:25 Finished compiler/backend/ag32                                 1m38s   1GB
Jan 07 14:42:25 Starting compiler/parsing/proofs
Jan 07 14:50:06 Finished compiler/parsing/proofs                               7m39s   1GB
Jan 07 14:50:06 Starting compiler/inference/proofs
Jan 07 14:53:21 Finished compiler/inference/proofs                             3m13s   1GB
Jan 07 14:53:22 Starting compiler/backend/semantics
Jan 07 15:03:15 Finished compiler/backend/semantics                            9m53s   2GB
Jan 07 15:03:16 Starting compiler/backend/reg_alloc/proofs
Jan 07 15:06:06 Finished compiler/backend/reg_alloc/proofs                     2m49s 706MB
Jan 07 15:06:07 Starting compiler/backend/proofs
Jan 07 15:48:34 Finished compiler/backend/proofs                              42m26s   3GB
Jan 07 15:48:34 Starting compiler/encoders/x64/proofs
Jan 07 15:59:28 Finished compiler/encoders/x64/proofs                         10m52s   4GB
Jan 07 15:59:28 Starting compiler/encoders/arm6/proofs
Jan 07 16:14:37 Finished compiler/encoders/arm6/proofs                        15m07s   3GB
Jan 07 16:14:38 Starting compiler/encoders/arm8/proofs
Jan 07 16:20:58 Finished compiler/encoders/arm8/proofs                         6m19s   1GB
Jan 07 16:20:59 Starting compiler/encoders/mips/proofs
Jan 07 16:31:59 Finished compiler/encoders/mips/proofs                        10m59s   2GB
Jan 07 16:32:00 Starting compiler/encoders/riscv/proofs
Jan 07 16:40:02 Finished compiler/encoders/riscv/proofs                        8m00s   1GB
Jan 07 16:40:03 Starting compiler/encoders/ag32/proofs
Jan 07 16:42:46 Finished compiler/encoders/ag32/proofs                         2m42s 610MB
Jan 07 16:42:47 Starting compiler/backend/x64/proofs
Jan 07 16:43:07 Finished compiler/backend/x64/proofs                             19s   1GB
Jan 07 16:43:08 Starting compiler/backend/arm6/proofs
Jan 07 16:43:30 Finished compiler/backend/arm6/proofs                            20s   1GB
Jan 07 16:43:30 Starting compiler/backend/arm8/proofs
Jan 07 16:43:50 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 07 16:43:51 Starting compiler/backend/mips/proofs
Jan 07 16:44:11 Finished compiler/backend/mips/proofs                            18s   1GB
Jan 07 16:44:11 Starting compiler/backend/riscv/proofs
Jan 07 16:44:32 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 07 16:44:32 Starting compiler/backend/ag32/proofs
Jan 07 16:54:12 Finished compiler/backend/ag32/proofs                          9m38s   2GB
Jan 07 16:54:13 Starting compiler/proofs
Jan 07 16:55:33 Finished compiler/proofs                                       1m19s   3GB
Jan 07 16:55:34 Starting candle/set-theory
Jan 07 16:56:00 Finished candle/set-theory                                       24s 886MB
Jan 07 16:56:00 Starting candle/syntax-lib
Jan 07 16:56:14 Finished candle/syntax-lib                                        9s 631MB
Jan 07 16:56:15 Starting candle/standard/syntax
Jan 07 16:58:05 Finished candle/standard/syntax                                1m49s   1GB
Jan 07 16:58:06 Starting candle/standard/semantics
Jan 07 16:59:45 Finished candle/standard/semantics                             1m38s   1GB
Jan 07 16:59:46 Starting candle/standard/monadic
Jan 07 17:01:27 Finished candle/standard/monadic                               1m40s   1GB
Jan 07 17:01:28 Starting candle/standard/ml_kernel
Jan 07 17:16:56 Finished candle/standard/ml_kernel                            15m27s   3GB
Jan 07 17:16:57 Starting candle/standard/opentheory
Jan 07 17:25:57 Finished candle/standard/opentheory                            8m58s   3GB
Jan 07 17:25:57 Starting candle/standard/opentheory/compilation
Jan 07 17:56:01 Finished candle/standard/opentheory/compilation               30m02s  13GB
Jan 07 17:56:02 Starting candle/standard/opentheory/compilation/proofs
Jan 07 17:56:50 Finished candle/standard/opentheory/compilation/proofs           46s   5GB
Jan 07 17:56:50 Starting characteristic/examples
Jan 07 17:58:20 Finished characteristic/examples                               1m28s   2GB
Jan 07 17:58:21 Starting tutorial/solutions
Jan 07 18:11:26 Finished tutorial/solutions                                   13m04s   6GB
Jan 07 18:11:27 Starting translator/monadic/examples
Jan 07 18:13:34 Finished translator/monadic/examples                           2m06s   2GB
Jan 07 18:13:35 Starting examples
Jan 07 18:21:21 Finished examples                                              7m45s   3GB
Jan 07 18:21:22 Starting examples/compilation/x64
Jan 07 20:22:48 Finished examples/compilation/x64                           2h01m25s  11GB
Jan 07 20:22:49 Starting examples/compilation/x64/proofs
Jan 07 20:24:35 Finished examples/compilation/x64/proofs                       1m45s   3GB
Jan 07 20:24:36 Starting examples/compilation/ag32
Jan 07 20:52:21 Finished examples/compilation/ag32                            27m44s   5GB
Jan 07 20:52:22 Starting examples/compilation/ag32/proofs
Jan 07 20:53:08 Finished examples/compilation/ag32/proofs                        45s   4GB
Jan 07 20:53:08 Starting translator/okasaki-examples
Jan 07 20:57:20 Finished translator/okasaki-examples                           4m10s   1GB
Jan 07 20:57:21 Starting translator/other-examples
Jan 07 21:00:45 Finished translator/other-examples                             3m22s   1GB
Jan 07 21:00:46 Starting compiler/parsing/tests
Jan 07 21:01:12 Finished compiler/parsing/tests                                  25s 520MB
Jan 07 21:01:13 Starting compiler/inference/tests
Jan 07 21:05:13 Finished compiler/inference/tests                              3m59s   3GB
Jan 07 21:05:14 Starting compiler/bootstrap/translation
Jan 08 00:38:04 Finished compiler/bootstrap/translation                     3h32m48s  49GB
Jan 08 00:38:05 Starting unverified/sexpr-bootstrap/x64/64
Jan 08 00:46:15 Finished unverified/sexpr-bootstrap/x64/64                     8m08s  14GB
Jan 08 00:46:16 Starting unverified/sexpr-bootstrap/x64/32
Jan 08 00:51:15 Finished unverified/sexpr-bootstrap/x64/32                     4m56s  20GB
Jan 08 00:51:15 Starting compiler/bootstrap/compilation/x64/64
Jan 08 11:03:54 Finished compiler/bootstrap/compilation/x64/64             10h12m36s  64GB
Jan 08 11:03:55 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 08 11:09:50 Finished compiler/bootstrap/compilation/x64/64/proofs          5m53s  30GB
Jan 08 11:09:50 Starting compiler/bootstrap/compilation/x64/32
Jan 08 20:00:17 Finished compiler/bootstrap/compilation/x64/32              8h50m24s  64GB
Jan 08 20:00:17 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 08 20:06:06 Finished compiler/bootstrap/compilation/x64/32/proofs          5m47s  30GB
Jan 08 20:06:07 SUCCESS