Job 837

CakeML:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:7b9343ee31f1202a7efd349e7ff291eef8311133
  Document some changes to emacs mode [May 03 00:36:20]
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 06 02:02:27 Claimed job
May 06 02:02:32 Building HOL
May 06 02:17:48 Starting developers
May 06 02:17:50 Finished developers                                               1s  32MB
May 06 02:17:50 Starting developers/bin
May 06 02:17:59 Finished developers/bin                                           8s 927MB
May 06 02:17:59 Starting semantics/ffi
May 06 02:19:10 Finished semantics/ffi                                         1m10s 532MB
May 06 02:19:10 Starting semantics
May 06 02:22:04 Finished semantics                                             2m53s   1GB
May 06 02:22:04 Starting semantics/proofs
May 06 02:27:55 Finished semantics/proofs                                      5m51s   1GB
May 06 02:27:55 Starting basis/pure
May 06 02:34:47 Finished basis/pure                                            6m51s 657MB
May 06 02:34:47 Starting translator
May 06 02:38:00 Finished translator                                            3m13s   1GB
May 06 02:38:01 Starting compiler/parsing
May 06 02:39:57 Finished compiler/parsing                                      1m56s   1GB
May 06 02:39:58 Starting characteristic
May 06 02:50:13 Finished characteristic                                       10m15s   2GB
May 06 02:50:13 Starting translator/monadic
May 06 02:52:57 Finished translator/monadic                                    2m43s   1GB
May 06 02:52:58 Starting basis
May 06 03:25:05 Finished basis                                                32m06s   2GB
May 06 03:25:05 Starting compiler/inference
May 06 03:28:49 Finished compiler/inference                                    3m44s   1GB
May 06 03:28:50 Starting compiler/backend/reg_alloc
May 06 03:30:26 Finished compiler/backend/reg_alloc                            1m36s   1GB
May 06 03:30:26 Starting compiler/backend/gc
May 06 03:46:57 Finished compiler/backend/gc                                  16m30s   2GB
May 06 03:46:57 Starting compiler/backend
May 06 03:47:05 Finished compiler/backend                                         8s 304MB
May 06 03:47:06 Starting compiler/encoders/asm
May 06 03:47:07 Finished compiler/encoders/asm                                    0s  29MB
May 06 03:47:07 Starting compiler/encoders/x64
May 06 03:49:00 Finished compiler/encoders/x64                                 1m53s 862MB
May 06 03:49:01 Starting compiler/encoders/arm6
May 06 03:52:37 Finished compiler/encoders/arm6                                3m36s   2GB
May 06 03:52:38 Starting compiler/encoders/arm8
May 06 03:53:41 Finished compiler/encoders/arm8                                1m03s 913MB
May 06 03:53:41 Starting compiler/encoders/mips
May 06 03:55:56 Finished compiler/encoders/mips                                2m14s   1GB
May 06 03:55:56 Starting compiler/encoders/riscv
May 06 03:58:31 Finished compiler/encoders/riscv                               2m35s   1GB
May 06 03:58:32 Starting compiler/encoders/ag32
May 06 03:59:02 Finished compiler/encoders/ag32                                  30s 644MB
May 06 03:59:02 Starting compiler/backend/x64
May 06 03:59:37 Finished compiler/backend/x64                                    34s 850MB
May 06 03:59:37 Starting compiler/backend/arm6
May 06 04:00:18 Finished compiler/backend/arm6                                   40s   1GB
May 06 04:00:18 Starting compiler/backend/arm8
May 06 04:00:58 Finished compiler/backend/arm8                                   39s   1GB
May 06 04:00:59 Starting compiler/backend/mips
May 06 04:01:37 Finished compiler/backend/mips                                   38s   1GB
May 06 04:01:37 Starting compiler/backend/riscv
May 06 04:02:15 Finished compiler/backend/riscv                                  37s   1GB
May 06 04:02:15 Starting compiler/backend/ag32
May 06 04:04:28 Finished compiler/backend/ag32                                 2m12s   1GB
May 06 04:04:28 Starting compiler/parsing/proofs
May 06 04:14:56 Finished compiler/parsing/proofs                              10m27s   1GB
May 06 04:14:57 Starting compiler/inference/proofs
May 06 04:20:23 Finished compiler/inference/proofs                             5m26s   1GB
May 06 04:20:23 Starting compiler/backend/semantics
May 06 04:33:47 Finished compiler/backend/semantics                           13m23s   2GB
May 06 04:33:48 Starting compiler/backend/reg_alloc/proofs
May 06 04:40:55 Finished compiler/backend/reg_alloc/proofs                     7m07s   1GB
May 06 04:40:55 Starting compiler/backend/proofs
May 06 05:48:58 Finished compiler/backend/proofs                            1h08m02s   4GB
May 06 05:48:58 Starting compiler/encoders/x64/proofs
May 06 06:09:54 Finished compiler/encoders/x64/proofs                         20m55s   5GB
May 06 06:09:54 Starting compiler/encoders/arm6/proofs
May 06 06:37:25 Finished compiler/encoders/arm6/proofs                        27m30s   4GB
May 06 06:37:25 Starting compiler/encoders/arm8/proofs
May 06 06:50:59 Finished compiler/encoders/arm8/proofs                        13m33s   2GB
May 06 06:50:59 Starting compiler/encoders/mips/proofs
May 06 07:11:14 Finished compiler/encoders/mips/proofs                        20m14s   2GB
May 06 07:11:14 Starting compiler/encoders/riscv/proofs
May 06 07:28:14 Finished compiler/encoders/riscv/proofs                       16m59s   1GB
May 06 07:28:14 Starting compiler/encoders/ag32/proofs
May 06 07:33:13 Finished compiler/encoders/ag32/proofs                         4m58s 730MB
May 06 07:33:13 Starting compiler/backend/x64/proofs
May 06 07:33:54 Finished compiler/backend/x64/proofs                             40s   1GB
May 06 07:33:54 Starting compiler/backend/arm6/proofs
May 06 07:34:39 Finished compiler/backend/arm6/proofs                            44s 985MB
May 06 07:34:39 Starting compiler/backend/arm8/proofs
May 06 07:35:20 Finished compiler/backend/arm8/proofs                            40s   1GB
May 06 07:35:21 Starting compiler/backend/mips/proofs
May 06 07:36:01 Finished compiler/backend/mips/proofs                            40s   1GB
May 06 07:36:02 Starting compiler/backend/riscv/proofs
May 06 07:36:44 Finished compiler/backend/riscv/proofs                           41s   1GB
May 06 07:36:44 Starting compiler/backend/ag32/proofs
May 06 07:54:22 Finished compiler/backend/ag32/proofs                         17m37s   2GB
May 06 07:54:22 Starting compiler/proofs
May 06 07:56:57 Finished compiler/proofs                                       2m34s   2GB
May 06 07:56:57 Starting candle/set-theory
May 06 07:57:43 Finished candle/set-theory                                       46s 728MB
May 06 07:57:43 Starting candle/syntax-lib
May 06 07:58:08 Finished candle/syntax-lib                                       24s 583MB
May 06 07:58:09 Starting candle/standard/syntax
May 06 08:01:28 Finished candle/standard/syntax                                3m18s   1GB
May 06 08:01:28 Starting candle/standard/semantics
May 06 08:04:44 Finished candle/standard/semantics                             3m15s   1GB
May 06 08:04:44 Starting candle/standard/monadic
May 06 08:07:59 Finished candle/standard/monadic                               3m14s   1GB
May 06 08:07:59 Starting candle/standard/ml_kernel
May 06 08:15:28 Finished candle/standard/ml_kernel                             7m28s   3GB
May 06 08:15:28 Starting candle/standard/opentheory
May 06 08:32:32 Finished candle/standard/opentheory                           17m04s   3GB
May 06 08:32:33 Starting candle/standard/opentheory/compilation
May 06 09:24:51 Finished candle/standard/opentheory/compilation               52m18s  20GB
May 06 09:24:51 Starting candle/standard/opentheory/compilation/proofs
May 06 09:26:37 Finished candle/standard/opentheory/compilation/proofs         1m45s   2GB
May 06 09:26:37 Starting characteristic/examples
May 06 09:29:27 Finished characteristic/examples                               2m49s   2GB
May 06 09:29:28 Starting tutorial/solutions
May 06 09:54:30 Finished tutorial/solutions                                   25m01s   7GB
May 06 09:54:30 Starting translator/monadic/examples
May 06 09:59:04 Finished translator/monadic/examples                           4m33s   2GB
May 06 09:59:04 Starting examples
May 06 10:11:51 Finished examples                                             12m46s   4GB
May 06 10:11:51 Starting examples/compilation/x64
May 06 13:42:59 Finished examples/compilation/x64                           3h31m07s  11GB
May 06 13:42:59 Starting examples/compilation/x64/proofs
May 06 13:45:26 Finished examples/compilation/x64/proofs                       2m26s   2GB
May 06 13:45:26 Starting examples/compilation/ag32
May 06 14:38:00 Finished examples/compilation/ag32                            52m32s   7GB
May 06 14:38:00 Starting examples/compilation/ag32/proofs
May 06 14:39:33 Finished examples/compilation/ag32/proofs                      1m33s   2GB
May 06 14:39:34 Starting translator/okasaki-examples
May 06 14:47:06 Finished translator/okasaki-examples                           7m32s   1GB
May 06 14:47:06 Starting translator/other-examples
May 06 14:53:36 Finished translator/other-examples                             6m29s   1GB
May 06 14:53:36 Starting compiler/parsing/tests
May 06 14:54:21 Finished compiler/parsing/tests                                  44s 583MB
May 06 14:54:21 Starting compiler/inference/tests
May 06 15:01:38 Finished compiler/inference/tests                              7m17s   3GB
May 06 15:01:38 Starting compiler/bootstrap/translation
May 06 19:50:18 Finished compiler/bootstrap/translation                     4h48m39s  66GB
May 06 19:50:19 Starting unverified/sexpr-bootstrap/x64/64
May 06 20:01:38 Finished unverified/sexpr-bootstrap/x64/64                    11m18s   5GB
May 06 20:01:38 Starting unverified/sexpr-bootstrap/x64/32
May 06 20:09:36 Finished unverified/sexpr-bootstrap/x64/32                     7m56s   6GB
May 06 20:09:36 Starting compiler/benchmarks
May 06 20:33:15 Finished compiler/benchmarks                                  23m38s   2GB
May 06 20:33:16 Starting compiler/bootstrap/compilation/x64/64
May 07 19:54:02 Finished compiler/bootstrap/compilation/x64/64             23h20m46s 240GB
May 07 19:54:03 Starting compiler/bootstrap/compilation/x64/64/proofs
May 07 19:57:54 Finished compiler/bootstrap/compilation/x64/64/proofs          3m51s   9GB
May 07 19:57:55 Starting compiler/bootstrap/compilation/x64/32
May 08 15:26:45 Finished compiler/bootstrap/compilation/x64/32             19h28m50s 178GB
May 08 15:26:46 Starting compiler/bootstrap/compilation/x64/32/proofs
May 08 15:31:31 Finished compiler/bootstrap/compilation/x64/32/proofs          4m45s   9GB
May 08 15:31:32 Starting compiler/bootstrap/compilation/ag32/32
May 09 13:39:57 Finished compiler/bootstrap/compilation/ag32/32            22h08m24s 194GB
May 09 13:39:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 09 13:59:36 Finished compiler/bootstrap/compilation/ag32/32/proofs        19m38s  31GB
May 09 13:59:36 SUCCESS