Job 1426

CakeML:f8cee9669d3a566324308dec3ee73f8ea6b2cb58
  fix lpr_commonProg [Dec 31 10:27:52]
#809 (lpr)
Merging into:86bded59186b861ecdecf4a8f3019df160b74b98
  fix ramseyScript [Dec 30 02:27:27]
HOL:5921a959757a023b13010b448a2cd05222e641b6
  Prove the converse of PERM_BIJ [Dec 27 00:55:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 02 21:40:38 Claimed job
Jan 02 21:40:44 Reusing HOL
Jan 02 21:40:52 Starting developers
Jan 02 21:40:54 Finished developers                                               2s 130MB
Jan 02 21:40:54 Starting developers/bin
Jan 02 21:41:02 Finished developers/bin                                           8s   1GB
Jan 02 21:41:03 Starting semantics/ffi
Jan 02 21:41:13 Finished semantics/ffi                                           10s 291MB
Jan 02 21:41:13 Starting semantics
Jan 02 21:42:38 Finished semantics                                             1m24s   1GB
Jan 02 21:42:38 Starting semantics/proofs
Jan 02 21:45:57 Finished semantics/proofs                                      3m18s   1GB
Jan 02 21:45:57 Starting semantics/alt_semantics
Jan 02 21:46:05 Finished semantics/alt_semantics                                  8s 405MB
Jan 02 21:46:05 Starting semantics/alt_semantics/proofs
Jan 02 21:48:13 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Jan 02 21:48:13 Starting basis/pure
Jan 02 21:49:05 Finished basis/pure                                              52s   1GB
Jan 02 21:49:05 Starting translator
Jan 02 21:51:41 Finished translator                                            2m34s   2GB
Jan 02 21:51:41 Starting compiler/parsing
Jan 02 21:52:47 Finished compiler/parsing                                      1m05s   2GB
Jan 02 21:52:47 Starting characteristic
Jan 02 21:58:46 Finished characteristic                                        5m58s   3GB
Jan 02 21:58:46 Starting translator/monadic
Jan 02 22:00:33 Finished translator/monadic                                    1m46s   3GB
Jan 02 22:00:33 Starting basis
Jan 02 22:34:19 Finished basis                                                33m46s  39GB
Jan 02 22:34:20 Starting compiler/inference
Jan 02 22:35:22 Finished compiler/inference                                    1m02s   1GB
Jan 02 22:35:22 Starting compiler/backend/reg_alloc
Jan 02 22:36:25 Finished compiler/backend/reg_alloc                            1m02s   1GB
Jan 02 22:36:25 Starting compiler/backend/gc
Jan 02 22:39:45 Finished compiler/backend/gc                                   3m19s   3GB
Jan 02 22:39:45 Starting compiler/backend
Jan 02 22:44:42 Finished compiler/backend                                      4m57s   4GB
Jan 02 22:44:43 Starting compiler/encoders/asm
Jan 02 22:45:04 Finished compiler/encoders/asm                                   21s   1GB
Jan 02 22:45:05 Starting compiler/encoders/x64
Jan 02 22:45:31 Finished compiler/encoders/x64                                   26s   1GB
Jan 02 22:45:31 Starting compiler/encoders/arm7
Jan 02 22:46:22 Finished compiler/encoders/arm7                                  50s   1GB
Jan 02 22:46:22 Starting compiler/encoders/arm8
Jan 02 22:46:36 Finished compiler/encoders/arm8                                  13s   1GB
Jan 02 22:46:36 Starting compiler/encoders/mips
Jan 02 22:46:54 Finished compiler/encoders/mips                                  17s   1GB
Jan 02 22:46:54 Starting compiler/encoders/riscv
Jan 02 22:47:10 Finished compiler/encoders/riscv                                 16s   1GB
Jan 02 22:47:10 Starting compiler/encoders/ag32
Jan 02 22:47:29 Finished compiler/encoders/ag32                                  18s 962MB
Jan 02 22:47:29 Starting compiler/backend/x64
Jan 02 22:47:48 Finished compiler/backend/x64                                    19s   1GB
Jan 02 22:47:48 Starting compiler/backend/arm7
Jan 02 22:48:10 Finished compiler/backend/arm7                                   21s   1GB
Jan 02 22:48:10 Starting compiler/backend/arm8
Jan 02 22:48:29 Finished compiler/backend/arm8                                   19s   1GB
Jan 02 22:48:29 Starting compiler/backend/mips
Jan 02 22:48:50 Finished compiler/backend/mips                                   20s   1GB
Jan 02 22:48:50 Starting compiler/backend/riscv
Jan 02 22:49:10 Finished compiler/backend/riscv                                  19s   1GB
Jan 02 22:49:10 Starting compiler/backend/ag32
Jan 02 22:50:22 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 02 22:50:22 Starting compiler/parsing/proofs
Jan 02 22:55:49 Finished compiler/parsing/proofs                               5m26s   3GB
Jan 02 22:55:49 Starting compiler/inference/proofs
Jan 02 22:58:20 Finished compiler/inference/proofs                             2m30s   2GB
Jan 02 22:58:20 Starting compiler/backend/semantics
Jan 02 23:25:20 Finished compiler/backend/semantics                           26m59s   6GB
Jan 02 23:25:20 Starting compiler/backend/reg_alloc/proofs
Jan 02 23:28:42 Finished compiler/backend/reg_alloc/proofs                     3m21s   2GB
Jan 02 23:28:43 Starting compiler/backend/proofs
Jan 03 00:22:36 Finished compiler/backend/proofs                              53m53s  17GB
Jan 03 00:22:36 Starting compiler/encoders/x64/proofs
Jan 03 00:31:57 Finished compiler/encoders/x64/proofs                          9m20s   9GB
Jan 03 00:31:57 Starting compiler/encoders/arm7/proofs
Jan 03 00:44:26 Finished compiler/encoders/arm7/proofs                        12m28s   7GB
Jan 03 00:44:26 Starting compiler/encoders/arm8/proofs
Jan 03 00:50:40 Finished compiler/encoders/arm8/proofs                         6m13s   3GB
Jan 03 00:50:40 Starting compiler/encoders/mips/proofs
Jan 03 01:00:37 Finished compiler/encoders/mips/proofs                         9m57s   6GB
Jan 03 01:00:38 Starting compiler/encoders/riscv/proofs
Jan 03 01:08:58 Finished compiler/encoders/riscv/proofs                        8m20s   3GB
Jan 03 01:08:59 Starting compiler/encoders/ag32/proofs
Jan 03 01:11:22 Finished compiler/encoders/ag32/proofs                         2m23s   1GB
Jan 03 01:11:22 Starting compiler/backend/x64/proofs
Jan 03 01:11:44 Finished compiler/backend/x64/proofs                             21s   2GB
Jan 03 01:11:44 Starting compiler/backend/arm7/proofs
Jan 03 01:12:07 Finished compiler/backend/arm7/proofs                            22s   1GB
Jan 03 01:12:07 Starting compiler/backend/arm8/proofs
Jan 03 01:12:27 Finished compiler/backend/arm8/proofs                            20s   1GB
Jan 03 01:12:27 Starting compiler/backend/mips/proofs
Jan 03 01:12:49 Finished compiler/backend/mips/proofs                            21s   1GB
Jan 03 01:12:49 Starting compiler/backend/riscv/proofs
Jan 03 01:13:11 Finished compiler/backend/riscv/proofs                           21s   2GB
Jan 03 01:13:11 Starting compiler/backend/ag32/proofs
Jan 03 01:25:15 Finished compiler/backend/ag32/proofs                         12m03s   4GB
Jan 03 01:25:15 Starting compiler/proofs
Jan 03 01:26:55 Finished compiler/proofs                                       1m39s   6GB
Jan 03 01:26:55 Starting candle/set-theory
Jan 03 01:27:25 Finished candle/set-theory                                       30s   1GB
Jan 03 01:27:25 Starting candle/syntax-lib
Jan 03 01:27:36 Finished candle/syntax-lib                                       11s 787MB
Jan 03 01:27:37 Starting candle/standard/syntax
Jan 03 01:29:26 Finished candle/standard/syntax                                1m49s   1GB
Jan 03 01:29:26 Starting candle/standard/semantics
Jan 03 01:31:13 Finished candle/standard/semantics                             1m47s   2GB
Jan 03 01:31:14 Starting candle/standard/monadic
Jan 03 01:32:56 Finished candle/standard/monadic                               1m42s   1GB
Jan 03 01:32:56 Starting candle/standard/ml_kernel
Jan 03 01:38:08 Finished candle/standard/ml_kernel                             5m11s   6GB
Jan 03 01:38:08 Starting candle/overloading/syntax
Jan 03 01:41:18 Finished candle/overloading/syntax                             3m09s   1GB
Jan 03 01:41:18 Starting candle/overloading/semantics
Jan 03 01:53:30 Finished candle/overloading/semantics                         12m11s   8GB
Jan 03 01:53:30 Starting characteristic/examples
Jan 03 01:54:49 Finished characteristic/examples                               1m18s   4GB
Jan 03 01:54:49 Starting tutorial/solutions
Jan 03 02:10:08 Finished tutorial/solutions                                   15m18s  16GB
Jan 03 02:10:08 Starting translator/monadic/examples
Jan 03 02:13:28 Finished translator/monadic/examples                           3m20s   3GB
Jan 03 02:13:28 Starting examples
Jan 03 02:21:59 Finished examples                                              8m30s   7GB
Jan 03 02:21:59 Starting examples/compilation/x64
Jan 03 04:45:38 Finished examples/compilation/x64                           2h23m38s  22GB
Jan 03 04:45:38 Starting examples/compilation/x64/proofs
Jan 03 04:47:32 Finished examples/compilation/x64/proofs                       1m53s   3GB
Jan 03 04:47:32 Starting examples/compilation/ag32
Jan 03 05:21:15 Finished examples/compilation/ag32                            33m43s  11GB
Jan 03 05:21:15 Starting examples/compilation/ag32/proofs
Jan 03 05:22:07 Finished examples/compilation/ag32/proofs                        52s   4GB
Jan 03 05:22:08 Starting examples/cost
Jan 03 06:15:36 Finished examples/cost                                        53m28s  21GB
Jan 03 06:15:37 Starting examples/lpr_checker
Jan 03 06:19:26 Finished examples/lpr_checker                                  3m49s   3GB
Jan 03 06:19:26 Starting examples/lpr_checker/compilation
Jan 03 06:38:20 Finished examples/lpr_checker/compilation                     18m54s  14GB
Jan 03 06:38:20 Starting examples/lpr_checker/compilation/proofs
Jan 03 06:39:03 Finished examples/lpr_checker/compilation/proofs                 42s   4GB
Jan 03 06:39:03 Starting examples/lpr_checker/array
Jan 03 06:52:44 Finished examples/lpr_checker/array                           13m40s   5GB
Jan 03 06:52:44 Starting examples/lpr_checker/array/compilation
Jan 03 07:13:21 Finished examples/lpr_checker/array/compilation               20m37s  16GB
Jan 03 07:13:21 Starting examples/lpr_checker/array/compilation/proofs
Jan 03 07:14:11 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Jan 03 07:14:11 Starting examples/opentheory
Jan 03 07:23:23 Finished examples/opentheory                                   9m11s   6GB
Jan 03 07:23:24 Starting examples/opentheory
Jan 03 07:23:24 Finished examples/opentheory                                      0s 100MB
Jan 03 07:23:25 Starting examples/opentheory/compilation
Jan 03 07:54:40 Finished examples/opentheory/compilation                      31m15s  24GB
Jan 03 07:54:40 Starting examples/opentheory/compilation/proofs
Jan 03 07:55:24 Finished examples/opentheory/compilation/proofs                  43s   4GB
Jan 03 07:55:24 Starting examples/opentheory/compilation/ag32
Jan 03 08:28:11 Finished examples/opentheory/compilation/ag32                 32m46s  23GB
Jan 03 08:28:11 Starting examples/opentheory/compilation/ag32/proofs
Jan 03 08:29:43 Finished examples/opentheory/compilation/ag32/proofs           1m31s   7GB
Jan 03 08:29:43 Starting translator/okasaki-examples
Jan 03 08:33:52 Finished translator/okasaki-examples                           4m08s   2GB
Jan 03 08:33:52 Starting translator/other-examples
Jan 03 08:34:37 Finished translator/other-examples                               44s   2GB
Jan 03 08:34:37 Starting compiler/parsing/tests
Jan 03 08:35:01 Finished compiler/parsing/tests                                  23s 638MB
Jan 03 08:35:01 Starting compiler/inference/tests
Jan 03 08:42:13 Finished compiler/inference/tests                              7m11s   6GB
Jan 03 08:42:13 Starting compiler/bootstrap/translation
Jan 03 11:24:32 Finished compiler/bootstrap/translation                     2h42m17s  55GB
Jan 03 11:24:32 Starting unverified/sexpr-bootstrap/x64/64
Jan 03 11:36:37 Finished unverified/sexpr-bootstrap/x64/64                    12m04s   8GB
Jan 03 11:36:37 Starting unverified/sexpr-bootstrap/x64/32
Jan 03 11:47:10 Finished unverified/sexpr-bootstrap/x64/32                    10m33s   8GB
Jan 03 11:47:11 Starting compiler/benchmarks
Jan 03 12:24:55 Finished compiler/benchmarks                                  37m44s   2GB
Jan 03 12:24:56 Starting compiler/bootstrap/compilation/x64/64
Jan 04 04:01:52 Finished compiler/bootstrap/compilation/x64/64             15h36m55s  64GB
Jan 04 04:01:52 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 04 04:04:25 Finished compiler/bootstrap/compilation/x64/64/proofs          2m32s  20GB
Jan 04 04:04:25 Starting compiler/bootstrap/compilation/x64/32
Jan 04 18:28:32 Finished compiler/bootstrap/compilation/x64/32             14h24m06s  64GB
Jan 04 18:28:32 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 04 18:30:35 Finished compiler/bootstrap/compilation/x64/32/proofs          2m02s  14GB
Jan 04 18:30:35 Starting compiler/bootstrap/compilation/ag32/32
Jan 05 09:53:15 Finished compiler/bootstrap/compilation/ag32/32            15h22m40s  64GB
Jan 05 09:53:15 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 05 10:02:47 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m31s  56GB
Jan 05 10:02:47 SUCCESS