Job 1425

CakeML: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
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Dec 31 06:25:48 Claimed job
Dec 31 06:25:50 Reusing HOL
Dec 31 06:25:55 Starting developers
Dec 31 06:25:58 Finished developers                                               2s  97MB
Dec 31 06:25:58 Starting developers/bin
Dec 31 06:26:04 Finished developers/bin                                           5s   1GB
Dec 31 06:26:04 Starting semantics/ffi
Dec 31 06:26:14 Finished semantics/ffi                                            9s 284MB
Dec 31 06:26:14 Starting semantics
Dec 31 06:27:39 Finished semantics                                             1m24s   1GB
Dec 31 06:27:39 Starting semantics/proofs
Dec 31 06:31:00 Finished semantics/proofs                                      3m20s   2GB
Dec 31 06:31:00 Starting semantics/alt_semantics
Dec 31 06:31:08 Finished semantics/alt_semantics                                  7s 402MB
Dec 31 06:31:08 Starting semantics/alt_semantics/proofs
Dec 31 06:33:15 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Dec 31 06:33:16 Starting basis/pure
Dec 31 06:34:08 Finished basis/pure                                              52s   1GB
Dec 31 06:34:08 Starting translator
Dec 31 06:36:47 Finished translator                                            2m38s   2GB
Dec 31 06:36:47 Starting compiler/parsing
Dec 31 06:37:55 Finished compiler/parsing                                      1m08s   4GB
Dec 31 06:37:56 Starting characteristic
Dec 31 06:43:53 Finished characteristic                                        5m57s   2GB
Dec 31 06:43:53 Starting translator/monadic
Dec 31 06:45:37 Finished translator/monadic                                    1m44s   3GB
Dec 31 06:45:38 Starting basis
Dec 31 07:19:01 Finished basis                                                33m23s  35GB
Dec 31 07:19:02 Starting compiler/inference
Dec 31 07:20:05 Finished compiler/inference                                    1m03s   1GB
Dec 31 07:20:05 Starting compiler/backend/reg_alloc
Dec 31 07:21:09 Finished compiler/backend/reg_alloc                            1m03s   1GB
Dec 31 07:21:09 Starting compiler/backend/gc
Dec 31 07:24:29 Finished compiler/backend/gc                                   3m19s   3GB
Dec 31 07:24:29 Starting compiler/backend
Dec 31 07:29:23 Finished compiler/backend                                      4m53s   4GB
Dec 31 07:29:23 Starting compiler/encoders/asm
Dec 31 07:29:45 Finished compiler/encoders/asm                                   21s   1GB
Dec 31 07:29:45 Starting compiler/encoders/x64
Dec 31 07:30:12 Finished compiler/encoders/x64                                   26s   1GB
Dec 31 07:30:12 Starting compiler/encoders/arm7
Dec 31 07:31:03 Finished compiler/encoders/arm7                                  50s   1GB
Dec 31 07:31:03 Starting compiler/encoders/arm8
Dec 31 07:31:16 Finished compiler/encoders/arm8                                  13s   1GB
Dec 31 07:31:16 Starting compiler/encoders/mips
Dec 31 07:31:35 Finished compiler/encoders/mips                                  18s   1GB
Dec 31 07:31:35 Starting compiler/encoders/riscv
Dec 31 07:31:51 Finished compiler/encoders/riscv                                 15s   1GB
Dec 31 07:31:51 Starting compiler/encoders/ag32
Dec 31 07:32:09 Finished compiler/encoders/ag32                                  17s 962MB
Dec 31 07:32:09 Starting compiler/backend/x64
Dec 31 07:32:29 Finished compiler/backend/x64                                    19s   1GB
Dec 31 07:32:29 Starting compiler/backend/arm7
Dec 31 07:32:50 Finished compiler/backend/arm7                                   20s   1GB
Dec 31 07:32:50 Starting compiler/backend/arm8
Dec 31 07:33:10 Finished compiler/backend/arm8                                   19s   1GB
Dec 31 07:33:11 Starting compiler/backend/mips
Dec 31 07:33:31 Finished compiler/backend/mips                                   20s   1GB
Dec 31 07:33:31 Starting compiler/backend/riscv
Dec 31 07:33:52 Finished compiler/backend/riscv                                  20s   1GB
Dec 31 07:33:52 Starting compiler/backend/ag32
Dec 31 07:35:01 Finished compiler/backend/ag32                                 1m08s   1GB
Dec 31 07:35:01 Starting compiler/parsing/proofs
Dec 31 07:40:38 Finished compiler/parsing/proofs                               5m37s   2GB
Dec 31 07:40:38 Starting compiler/inference/proofs
Dec 31 07:43:10 Finished compiler/inference/proofs                             2m31s   2GB
Dec 31 07:43:10 Starting compiler/backend/semantics
Dec 31 08:10:18 Finished compiler/backend/semantics                           27m07s   3GB
Dec 31 08:10:18 Starting compiler/backend/reg_alloc/proofs
Dec 31 08:13:36 Finished compiler/backend/reg_alloc/proofs                     3m17s   1GB
Dec 31 08:13:36 Starting compiler/backend/proofs
Dec 31 09:07:24 Finished compiler/backend/proofs                              53m48s  15GB
Dec 31 09:07:25 Starting compiler/encoders/x64/proofs
Dec 31 09:16:45 Finished compiler/encoders/x64/proofs                          9m19s   7GB
Dec 31 09:16:45 Starting compiler/encoders/arm7/proofs
Dec 31 09:29:23 Finished compiler/encoders/arm7/proofs                        12m38s   5GB
Dec 31 09:29:23 Starting compiler/encoders/arm8/proofs
Dec 31 09:35:42 Finished compiler/encoders/arm8/proofs                         6m17s   3GB
Dec 31 09:35:42 Starting compiler/encoders/mips/proofs
Dec 31 09:45:33 Finished compiler/encoders/mips/proofs                         9m51s   3GB
Dec 31 09:45:34 Starting compiler/encoders/riscv/proofs
Dec 31 09:53:52 Finished compiler/encoders/riscv/proofs                        8m18s   4GB
Dec 31 09:53:52 Starting compiler/encoders/ag32/proofs
Dec 31 09:56:14 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Dec 31 09:56:14 Starting compiler/backend/x64/proofs
Dec 31 09:56:35 Finished compiler/backend/x64/proofs                             21s   1GB
Dec 31 09:56:36 Starting compiler/backend/arm7/proofs
Dec 31 09:57:00 Finished compiler/backend/arm7/proofs                            24s   2GB
Dec 31 09:57:00 Starting compiler/backend/arm8/proofs
Dec 31 09:57:20 Finished compiler/backend/arm8/proofs                            20s   1GB
Dec 31 09:57:20 Starting compiler/backend/mips/proofs
Dec 31 09:57:42 Finished compiler/backend/mips/proofs                            21s   1GB
Dec 31 09:57:42 Starting compiler/backend/riscv/proofs
Dec 31 09:58:06 Finished compiler/backend/riscv/proofs                           23s   2GB
Dec 31 09:58:06 Starting compiler/backend/ag32/proofs
Dec 31 10:10:04 Finished compiler/backend/ag32/proofs                         11m57s   6GB
Dec 31 10:10:04 Starting compiler/proofs
Dec 31 10:11:43 Finished compiler/proofs                                       1m39s   6GB
Dec 31 10:11:43 Starting candle/set-theory
Dec 31 10:12:13 Finished candle/set-theory                                       29s 882MB
Dec 31 10:12:14 Starting candle/syntax-lib
Dec 31 10:12:25 Finished candle/syntax-lib                                       10s 785MB
Dec 31 10:12:25 Starting candle/standard/syntax
Dec 31 10:14:16 Finished candle/standard/syntax                                1m50s   1GB
Dec 31 10:14:16 Starting candle/standard/semantics
Dec 31 10:16:03 Finished candle/standard/semantics                             1m46s   2GB
Dec 31 10:16:03 Starting candle/standard/monadic
Dec 31 10:17:43 Finished candle/standard/monadic                               1m40s   1GB
Dec 31 10:17:44 Starting candle/standard/ml_kernel
Dec 31 10:22:59 Finished candle/standard/ml_kernel                             5m15s   5GB
Dec 31 10:22:59 Starting candle/overloading/syntax
Dec 31 10:26:09 Finished candle/overloading/syntax                             3m09s   1GB
Dec 31 10:26:09 Starting candle/overloading/semantics
Dec 31 10:38:14 Finished candle/overloading/semantics                         12m04s   8GB
Dec 31 10:38:14 Starting characteristic/examples
Dec 31 10:39:33 Finished characteristic/examples                               1m18s   4GB
Dec 31 10:39:33 Starting tutorial/solutions
Dec 31 10:54:53 Finished tutorial/solutions                                   15m20s  13GB
Dec 31 10:54:53 Starting translator/monadic/examples
Dec 31 10:58:12 Finished translator/monadic/examples                           3m18s   3GB
Dec 31 10:58:13 Starting examples
Dec 31 11:06:50 Finished examples                                              8m37s   6GB
Dec 31 11:06:51 Starting examples/compilation/x64
Dec 31 13:30:50 Finished examples/compilation/x64                           2h23m59s  23GB
Dec 31 13:30:51 Starting examples/compilation/x64/proofs
Dec 31 13:32:44 Finished examples/compilation/x64/proofs                       1m53s   3GB
Dec 31 13:32:44 Starting examples/compilation/ag32
Dec 31 14:06:33 Finished examples/compilation/ag32                            33m48s  10GB
Dec 31 14:06:33 Starting examples/compilation/ag32/proofs
Dec 31 14:07:23 Finished examples/compilation/ag32/proofs                        50s   4GB
Dec 31 14:07:23 Starting examples/cost
Dec 31 15:01:10 Finished examples/cost                                        53m45s  13GB
Dec 31 15:01:10 Starting examples/lpr_checker
Dec 31 15:04:56 Finished examples/lpr_checker                                  3m46s   3GB
Dec 31 15:04:56 Starting examples/lpr_checker/compilation
Dec 31 15:23:42 Finished examples/lpr_checker/compilation                     18m45s  14GB
Dec 31 15:23:42 Starting examples/lpr_checker/compilation/proofs
Dec 31 15:24:24 Finished examples/lpr_checker/compilation/proofs                 41s   3GB
Dec 31 15:24:24 Starting examples/lpr_checker/array
Dec 31 15:38:05 Finished examples/lpr_checker/array                           13m40s   6GB
Dec 31 15:38:05 Starting examples/lpr_checker/array/compilation
Dec 31 15:57:51 Finished examples/lpr_checker/array/compilation               19m46s  28GB
Dec 31 15:57:51 Starting examples/lpr_checker/array/compilation/proofs
Dec 31 15:58:39 Finished examples/lpr_checker/array/compilation/proofs           47s   4GB
Dec 31 15:58:40 Starting examples/opentheory
Dec 31 16:07:52 Finished examples/opentheory                                   9m11s   6GB
Dec 31 16:07:52 Starting examples/opentheory
Dec 31 16:07:53 Finished examples/opentheory                                      0s 100MB
Dec 31 16:07:53 Starting examples/opentheory/compilation
Dec 31 16:39:13 Finished examples/opentheory/compilation                      31m20s  25GB
Dec 31 16:39:13 Starting examples/opentheory/compilation/proofs
Dec 31 16:39:57 Finished examples/opentheory/compilation/proofs                  43s   4GB
Dec 31 16:39:57 Starting examples/opentheory/compilation/ag32
Dec 31 17:13:05 Finished examples/opentheory/compilation/ag32                 33m07s  26GB
Dec 31 17:13:05 Starting examples/opentheory/compilation/ag32/proofs
Dec 31 17:14:42 Finished examples/opentheory/compilation/ag32/proofs           1m36s   8GB
Dec 31 17:14:42 Starting translator/okasaki-examples
Dec 31 17:18:51 Finished translator/okasaki-examples                           4m08s   2GB
Dec 31 17:18:51 Starting translator/other-examples
Dec 31 17:20:53 Finished translator/other-examples                             2m01s   2GB
Dec 31 17:20:53 Starting compiler/parsing/tests
Dec 31 17:21:17 Finished compiler/parsing/tests                                  24s 655MB
Dec 31 17:21:17 Starting compiler/inference/tests
Dec 31 17:28:29 Finished compiler/inference/tests                              7m11s   5GB
Dec 31 17:28:29 Starting compiler/bootstrap/translation
Dec 31 20:12:50 Finished compiler/bootstrap/translation                     2h44m20s  55GB
Dec 31 20:12:51 Starting unverified/sexpr-bootstrap/x64/64
Dec 31 20:24:59 Finished unverified/sexpr-bootstrap/x64/64                    12m07s   8GB
Dec 31 20:24:59 Starting unverified/sexpr-bootstrap/x64/32
Dec 31 20:35:27 Finished unverified/sexpr-bootstrap/x64/32                    10m28s   8GB
Dec 31 20:35:28 Starting compiler/benchmarks
Dec 31 21:13:15 Finished compiler/benchmarks                                  37m46s   2GB
Dec 31 21:13:15 Starting compiler/bootstrap/compilation/x64/64
Jan 01 15:14:57 Finished compiler/bootstrap/compilation/x64/64             18h01m41s  64GB
Jan 01 15:14:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 01 15:17:23 Finished compiler/bootstrap/compilation/x64/64/proofs          2m25s  14GB
Jan 01 15:17:23 Starting compiler/bootstrap/compilation/x64/32
Jan 02 06:04:29 Finished compiler/bootstrap/compilation/x64/32             14h47m03s  64GB
Jan 02 06:04:29 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 02 06:06:43 Finished compiler/bootstrap/compilation/x64/32/proofs          2m13s  18GB
Jan 02 06:06:43 Starting compiler/bootstrap/compilation/ag32/32
Jan 02 21:31:12 Finished compiler/bootstrap/compilation/ag32/32            15h24m28s  64GB
Jan 02 21:31:12 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 02 21:40:37 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m23s  56GB
Jan 02 21:40:37 SUCCESS