Job 149

CakeML:0a36d0732a78e6daf38cb0390bc931e1f4767343
  Define sub_nocheck and add it to the translator [Jan 10 03:43:06]
#428 (sub-nocheck)
Merging into:7982b740eaa616bbfc1460d03f769fe720c02716
  Support large heap+stack on x64 [Jan 11 00:19:44]
HOL:a587378e2452022aca043c008a357e9ebd67ce79
  Make experimental kernel's term representation visible to Thm [Jan 10 23:00:07]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jan 11 08:30:42 Claimed job
Jan 11 08:30:49 Reusing HOL
Jan 11 08:31:01 Starting semantics/ffi
Jan 11 08:31:23 Finished semantics/ffi                                           19s 230MB
Jan 11 08:31:25 Starting semantics
Jan 11 08:33:44 Finished semantics                                             2m17s 978MB
Jan 11 08:33:46 Starting semantics/proofs
Jan 11 08:37:33 Finished semantics/proofs                                      3m45s   1GB
Jan 11 08:37:35 Starting basis/pure
Jan 11 08:38:48 Finished basis/pure                                            1m10s 588MB
Jan 11 08:38:50 Starting translator
Jan 11 08:46:19 Finished translator                                            7m27s 998MB
Jan 11 08:46:21 Starting compiler/parsing
Jan 11 08:48:51 Finished compiler/parsing                                      2m27s   1GB
Jan 11 08:48:53 Starting characteristic
Jan 11 08:53:50 Finished characteristic                                        4m54s   1GB
Jan 11 08:53:52 Starting basis
Jan 11 09:21:23 Finished basis                                                27m28s   2GB
Jan 11 09:21:24 Starting translator/monadic
Jan 11 09:24:56 Finished translator/monadic                                    3m29s   1GB
Jan 11 09:24:58 Starting compiler/inference
Jan 11 09:27:22 Finished compiler/inference                                    2m21s   1GB
Jan 11 09:27:24 Starting compiler/backend/reg_alloc
Jan 11 09:28:15 Finished compiler/backend/reg_alloc                              49s 823MB
Jan 11 09:28:17 Starting compiler/backend/gc
Jan 11 09:43:29 Finished compiler/backend/gc                                  15m09s   2GB
Jan 11 09:43:31 Starting compiler/backend
Jan 11 09:43:35 Finished compiler/backend                                         1s  19MB
Jan 11 09:43:37 Starting compiler/encoders/asm
Jan 11 09:43:40 Finished compiler/encoders/asm                                    0s  12MB
Jan 11 09:43:42 Starting compiler/encoders/x64
Jan 11 09:44:18 Finished compiler/encoders/x64                                   34s 495MB
Jan 11 09:44:20 Starting compiler/encoders/arm6
Jan 11 09:45:51 Finished compiler/encoders/arm6                                1m28s 421MB
Jan 11 09:45:53 Starting compiler/encoders/arm8
Jan 11 09:46:11 Finished compiler/encoders/arm8                                  16s 386MB
Jan 11 09:46:13 Starting compiler/encoders/mips
Jan 11 09:46:33 Finished compiler/encoders/mips                                  18s 557MB
Jan 11 09:46:35 Starting compiler/encoders/riscv
Jan 11 09:46:54 Finished compiler/encoders/riscv                                 17s 488MB
Jan 11 09:46:56 Starting compiler/backend/x64
Jan 11 09:47:41 Finished compiler/backend/x64                                    42s   1GB
Jan 11 09:47:43 Starting compiler/backend/arm6
Jan 11 09:48:32 Finished compiler/backend/arm6                                   47s   1GB
Jan 11 09:48:34 Starting compiler/backend/arm8
Jan 11 09:49:21 Finished compiler/backend/arm8                                   44s   1GB
Jan 11 09:49:23 Starting compiler/backend/mips
Jan 11 09:50:08 Finished compiler/backend/mips                                   43s   1GB
Jan 11 09:50:10 Starting compiler/backend/riscv
Jan 11 09:50:58 Finished compiler/backend/riscv                                  46s   1GB
Jan 11 09:51:00 Starting compiler/parsing/proofs
Jan 11 09:56:02 Finished compiler/parsing/proofs                               4m59s 705MB
Jan 11 09:56:04 Starting compiler/inference/proofs
Jan 11 10:00:36 Finished compiler/inference/proofs                             4m30s   1GB
Jan 11 10:00:38 Starting compiler/backend/semantics
Jan 11 10:20:36 Finished compiler/backend/semantics                           19m55s   2GB
Jan 11 10:20:38 Starting compiler/backend/reg_alloc/proofs
Jan 11 10:21:55 Finished compiler/backend/reg_alloc/proofs                     1m14s 395MB
Jan 11 10:21:57 Starting compiler/backend/proofs
Jan 11 11:35:28 Finished compiler/backend/proofs                            1h13m29s   4GB
Jan 11 11:35:31 Starting compiler/encoders/x64/proofs
Jan 11 11:46:39 Finished compiler/encoders/x64/proofs                         11m06s   1GB
Jan 11 11:46:41 Starting compiler/encoders/arm6/proofs
Jan 11 11:58:12 Finished compiler/encoders/arm6/proofs                        11m28s   1GB
Jan 11 11:58:13 Starting compiler/encoders/arm8/proofs
Jan 11 12:07:32 Finished compiler/encoders/arm8/proofs                         9m16s 689MB
Jan 11 12:07:34 Starting compiler/encoders/mips/proofs
Jan 11 12:19:54 Finished compiler/encoders/mips/proofs                        12m18s   1GB
Jan 11 12:19:56 Starting compiler/encoders/riscv/proofs
Jan 11 12:34:06 Finished compiler/encoders/riscv/proofs                       14m07s   1GB
Jan 11 12:34:08 Starting compiler/backend/x64/proofs
Jan 11 12:35:04 Finished compiler/backend/x64/proofs                             54s   1GB
Jan 11 12:35:06 Starting compiler/backend/arm6/proofs
Jan 11 12:36:07 Finished compiler/backend/arm6/proofs                            58s   1GB
Jan 11 12:36:09 Starting compiler/backend/arm8/proofs
Jan 11 12:37:03 Finished compiler/backend/arm8/proofs                            51s   1GB
Jan 11 12:37:05 Starting compiler/backend/mips/proofs
Jan 11 12:38:01 Finished compiler/backend/mips/proofs                            54s   1GB
Jan 11 12:38:03 Starting compiler/backend/riscv/proofs
Jan 11 12:38:58 Finished compiler/backend/riscv/proofs                           53s   1GB
Jan 11 12:39:00 Starting compiler/proofs
Jan 11 12:41:41 Finished compiler/proofs                                       2m38s   1GB
Jan 11 12:41:43 Starting candle/set-theory
Jan 11 12:42:36 Finished candle/set-theory                                       50s 549MB
Jan 11 12:42:38 Starting candle/syntax-lib
Jan 11 12:42:59 Finished candle/syntax-lib                                       19s 457MB
Jan 11 12:43:01 Starting candle/standard/syntax
Jan 11 12:46:08 Finished candle/standard/syntax                                3m05s 682MB
Jan 11 12:46:10 Starting candle/standard/semantics
Jan 11 12:48:46 Finished candle/standard/semantics                             2m33s 724MB
Jan 11 12:48:48 Starting candle/standard/monadic
Jan 11 12:51:37 Finished candle/standard/monadic                               2m47s 822MB
Jan 11 12:51:39 Starting candle/standard/ml_kernel
Jan 11 13:03:03 Finished candle/standard/ml_kernel                            11m21s   3GB
Jan 11 13:03:05 Starting candle/standard/opentheory
Jan 11 13:03:38 Finished candle/standard/opentheory                              31s 607MB
Jan 11 13:03:40 Starting characteristic/examples
Jan 11 13:06:03 Finished characteristic/examples                               2m20s   1GB
Jan 11 13:06:05 Starting tutorial/solutions
Jan 11 13:44:03 Finished tutorial/solutions                                   37m55s  10GB
Jan 11 13:44:05 Starting translator/monadic/examples
Jan 11 13:46:40 Finished translator/monadic/examples                           2m32s   1GB
Jan 11 13:46:42 Starting examples
Jan 11 13:54:45 Finished examples                                              8m00s   1GB
Jan 11 13:54:47 Starting examples/compilation
Jan 11 19:20:44 Finished examples/compilation                               5h25m54s  16GB
Jan 11 19:20:46 Starting examples/compilation/proofs
Jan 11 19:26:35 Finished examples/compilation/proofs                           5m46s   4GB
Jan 11 19:26:37 Starting compiler/benchmarks
Jan 11 19:26:40 Finished compiler/benchmarks                                      0s   6MB
Jan 11 19:26:42 Starting translator/okasaki-examples
Jan 11 19:34:22 Finished translator/okasaki-examples                           7m37s   1GB
Jan 11 19:34:24 Starting translator/other-examples
Jan 11 19:41:26 Finished translator/other-examples                             7m00s 759MB
Jan 11 19:41:28 Starting compiler/parsing/tests
Jan 11 19:42:09 Finished compiler/parsing/tests                                  38s 382MB
Jan 11 19:42:11 Starting compiler/bootstrap/translation
Jan 12 05:06:11 Finished compiler/bootstrap/translation                     9h23m58s  38GB
Jan 12 05:06:13 Starting compiler/bootstrap/compilation/x64/64
Jan 13 12:22:07 Finished compiler/bootstrap/compilation/x64/64             31h15m51s  83GB
Jan 13 12:22:09 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 13 12:26:56 Finished compiler/bootstrap/compilation/x64/64/proofs          4m45s  32GB
Jan 13 12:26:58 Starting compiler/bootstrap/compilation/x64/32
Jan 14 17:39:24 Finished compiler/bootstrap/compilation/x64/32             29h12m23s  83GB
Jan 14 17:39:26 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 14 17:42:43 Finished compiler/bootstrap/compilation/x64/32/proofs          3m15s  22GB
Jan 14 17:42:45 SUCCESS