Job 2303

CakeML:82012f90a7ee71dd8a07de33c92304ae526fe758
  Remove unused arg from closLang's ByteArray [Feb 10 23:41:50]
#982 (contexts)
Merging into:647a11e7fd30db7a862d9655aa3abbb231c1e199
  Fix Candle breakage caused by HOL-Theorem-Prover/HOL@d64dda1e4e [Feb 20 01:19:56]
HOL:cbfd91fbff3db1f5397fcf21b76efbba76c7f081
  Prove a nice BIT x (l2n b n) result [Feb 20 01:22:36]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Feb 22 09:36:39 Claimed job
Feb 22 09:36:46 Building HOL
Feb 22 09:49:44 Starting developers
Feb 22 09:49:49 Finished developers                                               5s 118MB
Feb 22 09:49:50 Starting developers/bin
Feb 22 09:49:56 Finished developers/bin                                           6s   1GB
Feb 22 09:49:56 Starting compiler/proofs
Feb 23 23:49:39 Resuming compiler/proofs
Feb 23 23:52:32 Finished compiler/proofs                                       2m52s   3GB
Feb 23 23:52:32 Starting compiler/bootstrap/translation
Feb 24 08:03:46 Finished compiler/bootstrap/translation                     8h11m13s  45GB
Feb 24 08:03:46 Starting semantics/ffi
Feb 24 08:03:51 Finished semantics/ffi                                            4s 384MB
Feb 24 08:03:51 Starting semantics
Feb 24 08:03:52 Finished semantics                                                1s  21MB
Feb 24 08:03:53 Starting semantics/proofs
Feb 24 08:04:26 Finished semantics/proofs                                        33s 726MB
Feb 24 08:04:26 Starting semantics/alt_semantics
Feb 24 08:04:58 Finished semantics/alt_semantics                                 32s 903MB
Feb 24 08:04:58 Starting semantics/alt_semantics/proofs
Feb 24 08:16:58 Finished semantics/alt_semantics/proofs                       11m59s   1GB
Feb 24 08:16:58 Starting basis/pure
Feb 24 08:17:00 Finished basis/pure                                               1s  18MB
Feb 24 08:17:00 Starting translator
Feb 24 08:18:50 Finished translator                                            1m50s   1GB
Feb 24 08:18:50 Starting compiler/parsing
Feb 24 08:18:52 Finished compiler/parsing                                         1s  18MB
Feb 24 08:18:52 Starting characteristic
Feb 24 08:18:54 Finished characteristic                                           1s  22MB
Feb 24 08:18:54 Starting translator/monadic
Feb 24 08:18:56 Finished translator/monadic                                       1s  20MB
Feb 24 08:18:56 Starting basis
Feb 24 08:22:42 Finished basis                                                 3m45s   3GB
Feb 24 08:22:42 Starting compiler/inference
Feb 24 08:22:43 Finished compiler/inference                                       1s  21MB
Feb 24 08:22:44 Starting compiler/backend/reg_alloc
Feb 24 08:22:45 Finished compiler/backend/reg_alloc                               1s  18MB
Feb 24 08:22:45 Starting compiler/backend/gc
Feb 24 08:22:48 Finished compiler/backend/gc                                      2s  29MB
Feb 24 08:22:48 Starting compiler/backend
Feb 24 08:23:01 Finished compiler/backend                                        12s 788MB
Feb 24 08:23:01 Starting compiler/encoders/asm
Feb 24 08:23:02 Finished compiler/encoders/asm                                    1s  22MB
Feb 24 08:23:02 Starting compiler/encoders/x64
Feb 24 08:23:04 Finished compiler/encoders/x64                                    1s  27MB
Feb 24 08:23:04 Starting compiler/encoders/arm7
Feb 24 08:23:06 Finished compiler/encoders/arm7                                   1s  28MB
Feb 24 08:23:06 Starting compiler/encoders/arm8
Feb 24 08:23:08 Finished compiler/encoders/arm8                                   1s  22MB
Feb 24 08:23:08 Starting compiler/encoders/arm8_asl
Feb 24 10:50:06 Finished compiler/encoders/arm8_asl                         2h26m57s  45GB
Feb 24 10:50:06 Starting compiler/encoders/mips
Feb 24 10:50:08 Finished compiler/encoders/mips                                   1s  22MB
Feb 24 10:50:08 Starting compiler/encoders/riscv
Feb 24 10:50:10 Finished compiler/encoders/riscv                                  1s  27MB
Feb 24 10:50:10 Starting compiler/encoders/ag32
Feb 24 10:50:12 Finished compiler/encoders/ag32                                   1s  20MB
Feb 24 10:50:12 Starting compiler/backend/x64
Feb 24 10:50:14 Finished compiler/backend/x64                                     2s  25MB
Feb 24 10:50:14 Starting compiler/backend/arm7
Feb 24 10:50:16 Finished compiler/backend/arm7                                    2s  22MB
Feb 24 10:50:16 Starting compiler/backend/arm8
Feb 24 10:50:19 Finished compiler/backend/arm8                                    2s  24MB
Feb 24 10:50:19 Starting compiler/backend/mips
Feb 24 10:50:21 Finished compiler/backend/mips                                    2s  32MB
Feb 24 10:50:21 Starting compiler/backend/riscv
Feb 24 10:50:23 Finished compiler/backend/riscv                                   2s  25MB
Feb 24 10:50:23 Starting compiler/backend/ag32
Feb 24 10:51:48 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 24 10:51:48 Starting compiler/parsing/proofs
Feb 24 10:51:50 Finished compiler/parsing/proofs                                  1s  21MB
Feb 24 10:51:50 Starting compiler/inference/proofs
Feb 24 10:51:52 Finished compiler/inference/proofs                                1s  27MB
Feb 24 10:51:52 Starting compiler/backend/semantics
Feb 24 10:53:05 Finished compiler/backend/semantics                            1m13s   1GB
Feb 24 10:53:06 Starting compiler/backend/reg_alloc/proofs
Feb 24 10:53:08 Finished compiler/backend/reg_alloc/proofs                        1s  25MB
Feb 24 10:53:08 Starting compiler/backend/proofs
Feb 24 10:54:07 Finished compiler/backend/proofs                                 59s   3GB
Feb 24 10:54:07 Starting compiler/backend/serialiser
Feb 24 10:54:10 Finished compiler/backend/serialiser                              2s  33MB
Feb 24 10:54:11 Starting compiler/encoders/x64/proofs
Feb 24 11:04:00 Finished compiler/encoders/x64/proofs                          9m49s   5GB
Feb 24 11:04:00 Starting compiler/encoders/arm7/proofs
Feb 24 11:17:55 Finished compiler/encoders/arm7/proofs                        13m54s   3GB
Feb 24 11:17:55 Starting compiler/encoders/arm8/proofs
Feb 24 11:25:00 Finished compiler/encoders/arm8/proofs                         7m04s   1GB
Feb 24 11:25:00 Starting compiler/encoders/arm8_asl/proofs
Feb 24 12:17:27 Finished compiler/encoders/arm8_asl/proofs                    52m26s   6GB
Feb 24 12:17:27 Starting compiler/encoders/mips/proofs
Feb 24 12:28:01 Finished compiler/encoders/mips/proofs                        10m33s   3GB
Feb 24 12:28:01 Starting compiler/encoders/riscv/proofs
Feb 24 12:37:04 Finished compiler/encoders/riscv/proofs                        9m03s   1GB
Feb 24 12:37:04 Starting compiler/encoders/ag32/proofs
Feb 24 12:39:37 Finished compiler/encoders/ag32/proofs                         2m33s   1GB
Feb 24 12:39:37 Starting compiler/backend/x64/proofs
Feb 24 12:40:08 Finished compiler/backend/x64/proofs                             30s   2GB
Feb 24 12:40:08 Starting compiler/backend/arm7/proofs
Feb 24 12:40:40 Finished compiler/backend/arm7/proofs                            31s   1GB
Feb 24 12:40:40 Starting compiler/backend/arm8/proofs
Feb 24 12:41:10 Finished compiler/backend/arm8/proofs                            29s   1GB
Feb 24 12:41:10 Starting compiler/backend/arm8_asl
Feb 24 12:41:34 Finished compiler/backend/arm8_asl                               24s   2GB
Feb 24 12:41:34 Starting compiler/backend/mips/proofs
Feb 24 12:42:09 Finished compiler/backend/mips/proofs                            34s   2GB
Feb 24 12:42:09 Starting compiler/backend/riscv/proofs
Feb 24 12:42:44 Finished compiler/backend/riscv/proofs                           35s   2GB
Feb 24 12:42:44 Starting compiler/backend/ag32/proofs
Feb 24 12:56:22 Finished compiler/backend/ag32/proofs                         13m38s   3GB
Feb 24 12:56:22 Starting candle/set-theory
Feb 24 12:57:01 Finished candle/set-theory                                       39s   1GB
Feb 24 12:57:01 Starting candle/syntax-lib
Feb 24 12:57:03 Finished candle/syntax-lib                                        1s  21MB
Feb 24 12:57:03 Starting candle/standard/syntax
Feb 24 12:57:14 Finished candle/standard/syntax                                  10s 797MB
Feb 24 12:57:14 Starting candle/standard/semantics
Feb 24 12:59:13 Finished candle/standard/semantics                             1m59s   1GB
Feb 24 12:59:13 Starting candle/standard/monadic
Feb 24 12:59:15 Finished candle/standard/monadic                                  1s  22MB
Feb 24 12:59:15 Starting candle/standard/ml_kernel
Feb 24 13:01:03 Finished candle/standard/ml_kernel                             1m47s   3GB
Feb 24 13:01:03 Starting candle/overloading/syntax
Feb 24 13:04:27 Finished candle/overloading/syntax                             3m23s   1GB
Feb 24 13:04:27 Starting candle/overloading/semantics
Feb 24 13:16:42 Finished candle/overloading/semantics                         12m14s   2GB
Feb 24 13:16:42 Starting candle/overloading/monadic
Feb 24 13:19:27 Finished candle/overloading/monadic                            2m44s   1GB
Feb 24 13:19:27 Starting candle/overloading/ml_kernel
Feb 24 13:27:17 Finished candle/overloading/ml_kernel                          7m49s   4GB
Feb 24 13:27:17 Starting candle/overloading/ml_checker
Feb 24 13:29:55 Finished candle/overloading/ml_checker                         2m37s   2GB
Feb 24 13:29:55 Starting candle/prover
Feb 24 13:40:03 Finished candle/prover                                        10m08s   4GB
Feb 24 13:40:03 Starting pancake
Feb 24 13:40:50 Finished pancake                                                 46s 884MB
Feb 24 13:40:50 Starting pancake/ffi
Feb 24 13:40:50 Finished pancake/ffi                                              0s  13MB
Feb 24 13:40:50 Starting pancake/semantics
Feb 24 13:43:21 Finished pancake/semantics                                     2m30s   1GB
Feb 24 13:43:21 Starting pancake/parser
Feb 24 13:43:43 Finished pancake/parser                                          22s 650MB
Feb 24 13:43:43 Starting pancake/proofs
Feb 24 14:17:25 Finished pancake/proofs                                       33m41s   4GB
Feb 24 14:17:26 Starting characteristic/examples
Feb 24 14:19:00 Finished characteristic/examples                               1m34s   2GB
Feb 24 14:19:00 Starting tutorial/solutions
Feb 24 14:34:35 Finished tutorial/solutions                                   15m35s   9GB
Feb 24 14:34:35 Starting translator/monadic/examples
Feb 24 14:38:42 Finished translator/monadic/examples                           4m06s   2GB
Feb 24 14:38:42 Starting examples
Feb 24 14:55:10 Finished examples                                             16m27s   4GB
Feb 24 14:55:10 Starting examples/compilation/x64
Feb 24 16:56:04 Finished examples/compilation/x64                           2h00m53s  16GB
Feb 24 16:56:04 Starting examples/compilation/x64/proofs
Feb 24 16:58:41 Finished examples/compilation/x64/proofs                       2m36s   4GB
Feb 24 16:58:41 Starting examples/compilation/ag32
Feb 24 17:29:10 Finished examples/compilation/ag32                            30m28s   9GB
Feb 24 17:29:10 Starting examples/compilation/ag32/proofs
Feb 24 17:30:14 Finished examples/compilation/ag32/proofs                      1m04s   4GB
Feb 24 17:30:14 Starting examples/compilation/to_word
Feb 24 17:33:40 Finished examples/compilation/to_word                          3m25s   6GB
Feb 24 17:33:40 Starting examples/lpr_checker
Feb 24 17:34:45 Finished examples/lpr_checker                                  1m04s   1GB
Feb 24 17:34:45 Starting examples/lpr_checker/array
Feb 24 18:05:25 Finished examples/lpr_checker/array                           30m39s   5GB
Feb 24 18:05:25 Starting examples/lpr_checker/array/compilation
Feb 24 18:56:36 Finished examples/lpr_checker/array/compilation               51m10s  19GB
Feb 24 18:56:36 Starting examples/lpr_checker/array/compilation/proofs
Feb 24 18:58:37 Finished examples/lpr_checker/array/compilation/proofs         2m01s   3GB
Feb 24 18:58:37 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 24 19:08:10 Finished examples/lpr_checker/array/compilation/proofsARM8     9m32s  25GB
Feb 24 19:08:10 Starting examples/xlrup_checker
Feb 25 12:03:48 Resuming examples/xlrup_checker