Job 2280

CakeML:db8016defb7dd3b4814a55f4f77c94a1d592c330
  fix npbc_full add wcnf final proofs [Jan 23 04:03:40]
#978 (pb_output)
Merging into:e026a91d58aabda091e58bb8b4b8ca67b192f07c
  Fix mlvector given changes in HOL [Jan 17 02:43:46]
HOL:526e1ebc9210e0f2e357c010ad48b41cfa1d53fa
  Simplify/prune schneiderUtils.{sig,sml} [Jan 22 06:58:27]
Machine:pavlova

Jan 23 14:35:14 Claimed job
Jan 23 14:35:18 Reusing HOL
Jan 23 14:35:27 Starting developers
Jan 23 14:35:31 Finished developers                                               2s 194MB
Jan 23 14:35:32 Starting developers/bin
Jan 23 14:35:44 Finished developers/bin                                          11s   1GB
Jan 23 14:35:45 Starting compiler/proofs
Jan 23 16:20:16 Finished compiler/proofs                                    1h44m29s  39GB
Jan 23 16:20:16 Starting compiler/bootstrap/translation
Jan 24 00:32:48 Finished compiler/bootstrap/translation                     8h12m30s  69GB
Jan 24 00:32:49 Starting semantics/ffi
Jan 24 00:32:57 Finished semantics/ffi                                            7s 691MB
Jan 24 00:32:58 Starting semantics
Jan 24 00:32:59 Finished semantics                                                0s  67MB
Jan 24 00:33:00 Starting semantics/proofs
Jan 24 00:33:36 Finished semantics/proofs                                        34s   2GB
Jan 24 00:33:36 Starting semantics/alt_semantics
Jan 24 00:34:16 Finished semantics/alt_semantics                                 38s   1GB
Jan 24 00:34:17 Starting semantics/alt_semantics/proofs
Jan 24 00:45:21 Finished semantics/alt_semantics/proofs                       11m03s   2GB
Jan 24 00:45:22 Starting basis/pure
Jan 24 00:45:23 Finished basis/pure                                               0s  67MB
Jan 24 00:45:24 Starting translator
Jan 24 00:47:05 Finished translator                                            1m40s   3GB
Jan 24 00:47:06 Starting compiler/parsing
Jan 24 00:47:07 Finished compiler/parsing                                         0s  72MB
Jan 24 00:47:08 Starting characteristic
Jan 24 00:47:09 Finished characteristic                                           0s  85MB
Jan 24 00:47:10 Starting translator/monadic
Jan 24 00:47:12 Finished translator/monadic                                       0s  98MB
Jan 24 00:47:12 Starting basis
Jan 24 00:50:49 Finished basis                                                 3m35s   5GB
Jan 24 00:50:49 Starting compiler/inference
Jan 24 00:50:51 Finished compiler/inference                                       0s  79MB
Jan 24 00:50:52 Starting compiler/backend/reg_alloc
Jan 24 00:50:53 Finished compiler/backend/reg_alloc                               0s  66MB
Jan 24 00:50:54 Starting compiler/backend/gc
Jan 24 00:50:56 Finished compiler/backend/gc                                      0s 138MB
Jan 24 00:50:56 Starting compiler/backend
Jan 24 00:51:14 Finished compiler/backend                                        16s   1GB
Jan 24 00:51:15 Starting compiler/encoders/asm
Jan 24 00:51:16 Finished compiler/encoders/asm                                    0s  91MB
Jan 24 00:51:17 Starting compiler/encoders/x64
Jan 24 00:51:18 Finished compiler/encoders/x64                                    0s  94MB
Jan 24 00:51:19 Starting compiler/encoders/arm7
Jan 24 00:51:21 Finished compiler/encoders/arm7                                   0s  95MB
Jan 24 00:51:21 Starting compiler/encoders/arm8
Jan 24 00:51:23 Finished compiler/encoders/arm8                                   0s  91MB
Jan 24 00:51:24 Starting compiler/encoders/arm8_asl
Jan 24 03:10:25 Finished compiler/encoders/arm8_asl                         2h19m00s  43GB
Jan 24 03:10:26 Starting compiler/encoders/mips
Jan 24 03:10:28 Finished compiler/encoders/mips                                   0s  87MB
Jan 24 03:10:29 Starting compiler/encoders/riscv
Jan 24 03:10:30 Finished compiler/encoders/riscv                                  0s  89MB
Jan 24 03:10:31 Starting compiler/encoders/ag32
Jan 24 03:10:32 Finished compiler/encoders/ag32                                   0s  85MB
Jan 24 03:10:33 Starting compiler/backend/x64
Jan 24 03:10:35 Finished compiler/backend/x64                                     0s 129MB
Jan 24 03:10:36 Starting compiler/backend/arm7
Jan 24 03:10:37 Finished compiler/backend/arm7                                    0s 129MB
Jan 24 03:10:38 Starting compiler/backend/arm8
Jan 24 03:10:40 Finished compiler/backend/arm8                                    0s 129MB
Jan 24 03:10:41 Starting compiler/backend/mips
Jan 24 03:10:42 Finished compiler/backend/mips                                    0s 129MB
Jan 24 03:10:43 Starting compiler/backend/riscv
Jan 24 03:10:45 Finished compiler/backend/riscv                                   0s 129MB
Jan 24 03:10:46 Starting compiler/backend/ag32
Jan 24 03:12:02 Finished compiler/backend/ag32                                 1m15s   2GB
Jan 24 03:12:03 Starting compiler/parsing/proofs
Jan 24 03:12:04 Finished compiler/parsing/proofs                                  0s  75MB
Jan 24 03:12:05 Starting compiler/inference/proofs
Jan 24 03:12:07 Finished compiler/inference/proofs                                0s  89MB
Jan 24 03:12:08 Starting compiler/backend/semantics
Jan 24 03:13:34 Finished compiler/backend/semantics                            1m25s   2GB
Jan 24 03:13:35 Starting compiler/backend/reg_alloc/proofs
Jan 24 03:13:36 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jan 24 03:13:37 Starting compiler/backend/proofs
Jan 24 03:14:38 Finished compiler/backend/proofs                                 59s   3GB
Jan 24 03:14:39 Starting compiler/backend/serialiser
Jan 24 03:14:41 Finished compiler/backend/serialiser                              1s 181MB
Jan 24 03:14:42 Starting compiler/encoders/x64/proofs
Jan 24 03:24:03 Finished compiler/encoders/x64/proofs                          9m20s   5GB
Jan 24 03:24:04 Starting compiler/encoders/arm7/proofs
Jan 24 03:36:52 Finished compiler/encoders/arm7/proofs                        12m47s   9GB
Jan 24 03:36:53 Starting compiler/encoders/arm8/proofs
Jan 24 03:43:20 Finished compiler/encoders/arm8/proofs                         6m26s   5GB
Jan 24 03:43:21 Starting compiler/encoders/arm8_asl/proofs
Jan 24 04:30:48 Finished compiler/encoders/arm8_asl/proofs                    47m26s   6GB
Jan 24 04:30:49 Starting compiler/encoders/mips/proofs
Jan 24 04:40:48 Finished compiler/encoders/mips/proofs                         9m57s   8GB
Jan 24 04:40:48 Starting compiler/encoders/riscv/proofs
Jan 24 04:49:00 Finished compiler/encoders/riscv/proofs                        8m11s   3GB
Jan 24 04:49:01 Starting compiler/encoders/ag32/proofs
Jan 25 23:49:43 Resuming compiler/encoders/ag32/proofs
Jan 25 23:49:44 Finished compiler/encoders/ag32/proofs                            0s  87MB
Jan 25 23:49:45 Starting compiler/backend/x64/proofs
Jan 25 23:50:25 Finished compiler/backend/x64/proofs                             39s   2GB
Jan 25 23:50:26 Starting compiler/backend/arm7/proofs
Jan 25 23:51:07 Finished compiler/backend/arm7/proofs                            39s   2GB
Jan 25 23:51:08 Starting compiler/backend/arm8/proofs
Jan 25 23:51:46 Finished compiler/backend/arm8/proofs                            37s   3GB
Jan 25 23:51:47 Starting compiler/backend/arm8_asl
Jan 25 23:52:15 Finished compiler/backend/arm8_asl                               26s   2GB
Jan 25 23:52:16 Starting compiler/backend/mips/proofs
Jan 25 23:52:59 Finished compiler/backend/mips/proofs                            42s   3GB
Jan 25 23:53:00 Starting compiler/backend/riscv/proofs
Jan 25 23:53:49 Finished compiler/backend/riscv/proofs                           48s   4GB
Jan 25 23:53:50 Starting compiler/backend/ag32/proofs
Jan 26 00:07:06 Finished compiler/backend/ag32/proofs                         13m15s   6GB
Jan 26 00:07:07 Starting candle/set-theory
Jan 26 00:07:51 Finished candle/set-theory                                       43s   1GB
Jan 26 00:07:52 Starting candle/syntax-lib
Jan 26 00:07:53 Finished candle/syntax-lib                                        0s  69MB
Jan 26 00:07:54 Starting candle/standard/syntax
Jan 26 00:08:11 Finished candle/standard/syntax                                  16s   1GB
Jan 26 00:08:12 Starting candle/standard/semantics
Jan 26 00:10:33 Finished candle/standard/semantics                             2m20s   2GB
Jan 26 00:10:34 Starting candle/standard/monadic
Jan 26 00:10:35 Finished candle/standard/monadic                                  0s 105MB
Jan 26 00:10:36 Starting candle/standard/ml_kernel
Jan 26 00:12:26 Finished candle/standard/ml_kernel                             1m48s   5GB
Jan 26 00:12:27 Starting candle/overloading/syntax
Jan 26 00:15:53 Finished candle/overloading/syntax                             3m25s   2GB
Jan 26 00:15:54 Starting candle/overloading/semantics
Jan 26 00:27:16 Finished candle/overloading/semantics                         11m20s  13GB
Jan 26 00:27:17 Starting candle/overloading/monadic
Jan 26 00:29:49 Finished candle/overloading/monadic                            2m31s   2GB
Jan 26 00:29:50 Starting candle/overloading/ml_kernel
Jan 26 00:37:20 Finished candle/overloading/ml_kernel                          7m28s   6GB
Jan 26 00:37:21 Starting candle/overloading/ml_checker
Jan 26 00:39:53 Finished candle/overloading/ml_checker                         2m31s   7GB
Jan 26 00:39:54 Starting candle/prover
Jan 26 00:49:44 Finished candle/prover                                         9m49s   5GB
Jan 26 00:49:45 Starting pancake
Jan 26 00:50:44 Finished pancake                                                 58s   1GB
Jan 26 00:50:45 Starting pancake/ffi
Jan 26 00:50:46 Finished pancake/ffi                                              0s  21MB
Jan 26 00:50:47 Starting pancake/semantics
Jan 26 00:53:04 Finished pancake/semantics                                     2m16s   2GB
Jan 26 00:53:05 Starting pancake/parser
Jan 26 00:53:32 Finished pancake/parser                                          26s   1GB
Jan 26 00:53:33 Starting pancake/proofs
Jan 26 01:23:18 Finished pancake/proofs                                       29m43s  11GB
Jan 26 01:23:18 Starting characteristic/examples
Jan 26 01:24:54 Finished characteristic/examples                               1m34s   5GB
Jan 26 01:24:55 Starting tutorial/solutions
Jan 26 01:40:07 Finished tutorial/solutions                                   15m11s  13GB
Jan 26 01:40:08 Starting translator/monadic/examples
Jan 26 01:43:53 Finished translator/monadic/examples                           3m44s   5GB
Jan 26 01:43:53 Starting examples
Jan 26 01:58:20 Finished examples                                             14m25s   7GB
Jan 26 01:58:21 Starting examples/compilation/x64
Jan 26 03:55:00 Finished examples/compilation/x64                           1h56m38s  36GB
Jan 26 03:55:01 Starting examples/compilation/x64/proofs
Jan 26 03:58:47 Finished examples/compilation/x64/proofs                       3m45s   6GB
Jan 26 03:58:48 Starting examples/compilation/ag32
Jan 26 04:28:26 Finished examples/compilation/ag32                            29m37s  14GB
Jan 26 04:28:27 Starting examples/compilation/ag32/proofs
Jan 26 04:30:04 Finished examples/compilation/ag32/proofs                      1m36s   7GB
Jan 26 04:30:05 Starting examples/compilation/to_word
Jan 26 04:33:59 Finished examples/compilation/to_word                          3m52s  14GB
Jan 26 04:34:00 Starting examples/lpr_checker
Jan 26 04:35:14 Finished examples/lpr_checker                                  1m13s   2GB
Jan 26 04:35:15 Starting examples/lpr_checker/array
Jan 26 05:04:28 Finished examples/lpr_checker/array                           29m11s   8GB
Jan 26 05:04:29 Starting examples/lpr_checker/array/compilation
Jan 26 05:38:32 Finished examples/lpr_checker/array/compilation               34m02s  42GB
Jan 26 05:38:33 Starting examples/lpr_checker/array/compilation/proofs
Jan 26 05:40:34 Finished examples/lpr_checker/array/compilation/proofs         2m00s  10GB
Jan 26 05:40:35 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 26 06:02:54 Finished examples/lpr_checker/array/compilation/proofsARM8    22m17s  36GB
Jan 26 06:02:55 Starting examples/pseudo_bool
Jan 26 06:04:55 Finished examples/pseudo_bool                                  1m59s   1GB
Jan 26 06:04:56 Starting examples/pseudo_bool/cnf_encoding
Jan 26 06:05:32 Finished examples/pseudo_bool/cnf_encoding                       34s   1GB
Jan 26 06:05:33 Starting examples/pseudo_bool/graph_encoding
Jan 26 06:06:21 Finished examples/pseudo_bool/graph_encoding                     47s   2GB
Jan 26 06:06:22 Starting examples/pseudo_bool/array
Jan 26 07:00:06 Finished examples/pseudo_bool/array                           53m42s  14GB
Jan 26 07:00:06 Starting examples/pseudo_bool/array/compilation
Jan 26 09:08:48 Finished examples/pseudo_bool/array/compilation             2h08m40s 112GB
Jan 26 09:08:49 Starting examples/pseudo_bool/array/compilation/proofs
Jan 26 09:11:58 Finished examples/pseudo_bool/array/compilation/proofs         3m07s   7GB
Jan 26 09:11:59 Starting examples/opentheory
Jan 26 09:22:27 Finished examples/opentheory                                  10m27s   8GB
Jan 26 09:22:28 Starting examples/opentheory
Jan 26 09:22:30 Finished examples/opentheory                                      0s 123MB
Jan 26 09:22:31 Starting examples/opentheory/compilation
Jan 26 09:58:03 Finished examples/opentheory/compilation                      35m31s  52GB
Jan 26 09:58:04 Starting examples/opentheory/compilation/proofs
Jan 26 09:59:32 Finished examples/opentheory/compilation/proofs                1m27s   6GB
Jan 26 09:59:33 Starting examples/opentheory/compilation/ag32
Jan 26 10:31:09 Finished examples/opentheory/compilation/ag32                 31m35s  48GB
Jan 26 10:31:10 Starting examples/opentheory/compilation/ag32/proofs
Jan 26 10:33:25 Finished examples/opentheory/compilation/ag32/proofs           2m13s  11GB
Jan 26 10:33:26 Starting examples/sat_encodings
Jan 26 10:36:04 Finished examples/sat_encodings                                2m36s   1GB
Jan 26 10:36:05 Starting examples/sat_encodings/case_studies
Jan 26 10:38:04 Finished examples/sat_encodings/case_studies                   1m58s   2GB
Jan 26 10:38:05 Starting examples/sat_encodings/translation
Jan 26 10:44:14 Finished examples/sat_encodings/translation                    6m08s   7GB
Jan 26 10:44:15 Starting examples/sat_encodings/translation/compilation
Jan 26 11:19:21 Finished examples/sat_encodings/translation/compilation       35m04s  43GB
Jan 26 11:19:22 Starting examples/deflate
Jan 26 11:20:36 Finished examples/deflate                                      1m12s   1GB
Jan 26 11:20:36 Starting examples/deflate/translation
Jan 26 11:22:12 Finished examples/deflate/translation                          1m34s   7GB
Jan 26 11:22:13 Starting examples/deflate/translation/compilation
Jan 26 11:38:35 Finished examples/deflate/translation/compilation             16m21s  28GB
Jan 26 11:38:36 Starting examples/vipr
Jan 26 11:42:36 Finished examples/vipr                                         3m59s   7GB
Jan 26 11:42:37 Starting examples/vipr/compilation
Jan 26 12:02:53 Finished examples/vipr/compilation                            20m14s  37GB
Jan 26 12:02:54 Starting translator/okasaki-examples
Jan 26 12:07:53 Finished translator/okasaki-examples                           4m57s   4GB
Jan 26 12:07:53 Starting translator/other-examples
Jan 26 12:11:29 Finished translator/other-examples                             3m34s   3GB
Jan 26 12:11:30 Starting compiler/parsing/tests
Jan 26 12:12:03 Finished compiler/parsing/tests                                  32s   1GB
Jan 26 12:12:04 Starting compiler/inference/tests
Jan 26 12:19:31 Finished compiler/inference/tests                              7m26s   5GB
Jan 26 12:19:32 Starting compiler/printing/test
Jan 26 12:23:00 Finished compiler/printing/test                                3m27s   6GB
Jan 26 12:23:01 Starting icing/flover
Jan 26 12:58:16 Finished icing/flover                                         35m14s   4GB
Jan 26 12:58:17 Starting icing/
Jan 26 13:53:34 Finished icing/                                               55m15s  30GB
Jan 26 13:53:35 Starting icing/examples
Jan 26 13:55:16 Finished icing/examples                                        1m40s   8GB
Jan 26 13:55:17 Starting compiler/repl
Jan 26 14:04:01 Finished compiler/repl                                         8m42s   9GB
Jan 26 14:04:02 Starting unverified/sexpr-bootstrap/x64/64
Jan 26 14:15:01 Finished unverified/sexpr-bootstrap/x64/64                    10m58s  16GB
Jan 26 14:15:02 Starting unverified/sexpr-bootstrap/x64/32
Jan 26 14:23:59 Finished unverified/sexpr-bootstrap/x64/32                     8m55s  13GB
Jan 26 14:24:00 Starting compiler/benchmarks
Jan 26 14:24:44 Finished compiler/benchmarks                                     43s 713MB
Jan 26 14:24:45 Starting compiler/bootstrap/compilation/x64/64
Jan 27 04:55:41 Finished compiler/bootstrap/compilation/x64/64             14h30m55s 148GB
Jan 27 04:55:42 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 27 05:16:58 Finished compiler/bootstrap/compilation/x64/64/proofs         21m15s  46GB
Jan 27 05:16:59 Starting compiler/bootstrap/compilation/x64/32
Jan 27 12:15:27 Finished compiler/bootstrap/compilation/x64/32              6h58m27s 155GB
Jan 27 12:15:28 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 27 12:19:00 Finished compiler/bootstrap/compilation/x64/32/proofs          3m30s  18GB
Jan 27 12:19:01 Starting compiler/bootstrap/compilation/ag32/32
Jan 27 19:44:57 Finished compiler/bootstrap/compilation/ag32/32             7h25m55s 145GB
Jan 27 19:44:58 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 27 19:52:23 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m23s  45GB
Jan 27 19:52:24 SUCCESS