Job 165

CakeML:f8dd05aea6320bbd612745b9edc67b48646124a3
  Update diffTheory to use mlnumTheory [Jan 19 16:44:16]
HOL:8da85ad615f3f14a7db120e68d75138b6101bedb
  holyhammer: fix error by matching the changes in hhsPredict [Jan 18 23:08:13]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 19 22:14:16 Claimed job
Jan 19 22:14:24 Building HOL
Jan 19 22:27:00 Starting semantics/ffi
Jan 19 22:28:09 Finished semantics/ffi                                         1m07s 548MB
Jan 19 22:28:11 Starting semantics
Jan 19 22:30:52 Finished semantics                                             2m38s   1GB
Jan 19 22:30:53 Starting semantics/proofs
Jan 19 22:34:28 Finished semantics/proofs                                      3m32s   1GB
Jan 19 22:34:30 Starting basis/pure
Jan 19 22:40:43 Finished basis/pure                                            6m10s 802MB
Jan 19 22:40:45 Starting translator
Jan 19 22:47:49 Finished translator                                            7m02s   1GB
Jan 19 22:47:51 Starting compiler/parsing
Jan 19 22:50:14 Finished compiler/parsing                                      2m21s   1GB
Jan 19 22:50:16 Starting characteristic
Jan 19 22:55:05 Finished characteristic                                        4m46s   2GB
Jan 19 22:55:07 Starting basis
Jan 19 23:25:37 Finished basis                                                30m28s   2GB
Jan 19 23:25:39 Starting translator/monadic
Jan 19 23:29:06 Finished translator/monadic                                    3m24s   1GB
Jan 19 23:29:08 Starting compiler/inference
Jan 19 23:32:02 Finished compiler/inference                                    2m51s   1GB
Jan 19 23:32:04 Starting compiler/backend/reg_alloc
Jan 19 23:32:53 Finished compiler/backend/reg_alloc                              47s 885MB
Jan 19 23:32:55 Starting compiler/backend/gc
Jan 19 23:48:57 Finished compiler/backend/gc                                  15m59s   2GB
Jan 19 23:48:59 Starting compiler/backend
Jan 19 23:49:03 Finished compiler/backend                                         1s  17MB
Jan 19 23:49:05 Starting compiler/encoders/asm
Jan 19 23:49:07 Finished compiler/encoders/asm                                    0s  16MB
Jan 19 23:49:09 Starting compiler/encoders/x64
Jan 19 23:50:49 Finished compiler/encoders/x64                                 1m37s 433MB
Jan 19 23:50:51 Starting compiler/encoders/arm6
Jan 19 23:54:02 Finished compiler/encoders/arm6                                3m08s   1GB
Jan 19 23:54:04 Starting compiler/encoders/arm8
Jan 19 23:54:53 Finished compiler/encoders/arm8                                  47s 409MB
Jan 19 23:54:55 Starting compiler/encoders/mips
Jan 19 23:56:22 Finished compiler/encoders/mips                                1m24s 615MB
Jan 19 23:56:23 Starting compiler/encoders/riscv
Jan 19 23:57:56 Finished compiler/encoders/riscv                               1m30s 450MB
Jan 19 23:57:58 Starting compiler/backend/x64
Jan 19 23:58:40 Finished compiler/backend/x64                                    39s 849MB
Jan 19 23:58:42 Starting compiler/backend/arm6
Jan 19 23:59:28 Finished compiler/backend/arm6                                   44s   1GB
Jan 19 23:59:30 Starting compiler/backend/arm8
Jan 20 00:00:12 Finished compiler/backend/arm8                                   39s 928MB
Jan 20 00:00:14 Starting compiler/backend/mips
Jan 20 00:00:57 Finished compiler/backend/mips                                   41s   1GB
Jan 20 00:00:59 Starting compiler/backend/riscv
Jan 20 00:01:42 Finished compiler/backend/riscv                                  40s 945MB
Jan 20 00:01:44 Starting compiler/parsing/proofs
Jan 20 00:06:16 Finished compiler/parsing/proofs                               4m30s 858MB
Jan 20 00:06:17 Starting compiler/inference/proofs
Jan 20 00:10:38 Finished compiler/inference/proofs                             4m18s   1GB
Jan 20 00:10:40 Starting compiler/backend/semantics
Jan 20 00:29:36 Finished compiler/backend/semantics                           18m53s   3GB
Jan 20 00:29:38 Starting compiler/backend/reg_alloc/proofs
Jan 20 00:30:53 Finished compiler/backend/reg_alloc/proofs                     1m12s 401MB
Jan 20 00:30:55 Starting compiler/backend/proofs
Jan 20 01:40:51 Finished compiler/backend/proofs                            1h09m54s   4GB
Jan 20 01:40:53 Starting compiler/encoders/x64/proofs
Jan 20 01:54:35 Finished compiler/encoders/x64/proofs                         13m39s   1GB
Jan 20 01:54:37 Starting compiler/encoders/arm6/proofs
Jan 20 02:08:11 Finished compiler/encoders/arm6/proofs                        13m32s   3GB
Jan 20 02:08:12 Starting compiler/encoders/arm8/proofs
Jan 20 02:17:32 Finished compiler/encoders/arm8/proofs                         9m17s   1GB
Jan 20 02:17:34 Starting compiler/encoders/mips/proofs
Jan 20 02:30:35 Finished compiler/encoders/mips/proofs                        12m59s   1GB
Jan 20 02:30:37 Starting compiler/encoders/riscv/proofs
Jan 20 02:44:37 Finished compiler/encoders/riscv/proofs                       13m57s 913MB
Jan 20 02:44:39 Starting compiler/backend/x64/proofs
Jan 20 02:45:31 Finished compiler/backend/x64/proofs                             50s   1GB
Jan 20 02:45:33 Starting compiler/backend/arm6/proofs
Jan 20 02:46:32 Finished compiler/backend/arm6/proofs                            56s   1GB
Jan 20 02:46:34 Starting compiler/backend/arm8/proofs
Jan 20 02:47:26 Finished compiler/backend/arm8/proofs                            50s   1GB
Jan 20 02:47:28 Starting compiler/backend/mips/proofs
Jan 20 02:48:23 Finished compiler/backend/mips/proofs                            52s   1GB
Jan 20 02:48:25 Starting compiler/backend/riscv/proofs
Jan 20 02:49:20 Finished compiler/backend/riscv/proofs                           51s   1GB
Jan 20 02:49:22 Starting compiler/proofs
Jan 20 02:52:10 Finished compiler/proofs                                       2m46s   2GB
Jan 20 02:52:12 Starting candle/set-theory
Jan 20 02:53:55 Finished candle/set-theory                                     1m41s 584MB
Jan 20 02:53:57 Starting candle/syntax-lib
Jan 20 02:54:19 Finished candle/syntax-lib                                       19s 552MB
Jan 20 02:54:21 Starting candle/standard/syntax
Jan 20 02:57:22 Finished candle/standard/syntax                                2m58s 623MB
Jan 20 02:57:24 Starting candle/standard/semantics
Jan 20 02:59:53 Finished candle/standard/semantics                             2m26s 730MB
Jan 20 02:59:54 Starting candle/standard/monadic
Jan 20 03:02:40 Finished candle/standard/monadic                               2m43s 819MB
Jan 20 03:02:42 Starting candle/standard/ml_kernel
Jan 20 03:13:46 Finished candle/standard/ml_kernel                            11m01s   2GB
Jan 20 03:13:48 Starting candle/standard/opentheory
Jan 20 03:14:19 Finished candle/standard/opentheory                              29s 613MB
Jan 20 03:14:21 Starting characteristic/examples
Jan 20 03:16:58 Finished characteristic/examples                               2m35s   1GB
Jan 20 03:17:00 Starting tutorial/solutions
Jan 20 03:55:36 Finished tutorial/solutions                                   38m32s  11GB
Jan 20 03:55:37 Starting translator/monadic/examples
Jan 20 03:58:03 Finished translator/monadic/examples                           2m23s   1GB
Jan 20 03:58:05 Starting examples
Jan 20 04:06:23 Finished examples                                              8m16s   2GB
Jan 20 04:06:25 Starting examples/compilation
Jan 20 10:15:15 Finished examples/compilation                               6h08m47s  29GB
Jan 20 10:15:16 Starting examples/compilation/proofs
Jan 20 10:21:18 Finished examples/compilation/proofs                           5m59s   4GB
Jan 20 10:21:20 Starting compiler/benchmarks
Jan 20 10:21:22 Finished compiler/benchmarks                                      0s   4MB
Jan 20 10:21:24 Starting translator/okasaki-examples
Jan 20 10:28:46 Finished translator/okasaki-examples                           7m20s   1GB
Jan 20 10:28:48 Starting translator/other-examples
Jan 20 10:35:46 Finished translator/other-examples                             6m56s   1GB
Jan 20 10:35:48 Starting compiler/parsing/tests
Jan 20 10:36:30 Finished compiler/parsing/tests                                  40s 364MB
Jan 20 10:36:32 Starting compiler/bootstrap/translation
Jan 20 19:27:16 Finished compiler/bootstrap/translation                     8h50m42s  51GB
Jan 20 19:27:18 Starting compiler/bootstrap/compilation/x64/64
Jan 22 10:41:52 Finished compiler/bootstrap/compilation/x64/64             39h14m31s  85GB
Jan 22 10:41:54 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 22 10:46:01 Finished compiler/bootstrap/compilation/x64/64/proofs          4m04s  30GB
Jan 22 10:46:03 Starting compiler/bootstrap/compilation/x64/32
Jan 23 18:41:15 Finished compiler/bootstrap/compilation/x64/32             31h55m09s  85GB
Jan 23 18:41:17 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 23 18:45:42 Finished compiler/bootstrap/compilation/x64/32/proofs          4m23s  33GB
Jan 23 18:45:44 SUCCESS