Job 466

CakeML:f6d8ed2ee71091a75c6c7c634490380e8abe11a9
  Fix typo [Aug 28 07:46:30]
HOL:cc8f983f09c21e413738c986d6ce54b256e8feef
  Promote more functions from Isabelle Library into Portable [Aug 30 02:04:45]
Machine:cakeml1798 4.4.0-98-generic x86_64 GNU/Linux
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz

Aug 30 15:34:36 Claimed job
Aug 30 15:34:48 Building HOL
Aug 30 15:48:23 Starting developers/bin
Aug 30 15:48:34 Finished developers/bin                                           9s 144MB
Aug 30 15:48:36 Starting semantics/ffi
Aug 30 15:49:37 Finished semantics/ffi                                           58s 302MB
Aug 30 15:49:39 Starting semantics
Aug 30 15:52:01 Finished semantics                                             2m20s 858MB
Aug 30 15:52:03 Starting semantics/proofs
Aug 30 15:57:13 Finished semantics/proofs                                      5m08s   1GB
Aug 30 15:57:15 Starting basis/pure
Aug 30 16:03:04 Finished basis/pure                                            5m46s 648MB
Aug 30 16:03:06 Starting translator
Aug 30 16:05:04 Finished translator                                            1m55s 854MB
Aug 30 16:05:06 Starting compiler/parsing
Aug 30 16:07:28 Finished compiler/parsing                                      2m20s   2GB
Aug 30 16:07:30 Starting characteristic
Aug 30 16:12:04 Finished characteristic                                        4m31s   1GB
Aug 30 16:12:06 Starting translator/monadic
Aug 30 16:14:48 Finished translator/monadic                                    2m40s   1GB
Aug 30 16:14:50 Starting basis
Aug 30 16:42:47 Finished basis                                                27m54s   3GB
Aug 30 16:42:49 Starting compiler/inference
Aug 30 16:45:36 Finished compiler/inference                                    2m45s   1GB
Aug 30 16:45:38 Starting compiler/backend/reg_alloc
Aug 30 16:47:00 Finished compiler/backend/reg_alloc                            1m19s   1GB
Aug 30 16:47:02 Starting compiler/backend/gc
Aug 30 17:01:51 Finished compiler/backend/gc                                  14m47s   3GB
Aug 30 17:01:53 Starting compiler/backend
Aug 30 17:01:58 Finished compiler/backend                                         3s  20MB
Aug 30 17:02:00 Starting compiler/encoders/asm
Aug 30 17:02:03 Finished compiler/encoders/asm                                    0s  16MB
Aug 30 17:02:05 Starting compiler/encoders/x64
Aug 30 17:03:34 Finished compiler/encoders/x64                                 1m26s 506MB
Aug 30 17:03:36 Starting compiler/encoders/arm6
Aug 30 17:06:34 Finished compiler/encoders/arm6                                2m55s   1GB
Aug 30 17:06:36 Starting compiler/encoders/arm8
Aug 30 17:07:21 Finished compiler/encoders/arm8                                  42s 364MB
Aug 30 17:07:22 Starting compiler/encoders/mips
Aug 30 17:08:59 Finished compiler/encoders/mips                                1m34s 865MB
Aug 30 17:09:01 Starting compiler/encoders/riscv
Aug 30 17:10:36 Finished compiler/encoders/riscv                               1m32s 716MB
Aug 30 17:10:38 Starting compiler/backend/x64
Aug 30 17:11:11 Finished compiler/backend/x64                                    30s   1GB
Aug 30 17:11:13 Starting compiler/backend/arm6
Aug 30 17:11:47 Finished compiler/backend/arm6                                   32s   1GB
Aug 30 17:11:49 Starting compiler/backend/arm8
Aug 30 17:12:21 Finished compiler/backend/arm8                                   29s   1GB
Aug 30 17:12:22 Starting compiler/backend/mips
Aug 30 17:12:58 Finished compiler/backend/mips                                   34s 895MB
Aug 30 17:13:00 Starting compiler/backend/riscv
Aug 30 17:13:34 Finished compiler/backend/riscv                                  31s   1GB
Aug 30 17:13:36 Starting compiler/parsing/proofs
Aug 30 17:17:37 Finished compiler/parsing/proofs                               3m58s 785MB
Aug 30 17:17:39 Starting compiler/inference/proofs
Aug 30 17:22:28 Finished compiler/inference/proofs                             4m47s   1GB
Aug 30 17:22:30 Starting compiler/backend/semantics
Aug 30 17:37:05 Finished compiler/backend/semantics                           14m32s   2GB
Aug 30 17:37:07 Starting compiler/backend/reg_alloc/proofs
Aug 30 17:48:56 Finished compiler/backend/reg_alloc/proofs                    11m46s 520MB
Aug 30 17:48:58 Starting compiler/backend/proofs
Aug 30 18:44:25 Finished compiler/backend/proofs                              55m24s   3GB
Aug 30 18:44:27 Starting compiler/encoders/x64/proofs
Aug 30 18:56:13 Finished compiler/encoders/x64/proofs                         11m41s   1GB
Aug 30 18:56:15 Starting compiler/encoders/arm6/proofs
Aug 30 19:08:18 Finished compiler/encoders/arm6/proofs                        12m01s   3GB
Aug 30 19:08:20 Starting compiler/encoders/arm8/proofs
Aug 30 19:16:41 Finished compiler/encoders/arm8/proofs                         8m18s   1GB
Aug 30 19:16:43 Starting compiler/encoders/mips/proofs
Aug 30 19:28:28 Finished compiler/encoders/mips/proofs                        11m42s   1GB
Aug 30 19:28:30 Starting compiler/encoders/riscv/proofs
Aug 30 19:41:05 Finished compiler/encoders/riscv/proofs                       12m33s   1GB
Aug 30 19:41:07 Starting compiler/backend/x64/proofs
Aug 30 19:41:43 Finished compiler/backend/x64/proofs                             33s   1GB
Aug 30 19:41:45 Starting compiler/backend/arm6/proofs
Aug 30 19:42:24 Finished compiler/backend/arm6/proofs                            37s   1GB
Aug 30 19:42:26 Starting compiler/backend/arm8/proofs
Aug 30 19:43:02 Finished compiler/backend/arm8/proofs                            33s   1GB
Aug 30 19:43:04 Starting compiler/backend/mips/proofs
Aug 30 19:43:40 Finished compiler/backend/mips/proofs                            33s   1GB
Aug 30 19:43:42 Starting compiler/backend/riscv/proofs
Aug 30 19:44:17 Finished compiler/backend/riscv/proofs                           33s   1GB
Aug 30 19:44:19 Starting compiler/proofs
Aug 30 19:46:44 Finished compiler/proofs                                       2m22s   2GB
Aug 30 19:46:47 Starting candle/set-theory
Aug 30 19:47:42 Finished candle/set-theory                                       52s 548MB
Aug 30 19:47:44 Starting candle/syntax-lib
Aug 30 19:48:03 Finished candle/syntax-lib                                       16s 554MB
Aug 30 19:48:06 Starting candle/standard/syntax
Aug 30 19:50:48 Finished candle/standard/syntax                                2m40s 529MB
Aug 30 19:50:50 Starting candle/standard/semantics
Aug 30 19:53:07 Finished candle/standard/semantics                             2m13s 899MB
Aug 30 19:53:09 Starting candle/standard/monadic
Aug 30 19:55:43 Finished candle/standard/monadic                               2m32s   1GB
Aug 30 19:55:45 Starting candle/standard/ml_kernel
Aug 30 20:20:03 Finished candle/standard/ml_kernel                            24m16s   3GB
Aug 30 20:20:06 Starting candle/standard/opentheory
Aug 30 20:34:50 Finished candle/standard/opentheory                           14m42s   4GB
Aug 30 20:34:52 Starting characteristic/examples
Aug 30 20:37:34 Finished characteristic/examples                               2m40s   1GB
Aug 30 20:37:36 Starting tutorial/solutions
Aug 30 20:58:20 Finished tutorial/solutions                                   20m41s   9GB
Aug 30 20:58:22 Starting translator/monadic/examples
Aug 30 21:01:06 Finished translator/monadic/examples                           2m42s   2GB
Aug 30 21:01:09 Starting examples
Aug 30 21:09:14 Finished examples                                              8m03s   2GB
Aug 30 21:09:16 Starting examples/compilation
Aug 31 00:04:13 Finished examples/compilation                               2h54m53s   8GB
Aug 31 00:04:15 Starting examples/compilation/proofs
Aug 31 00:07:47 Finished examples/compilation/proofs                           3m30s   2GB
Aug 31 00:07:49 Starting compiler/benchmarks
Aug 31 00:07:52 Finished compiler/benchmarks                                      0s   4MB
Aug 31 00:07:54 Starting translator/okasaki-examples
Aug 31 00:14:19 Finished translator/okasaki-examples                           6m22s   1GB
Aug 31 00:14:21 Starting translator/other-examples
Aug 31 00:21:05 Finished translator/other-examples                             6m42s   1GB
Aug 31 00:21:08 Starting compiler/parsing/tests
Aug 31 00:21:49 Finished compiler/parsing/tests                                  39s 353MB
Aug 31 00:21:51 Starting compiler/inference/tests
Aug 31 00:28:02 Finished compiler/inference/tests                              6m09s   4GB
Aug 31 00:28:04 Starting compiler/bootstrap/translation
Aug 31 08:29:44 Finished compiler/bootstrap/translation                     8h01m36s  70GB
Aug 31 08:29:46 Starting unverified/sexpr-bootstrap/x64/64
Aug 31 08:36:16 Finished unverified/sexpr-bootstrap/x64/64                     6m24s  12GB
Aug 31 08:36:18 Starting unverified/sexpr-bootstrap/x64/32
Aug 31 08:40:03 Finished unverified/sexpr-bootstrap/x64/32                     3m39s  13GB
Aug 31 08:40:05 Starting compiler/bootstrap/compilation/x64/64 Aug 31 08:40:05 62137s