Job 1023

CakeML:2fc3b9b98646e0fcef0eee47a1a5a8a41f02b22b
  Make a proof more robust [Aug 31 14:38:40]
HOL:def261d77aedb1c1565a5447e2e1170507b1dba8
  Fix Unicode-in-Definition test-case to not trip Unicode-in-src test [Aug 28 06:29:56]
Machine:oven2 4.15.0-34-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

Aug 31 14:49:07 Claimed job
Aug 31 14:49:59 Building HOL
Aug 31 14:57:57 Starting developers
Aug 31 14:57:59 Finished developers                                               1s  79MB
Aug 31 14:57:59 Starting developers/bin
Aug 31 14:59:32 Finished developers/bin                                        1m32s 238MB
Aug 31 14:59:32 Starting semantics/ffi
Aug 31 15:00:06 Finished semantics/ffi                                           33s 381MB
Aug 31 15:00:06 Starting semantics
Aug 31 15:01:36 Finished semantics                                             1m30s   1GB
Aug 31 15:01:37 Starting semantics/proofs
Aug 31 15:04:33 Finished semantics/proofs                                      2m55s 896MB
Aug 31 15:04:33 Starting semantics/alt_semantics
Aug 31 15:04:39 Finished semantics/alt_semantics                                  6s 261MB
Aug 31 15:04:40 Starting semantics/alt_semantics/proofs
Aug 31 15:06:28 Finished semantics/alt_semantics/proofs                        1m47s 787MB
Aug 31 15:06:28 Starting basis/pure
Aug 31 15:10:02 Finished basis/pure                                            3m33s 625MB
Aug 31 15:10:02 Starting translator
Aug 31 15:11:46 Finished translator                                            1m43s   1GB
Aug 31 15:11:47 Starting compiler/parsing
Aug 31 15:12:44 Finished compiler/parsing                                        56s   2GB
Aug 31 15:12:44 Starting characteristic
Aug 31 15:17:56 Finished characteristic                                        5m11s   1GB
Aug 31 15:17:56 Starting translator/monadic
Aug 31 15:19:22 Finished translator/monadic                                    1m25s   1GB
Aug 31 15:19:23 Starting basis
Aug 31 15:37:17 Finished basis                                                17m54s   2GB
Aug 31 15:37:18 Starting compiler/inference
Aug 31 15:39:08 Finished compiler/inference                                    1m50s   1GB
Aug 31 15:39:09 Starting compiler/backend/reg_alloc
Aug 31 15:40:06 Finished compiler/backend/reg_alloc                              56s   1GB
Aug 31 15:40:06 Starting compiler/backend/gc
Aug 31 15:49:09 Finished compiler/backend/gc                                   9m01s   2GB
Aug 31 15:49:09 Starting compiler/backend
Aug 31 15:49:10 Finished compiler/backend                                         0s  45MB
Aug 31 15:49:10 Starting compiler/encoders/asm
Aug 31 15:49:11 Finished compiler/encoders/asm                                    0s  35MB
Aug 31 15:49:11 Starting compiler/encoders/x64
Aug 31 15:50:07 Finished compiler/encoders/x64                                   55s 604MB
Aug 31 15:50:08 Starting compiler/encoders/arm7
Aug 31 15:51:44 Finished compiler/encoders/arm7                                1m36s   1GB
Aug 31 15:51:45 Starting compiler/encoders/arm8
Aug 31 15:52:13 Finished compiler/encoders/arm8                                  28s 543MB
Aug 31 15:52:14 Starting compiler/encoders/mips
Aug 31 15:53:18 Finished compiler/encoders/mips                                1m04s   1GB
Aug 31 15:53:18 Starting compiler/encoders/riscv
Aug 31 15:54:36 Finished compiler/encoders/riscv                               1m16s   1GB
Aug 31 15:54:36 Starting compiler/encoders/ag32
Aug 31 15:54:51 Finished compiler/encoders/ag32                                  14s 533MB
Aug 31 15:54:52 Starting compiler/backend/x64
Aug 31 15:55:07 Finished compiler/backend/x64                                    15s   1GB
Aug 31 15:55:08 Starting compiler/backend/arm7
Aug 31 15:55:27 Finished compiler/backend/arm7                                   18s   1GB
Aug 31 15:55:27 Starting compiler/backend/arm8
Aug 31 15:55:43 Finished compiler/backend/arm8                                   15s   1GB
Aug 31 15:55:43 Starting compiler/backend/mips
Aug 31 15:56:00 Finished compiler/backend/mips                                   16s   1GB
Aug 31 15:56:00 Starting compiler/backend/riscv
Aug 31 15:56:16 Finished compiler/backend/riscv                                  15s   1GB
Aug 31 15:56:16 Starting compiler/backend/ag32
Aug 31 15:57:23 Finished compiler/backend/ag32                                 1m05s   1GB
Aug 31 15:57:23 Starting compiler/parsing/proofs
Aug 31 16:02:56 Finished compiler/parsing/proofs                               5m32s 957MB
Aug 31 16:02:56 Starting compiler/inference/proofs
Aug 31 16:05:36 Finished compiler/inference/proofs                             2m39s   1GB
Aug 31 16:05:36 Starting compiler/backend/semantics
Aug 31 16:11:33 Finished compiler/backend/semantics                            5m56s   2GB
Aug 31 16:11:34 Starting compiler/backend/reg_alloc/proofs
Aug 31 16:14:47 Finished compiler/backend/reg_alloc/proofs                     3m13s 869MB
Aug 31 16:14:48 Starting compiler/backend/proofs
Aug 31 16:55:14 Finished compiler/backend/proofs                              40m25s   3GB
Aug 31 16:55:14 Starting compiler/encoders/x64/proofs
Aug 31 17:05:19 Finished compiler/encoders/x64/proofs                         10m03s   5GB
Aug 31 17:05:19 Starting compiler/encoders/arm7/proofs
Aug 31 17:19:02 Finished compiler/encoders/arm7/proofs                        13m42s   3GB
Aug 31 17:19:02 Starting compiler/encoders/arm8/proofs
Aug 31 17:25:51 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
Aug 31 17:25:51 Starting compiler/encoders/mips/proofs
Aug 31 17:35:49 Finished compiler/encoders/mips/proofs                         9m57s   2GB
Aug 31 17:35:49 Starting compiler/encoders/riscv/proofs
Aug 31 17:44:15 Finished compiler/encoders/riscv/proofs                        8m25s   1GB
Aug 31 17:44:16 Starting compiler/encoders/ag32/proofs
Aug 31 17:46:43 Finished compiler/encoders/ag32/proofs                         2m27s 845MB
Aug 31 17:46:43 Starting compiler/backend/x64/proofs
Aug 31 17:47:00 Finished compiler/backend/x64/proofs                             16s   1GB
Aug 31 17:47:00 Starting compiler/backend/arm7/proofs
Aug 31 17:47:18 Finished compiler/backend/arm7/proofs                            17s   1GB
Aug 31 17:47:18 Starting compiler/backend/arm8/proofs
Aug 31 17:47:35 Finished compiler/backend/arm8/proofs                            15s 773MB
Aug 31 17:47:35 Starting compiler/backend/mips/proofs
Aug 31 17:47:53 Finished compiler/backend/mips/proofs                            17s   1GB
Aug 31 17:47:53 Starting compiler/backend/riscv/proofs
Aug 31 17:48:10 Finished compiler/backend/riscv/proofs                           17s   1GB
Aug 31 17:48:11 Starting compiler/backend/ag32/proofs
Aug 31 17:57:08 Finished compiler/backend/ag32/proofs                          8m56s   2GB
Aug 31 17:57:08 Starting compiler/proofs
Aug 31 17:58:27 Finished compiler/proofs                                       1m18s   2GB
Aug 31 17:58:27 Starting candle/set-theory
Aug 31 17:58:53 Finished candle/set-theory                                       25s 752MB
Aug 31 17:58:54 Starting candle/syntax-lib
Aug 31 17:59:03 Finished candle/syntax-lib                                        9s 588MB
Aug 31 17:59:04 Starting candle/standard/syntax
Aug 31 18:00:44 Finished candle/standard/syntax                                1m40s   1GB
Aug 31 18:00:45 Starting candle/standard/semantics
Aug 31 18:02:19 Finished candle/standard/semantics                             1m33s   1GB
Aug 31 18:02:19 Starting candle/standard/monadic
Aug 31 18:03:51 Finished candle/standard/monadic                               1m31s   1GB
Aug 31 18:03:51 Starting candle/standard/ml_kernel
Aug 31 18:07:38 Finished candle/standard/ml_kernel                             3m46s   3GB
Aug 31 18:07:39 Starting candle/standard/opentheory
Aug 31 18:16:16 Finished candle/standard/opentheory                            8m36s   3GB
Aug 31 18:16:16 Starting candle/standard/opentheory/compilation
Aug 31 18:45:42 Finished candle/standard/opentheory/compilation               29m25s  16GB
Aug 31 18:45:42 Starting candle/standard/opentheory/compilation/proofs
Aug 31 18:46:16 Finished candle/standard/opentheory/compilation/proofs           33s   3GB
Aug 31 18:46:16 Starting characteristic/examples
Aug 31 18:47:40 Finished characteristic/examples                               1m23s   2GB
Aug 31 18:47:41 Starting tutorial/solutions
Aug 31 19:00:50 Finished tutorial/solutions                                   13m09s   6GB
Aug 31 19:00:50 Starting translator/monadic/examples
Aug 31 19:03:47 Finished translator/monadic/examples                           2m55s   2GB
Aug 31 19:03:47 Starting examples
Aug 31 19:12:38 Finished examples                                              8m50s   3GB
Aug 31 19:12:39 Starting examples/compilation/x64
Aug 31 21:18:33 Finished examples/compilation/x64                           2h05m53s  12GB
Aug 31 21:18:33 Starting examples/compilation/x64/proofs
Aug 31 21:20:00 Finished examples/compilation/x64/proofs                       1m25s   2GB
Aug 31 21:20:00 Starting examples/compilation/ag32
Aug 31 21:48:34 Finished examples/compilation/ag32                            28m33s   5GB
Aug 31 21:48:35 Starting examples/compilation/ag32/proofs
Aug 31 21:49:32 Finished examples/compilation/ag32/proofs                        57s   3GB
Aug 31 21:49:33 Starting translator/okasaki-examples
Aug 31 21:53:37 Finished translator/okasaki-examples                           4m04s   2GB
Aug 31 21:53:38 Starting translator/other-examples
Aug 31 21:56:59 Finished translator/other-examples                             3m20s   1GB
Aug 31 21:56:59 Starting compiler/parsing/tests
Aug 31 21:57:24 Finished compiler/parsing/tests                                  23s 561MB
Aug 31 21:57:24 Starting compiler/inference/tests
Aug 31 22:01:36 Finished compiler/inference/tests                              4m11s   5GB
Aug 31 22:01:36 Starting compiler/bootstrap/translation
Sep 01 00:31:37 Finished compiler/bootstrap/translation                     2h30m00s  38GB
Sep 01 00:31:37 Starting unverified/sexpr-bootstrap/x64/64
Sep 01 00:44:19 Finished unverified/sexpr-bootstrap/x64/64                    12m41s   3GB
Sep 01 00:44:19 Starting unverified/sexpr-bootstrap/x64/32
Sep 01 00:53:09 Finished unverified/sexpr-bootstrap/x64/32                     8m48s   6GB
Sep 01 00:53:09 Starting compiler/benchmarks
Sep 01 01:31:32 Finished compiler/benchmarks                                  38m22s   2GB
Sep 01 01:31:32 Starting compiler/bootstrap/compilation/x64/64
Sep 01 13:59:23 Finished compiler/bootstrap/compilation/x64/64             12h27m49s  64GB
Sep 01 13:59:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 01 14:02:19 Finished compiler/bootstrap/compilation/x64/64/proofs          2m55s  11GB
Sep 01 14:02:19 Starting compiler/bootstrap/compilation/x64/32
Sep 02 01:27:37 Finished compiler/bootstrap/compilation/x64/32             11h25m16s  64GB
Sep 02 01:27:37 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 02 01:31:09 Finished compiler/bootstrap/compilation/x64/32/proofs          3m31s   5GB
Sep 02 01:31:09 Starting compiler/bootstrap/compilation/ag32/32
Sep 02 13:57:39 Finished compiler/bootstrap/compilation/ag32/32            12h26m29s  63GB
Sep 02 13:57:40 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 02 14:16:42 Finished compiler/bootstrap/compilation/ag32/32/proofs        19m01s  18GB
Sep 02 14:16:42 SUCCESS