Job 153

CakeML:399781715601ee8b2b6faec7362c31cc6e40fc68
  Define sub_nocheck and add it to the translator [Jan 12 08:30:31]
HOL:bd59c5b8d4dc95f104c695ea4dbf766d27bc347f
  Test-case illustrating a current bug in Holmake [Jan 12 04:56:34]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux
Artefacts:cake-x64-32.tar.gz
cake-x64-64.tar.gz

Jan 12 13:52:04 Claimed job
Jan 12 13:52:14 Building HOL
Jan 12 14:04:51 Starting semantics/ffi
Jan 12 14:06:00 Finished semantics/ffi                                         1m06s 390MB
Jan 12 14:06:02 Starting semantics
Jan 12 14:08:42 Finished semantics                                             2m37s   1GB
Jan 12 14:08:44 Starting semantics/proofs
Jan 12 14:12:20 Finished semantics/proofs                                      3m34s   1GB
Jan 12 14:12:22 Starting basis/pure
Jan 12 14:18:26 Finished basis/pure                                            6m01s 641MB
Jan 12 14:18:28 Starting translator
Jan 12 14:25:37 Finished translator                                            7m06s   1GB
Jan 12 14:25:39 Starting compiler/parsing
Jan 12 14:28:03 Finished compiler/parsing                                      2m22s   1GB
Jan 12 14:28:05 Starting characteristic
Jan 12 14:32:49 Finished characteristic                                        4m41s   1GB
Jan 12 14:32:51 Starting basis
Jan 12 14:59:21 Finished basis                                                26m28s   2GB
Jan 12 14:59:23 Starting translator/monadic
Jan 12 15:02:48 Finished translator/monadic                                    3m22s 990MB
Jan 12 15:02:50 Starting compiler/inference
Jan 12 15:05:43 Finished compiler/inference                                    2m50s   1GB
Jan 12 15:05:45 Starting compiler/backend/reg_alloc
Jan 12 15:06:35 Finished compiler/backend/reg_alloc                              48s 813MB
Jan 12 15:06:37 Starting compiler/backend/gc
Jan 12 15:22:44 Finished compiler/backend/gc                                  16m05s   3GB
Jan 12 15:22:46 Starting compiler/backend
Jan 12 15:22:50 Finished compiler/backend                                         1s  16MB
Jan 12 15:22:52 Starting compiler/encoders/asm
Jan 12 15:22:54 Finished compiler/encoders/asm                                    0s  12MB
Jan 12 15:22:56 Starting compiler/encoders/x64
Jan 12 15:24:36 Finished compiler/encoders/x64                                 1m38s 447MB
Jan 12 15:24:38 Starting compiler/encoders/arm6
Jan 12 15:27:49 Finished compiler/encoders/arm6                                3m09s   1GB
Jan 12 15:27:51 Starting compiler/encoders/arm8
Jan 12 15:28:42 Finished compiler/encoders/arm8                                  48s 392MB
Jan 12 15:28:44 Starting compiler/encoders/mips
Jan 12 15:30:11 Finished compiler/encoders/mips                                1m25s 657MB
Jan 12 15:30:13 Starting compiler/encoders/riscv
Jan 12 15:31:49 Finished compiler/encoders/riscv                               1m33s 424MB
Jan 12 15:31:51 Starting compiler/backend/x64
Jan 12 15:32:35 Finished compiler/backend/x64                                    42s   1GB
Jan 12 15:32:37 Starting compiler/backend/arm6
Jan 12 15:33:27 Finished compiler/backend/arm6                                   47s   1GB
Jan 12 15:33:29 Starting compiler/backend/arm8
Jan 12 15:34:14 Finished compiler/backend/arm8                                   43s   1GB
Jan 12 15:34:16 Starting compiler/backend/mips
Jan 12 15:35:02 Finished compiler/backend/mips                                   43s   1GB
Jan 12 15:35:04 Starting compiler/backend/riscv
Jan 12 15:35:50 Finished compiler/backend/riscv                                  43s   1GB
Jan 12 15:35:52 Starting compiler/parsing/proofs
Jan 12 15:40:35 Finished compiler/parsing/proofs                               4m41s 774MB
Jan 12 15:40:37 Starting compiler/inference/proofs
Jan 12 15:45:02 Finished compiler/inference/proofs                             4m22s   1GB
Jan 12 15:45:04 Starting compiler/backend/semantics
Jan 12 16:04:13 Finished compiler/backend/semantics                           19m07s   2GB
Jan 12 16:04:15 Starting compiler/backend/reg_alloc/proofs
Jan 12 16:05:31 Finished compiler/backend/reg_alloc/proofs                     1m14s 546MB
Jan 12 16:05:33 Starting compiler/backend/proofs
Jan 12 17:15:06 Finished compiler/backend/proofs                            1h09m30s   5GB
Jan 12 17:15:08 Starting compiler/encoders/x64/proofs
Jan 12 17:28:50 Finished compiler/encoders/x64/proofs                         13m39s   1GB
Jan 12 17:28:52 Starting compiler/encoders/arm6/proofs
Jan 12 17:42:40 Finished compiler/encoders/arm6/proofs                        13m46s   3GB
Jan 12 17:42:42 Starting compiler/encoders/arm8/proofs
Jan 12 17:52:09 Finished compiler/encoders/arm8/proofs                         9m24s   1GB
Jan 12 17:52:11 Starting compiler/encoders/mips/proofs
Jan 12 18:05:04 Finished compiler/encoders/mips/proofs                        12m50s   1GB
Jan 12 18:05:06 Starting compiler/encoders/riscv/proofs
Jan 12 18:19:00 Finished compiler/encoders/riscv/proofs                       13m52s 913MB
Jan 12 18:19:02 Starting compiler/backend/x64/proofs
Jan 12 18:19:56 Finished compiler/backend/x64/proofs                             52s   1GB
Jan 12 18:19:58 Starting compiler/backend/arm6/proofs
Jan 12 18:20:58 Finished compiler/backend/arm6/proofs                            57s   1GB
Jan 12 18:21:00 Starting compiler/backend/arm8/proofs
Jan 12 18:21:54 Finished compiler/backend/arm8/proofs                            51s   1GB
Jan 12 18:21:56 Starting compiler/backend/mips/proofs
Jan 12 18:22:50 Finished compiler/backend/mips/proofs                            52s   1GB
Jan 12 18:22:52 Starting compiler/backend/riscv/proofs
Jan 12 18:23:47 Finished compiler/backend/riscv/proofs                           52s   1GB
Jan 12 18:23:48 Starting compiler/proofs
Jan 12 18:26:25 Finished compiler/proofs                                       2m34s   1GB
Jan 12 18:26:27 Starting candle/set-theory
Jan 12 18:28:09 Finished candle/set-theory                                     1m39s 592MB
Jan 12 18:28:11 Starting candle/syntax-lib
Jan 12 18:28:32 Finished candle/syntax-lib                                       19s 586MB
Jan 12 18:28:34 Starting candle/standard/syntax
Jan 12 18:31:32 Finished candle/standard/syntax                                2m56s 838MB
Jan 12 18:31:34 Starting candle/standard/semantics
Jan 12 18:34:00 Finished candle/standard/semantics                             2m24s 927MB
Jan 12 18:34:02 Starting candle/standard/monadic
Jan 12 18:36:46 Finished candle/standard/monadic                               2m41s 826MB
Jan 12 18:36:48 Starting candle/standard/ml_kernel
Jan 12 18:47:50 Finished candle/standard/ml_kernel                            11m00s   1GB
Jan 12 18:47:52 Starting candle/standard/opentheory
Jan 12 18:48:24 Finished candle/standard/opentheory                              30s 613MB
Jan 12 18:48:26 Starting characteristic/examples
Jan 12 18:50:42 Finished characteristic/examples                               2m14s   1GB
Jan 12 18:50:44 Starting tutorial/solutions
Jan 12 19:26:55 Finished tutorial/solutions                                   36m08s  11GB
Jan 12 19:26:57 Starting translator/monadic/examples
Jan 12 19:29:22 Finished translator/monadic/examples                           2m23s   1GB
Jan 12 19:29:24 Starting examples
Jan 12 19:37:06 Finished examples                                              7m39s   1GB
Jan 12 19:37:08 Starting examples/compilation
Jan 13 00:48:53 Finished examples/compilation                               5h11m43s  15GB
Jan 13 00:48:55 Starting examples/compilation/proofs
Jan 13 00:54:26 Finished examples/compilation/proofs                           5m28s   3GB
Jan 13 00:54:28 Starting compiler/benchmarks
Jan 13 00:54:30 Finished compiler/benchmarks                                      0s   6MB
Jan 13 00:54:32 Starting translator/okasaki-examples
Jan 13 01:01:55 Finished translator/okasaki-examples                           7m21s   1GB
Jan 13 01:01:57 Starting translator/other-examples
Jan 13 01:08:49 Finished translator/other-examples                             6m49s   1GB
Jan 13 01:08:51 Starting compiler/parsing/tests
Jan 13 01:09:32 Finished compiler/parsing/tests                                  39s 371MB
Jan 13 01:09:34 Starting compiler/bootstrap/translation
Jan 13 09:46:45 Finished compiler/bootstrap/translation                     8h37m08s  43GB
Jan 13 09:46:47 Starting compiler/bootstrap/compilation/x64/64
Jan 14 13:57:37 Finished compiler/bootstrap/compilation/x64/64             28h10m47s  96GB
Jan 14 13:57:39 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 14 14:02:42 Finished compiler/bootstrap/compilation/x64/64/proofs          5m00s  21GB
Jan 14 14:02:44 Starting compiler/bootstrap/compilation/x64/32
Jan 15 12:25:25 Finished compiler/bootstrap/compilation/x64/32             22h22m38s  88GB
Jan 15 12:25:27 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 15 12:28:42 Finished compiler/bootstrap/compilation/x64/32/proofs          3m13s  25GB
Jan 15 12:28:44 SUCCESS