Job 910

CakeML:38556cc97d26ac563f2b30eac5c1f3f12ff77587
  Merge pull request #657 from CakeML/fp_translation [May 30 07:20:00]
HOL:c5497b7744e02ccc95c4ac2c4f2d45bcd4ebbae0
  Allow comments inside the terms inside Definition syntax [May 30 06:38:13]
Machine:brain08 4.14.89.1.amd64-smp 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

May 30 22:39:58 Claimed job
May 30 22:40:06 Building HOL
May 30 22:55:25 Starting developers
May 30 22:55:26 Finished developers                                               1s  34MB
May 30 22:55:26 Starting developers/bin
May 30 22:55:35 Finished developers/bin                                           8s 927MB
May 30 22:55:36 Starting semantics/ffi
May 30 22:56:49 Finished semantics/ffi                                         1m12s 607MB
May 30 22:56:49 Starting semantics
May 30 22:59:45 Finished semantics                                             2m55s   1GB
May 30 22:59:45 Starting semantics/proofs
May 30 23:05:58 Finished semantics/proofs                                      6m12s   1GB
May 30 23:05:58 Starting semantics/alt_semantics
May 30 23:06:11 Finished semantics/alt_semantics                                 12s 316MB
May 30 23:06:11 Starting semantics/alt_semantics/proofs
May 30 23:09:42 Finished semantics/alt_semantics/proofs                        3m30s   1GB
May 30 23:09:42 Starting basis/pure
May 30 23:16:34 Finished basis/pure                                            6m52s 645MB
May 30 23:16:35 Starting translator
May 30 23:19:39 Finished translator                                            3m04s   1GB
May 30 23:19:39 Starting compiler/parsing
May 30 23:21:32 Finished compiler/parsing                                      1m52s   1GB
May 30 23:21:32 Starting characteristic
May 30 23:31:56 Finished characteristic                                       10m23s   2GB
May 30 23:31:56 Starting translator/monadic
May 30 23:34:37 Finished translator/monadic                                    2m40s   1GB
May 30 23:34:38 Starting basis
May 31 00:08:02 Finished basis                                                33m24s   2GB
May 31 00:08:02 Starting compiler/inference
May 31 00:11:49 Finished compiler/inference                                    3m46s   1GB
May 31 00:11:49 Starting compiler/backend/reg_alloc
May 31 00:13:28 Finished compiler/backend/reg_alloc                            1m38s   1GB
May 31 00:13:28 Starting compiler/backend/gc
May 31 00:30:14 Finished compiler/backend/gc                                  16m46s   2GB
May 31 00:30:14 Starting compiler/backend
May 31 00:30:22 Finished compiler/backend                                         7s 301MB
May 31 00:30:22 Starting compiler/encoders/asm
May 31 00:30:24 Finished compiler/encoders/asm                                    0s  26MB
May 31 00:30:24 Starting compiler/encoders/x64
May 31 00:32:22 Finished compiler/encoders/x64                                 1m58s 924MB
May 31 00:32:22 Starting compiler/encoders/arm7
May 31 00:36:03 Finished compiler/encoders/arm7                                3m40s   2GB
May 31 00:36:04 Starting compiler/encoders/arm8
May 31 00:37:10 Finished compiler/encoders/arm8                                1m05s   1GB
May 31 00:37:10 Starting compiler/encoders/mips
May 31 00:39:27 Finished compiler/encoders/mips                                2m16s   1GB
May 31 00:39:27 Starting compiler/encoders/riscv
May 31 00:42:02 Finished compiler/encoders/riscv                               2m34s   1GB
May 31 00:42:02 Starting compiler/encoders/ag32
May 31 00:42:30 Finished compiler/encoders/ag32                                  27s 789MB
May 31 00:42:30 Starting compiler/backend/x64
May 31 00:43:10 Finished compiler/backend/x64                                    39s   1GB
May 31 00:43:10 Starting compiler/backend/arm7
May 31 00:43:54 Finished compiler/backend/arm7                                   43s   1GB
May 31 00:43:54 Starting compiler/backend/arm8
May 31 00:44:34 Finished compiler/backend/arm8                                   39s   1GB
May 31 00:44:35 Starting compiler/backend/mips
May 31 00:45:12 Finished compiler/backend/mips                                   37s   1GB
May 31 00:45:13 Starting compiler/backend/riscv
May 31 00:45:51 Finished compiler/backend/riscv                                  37s 850MB
May 31 00:45:51 Starting compiler/backend/ag32
May 31 00:48:06 Finished compiler/backend/ag32                                 2m14s   1GB
May 31 00:48:07 Starting compiler/parsing/proofs
May 31 00:58:49 Finished compiler/parsing/proofs                              10m42s 950MB
May 31 00:58:49 Starting compiler/inference/proofs
May 31 01:04:25 Finished compiler/inference/proofs                             5m35s   1GB
May 31 01:04:25 Starting compiler/backend/semantics
May 31 01:17:56 Finished compiler/backend/semantics                           13m30s   1GB
May 31 01:17:56 Starting compiler/backend/reg_alloc/proofs
May 31 01:24:51 Finished compiler/backend/reg_alloc/proofs                     6m54s   1GB
May 31 01:24:52 Starting compiler/backend/proofs
May 31 02:34:19 Finished compiler/backend/proofs                            1h09m27s   5GB
May 31 02:34:20 Starting compiler/encoders/x64/proofs
May 31 02:55:29 Finished compiler/encoders/x64/proofs                         21m08s   4GB
May 31 02:55:29 Starting compiler/encoders/arm7/proofs
May 31 03:24:12 Finished compiler/encoders/arm7/proofs                        28m42s   4GB
May 31 03:24:12 Starting compiler/encoders/arm8/proofs
May 31 03:37:56 Finished compiler/encoders/arm8/proofs                        13m43s   2GB
May 31 03:37:56 Starting compiler/encoders/mips/proofs
May 31 03:58:11 Finished compiler/encoders/mips/proofs                        20m14s   2GB
May 31 03:58:11 Starting compiler/encoders/riscv/proofs
May 31 04:15:39 Finished compiler/encoders/riscv/proofs                       17m28s   1GB
May 31 04:15:39 Starting compiler/encoders/ag32/proofs
May 31 04:20:39 Finished compiler/encoders/ag32/proofs                         4m59s 930MB
May 31 04:20:40 Starting compiler/backend/x64/proofs
May 31 04:21:20 Finished compiler/backend/x64/proofs                             40s 998MB
May 31 04:21:21 Starting compiler/backend/arm7/proofs
May 31 04:22:02 Finished compiler/backend/arm7/proofs                            40s   1GB
May 31 04:22:02 Starting compiler/backend/arm8/proofs
May 31 04:22:43 Finished compiler/backend/arm8/proofs                            40s   1GB
May 31 04:22:43 Starting compiler/backend/mips/proofs
May 31 04:23:25 Finished compiler/backend/mips/proofs                            42s   1GB
May 31 04:23:26 Starting compiler/backend/riscv/proofs
May 31 04:24:06 Finished compiler/backend/riscv/proofs                           40s   1GB
May 31 04:24:07 Starting compiler/backend/ag32/proofs
May 31 04:42:11 Finished compiler/backend/ag32/proofs                         18m04s   2GB
May 31 04:42:11 Starting compiler/proofs
May 31 04:44:50 Finished compiler/proofs                                       2m38s   2GB
May 31 04:44:51 Starting candle/set-theory
May 31 04:45:36 Finished candle/set-theory                                       44s 726MB
May 31 04:45:36 Starting candle/syntax-lib
May 31 04:46:00 Finished candle/syntax-lib                                       24s 582MB
May 31 04:46:01 Starting candle/standard/syntax
May 31 04:49:24 Finished candle/standard/syntax                                3m23s   1GB
May 31 04:49:24 Starting candle/standard/semantics
May 31 04:52:37 Finished candle/standard/semantics                             3m12s   1GB
May 31 04:52:37 Starting candle/standard/monadic
May 31 04:55:47 Finished candle/standard/monadic                               3m09s   1GB
May 31 04:55:47 Starting candle/standard/ml_kernel
May 31 05:03:16 Finished candle/standard/ml_kernel                             7m28s   3GB
May 31 05:03:16 Starting candle/standard/opentheory
May 31 05:20:15 Finished candle/standard/opentheory                           16m58s   3GB
May 31 05:20:15 Starting candle/standard/opentheory/compilation
May 31 06:12:53 Finished candle/standard/opentheory/compilation               52m37s  13GB
May 31 06:12:53 Starting candle/standard/opentheory/compilation/proofs
May 31 06:14:22 Finished candle/standard/opentheory/compilation/proofs         1m28s   2GB
May 31 06:14:22 Starting characteristic/examples
May 31 06:17:06 Finished characteristic/examples                               2m43s   2GB
May 31 06:17:06 Starting tutorial/solutions
May 31 06:41:48 Finished tutorial/solutions                                   24m42s   7GB
May 31 06:41:49 Starting translator/monadic/examples
May 31 06:46:12 Finished translator/monadic/examples                           4m23s   2GB
May 31 06:46:13 Starting examples
May 31 06:59:41 Finished examples                                             13m28s   4GB
May 31 06:59:42 Starting examples/compilation/x64
May 31 10:49:51 Finished examples/compilation/x64                           3h50m09s  20GB
May 31 10:49:52 Starting examples/compilation/x64/proofs
May 31 10:52:36 Finished examples/compilation/x64/proofs                       2m43s   2GB
May 31 10:52:36 Starting examples/compilation/ag32
May 31 11:44:50 Finished examples/compilation/ag32                            52m13s   6GB
May 31 11:44:50 Starting examples/compilation/ag32/proofs
May 31 11:46:37 Finished examples/compilation/ag32/proofs                      1m46s   3GB
May 31 11:46:37 Starting translator/okasaki-examples
May 31 11:54:12 Finished translator/okasaki-examples                           7m34s   1GB
May 31 11:54:12 Starting translator/other-examples
May 31 12:01:04 Finished translator/other-examples                             6m51s   1GB
May 31 12:01:04 Starting compiler/parsing/tests
May 31 12:01:48 Finished compiler/parsing/tests                                  43s 510MB
May 31 12:01:48 Starting compiler/inference/tests
May 31 12:09:00 Finished compiler/inference/tests                              7m11s   3GB
May 31 12:09:00 Starting compiler/bootstrap/translation
May 31 16:59:03 Finished compiler/bootstrap/translation                     4h50m02s  44GB
May 31 16:59:03 Starting unverified/sexpr-bootstrap/x64/64
May 31 17:10:47 Finished unverified/sexpr-bootstrap/x64/64                    11m43s   7GB
May 31 17:10:47 Starting unverified/sexpr-bootstrap/x64/32
May 31 17:19:14 Finished unverified/sexpr-bootstrap/x64/32                     8m26s   5GB
May 31 17:19:14 Starting compiler/benchmarks
May 31 17:43:01 Finished compiler/benchmarks                                  23m47s   2GB
May 31 17:43:02 Starting compiler/bootstrap/compilation/x64/64
Jun 01 18:57:51 Finished compiler/bootstrap/compilation/x64/64             25h14m48s 307GB
Jun 01 18:57:51 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 01 19:02:07 Finished compiler/bootstrap/compilation/x64/64/proofs          4m16s   9GB
Jun 01 19:02:07 Starting compiler/bootstrap/compilation/x64/32
Jun 02 15:39:25 Finished compiler/bootstrap/compilation/x64/32             20h37m16s 253GB
Jun 02 15:39:25 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 02 15:43:35 Finished compiler/bootstrap/compilation/x64/32/proofs          4m09s  11GB
Jun 02 15:43:35 Starting compiler/bootstrap/compilation/ag32/32
Jun 03 13:37:17 Finished compiler/bootstrap/compilation/ag32/32            21h53m41s 281GB
Jun 03 13:37:17 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 03 13:57:24 Finished compiler/bootstrap/compilation/ag32/32/proofs        20m06s  31GB
Jun 03 13:57:24 SUCCESS