Job 1294

CakeML:311f6e9de8151110c5a522b552a599b25d61ddeb
  Merge pull request #738 from CakeML/export_update [Jun 29 08:58:28]
HOL:0aae6443b97e2d1bd0ea728d27ca72d0913aa763
  Prove a chunk of Rutten's Theorem 7.1 (First Isomorphism theorem) [Jun 23 08:07:27]
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

Jun 29 09:04:08 Claimed job
Jun 29 09:04:15 Building HOL
Jun 29 09:16:32 Starting developers
Jun 29 09:16:32 Finished developers                                               0s  32MB
Jun 29 09:16:32 Starting developers/bin
Jun 29 09:16:38 Finished developers/bin                                           5s   1GB
Jun 29 09:16:39 Starting semantics/ffi
Jun 29 09:16:48 Finished semantics/ffi                                            8s 263MB
Jun 29 09:16:48 Starting semantics
Jun 29 09:18:16 Finished semantics                                             1m28s 917MB
Jun 29 09:18:16 Starting semantics/proofs
Jun 29 09:21:29 Finished semantics/proofs                                      3m12s 977MB
Jun 29 09:21:29 Starting semantics/alt_semantics
Jun 29 09:21:37 Finished semantics/alt_semantics                                  7s 334MB
Jun 29 09:21:37 Starting semantics/alt_semantics/proofs
Jun 29 09:23:41 Finished semantics/alt_semantics/proofs                        2m03s 846MB
Jun 29 09:23:41 Starting basis/pure
Jun 29 09:26:27 Finished basis/pure                                            2m45s 852MB
Jun 29 09:26:27 Starting translator
Jun 29 09:29:03 Finished translator                                            2m35s   1GB
Jun 29 09:29:03 Starting compiler/parsing
Jun 29 09:30:11 Finished compiler/parsing                                      1m07s   2GB
Jun 29 09:30:11 Starting characteristic
Jun 29 09:35:52 Finished characteristic                                        5m41s   2GB
Jun 29 09:35:52 Starting translator/monadic
Jun 29 09:37:26 Finished translator/monadic                                    1m33s   1GB
Jun 29 09:37:26 Starting basis
Jun 29 10:08:20 Finished basis                                                30m53s  13GB
Jun 29 10:08:20 Starting compiler/inference
Jun 29 10:09:25 Finished compiler/inference                                    1m05s   1GB
Jun 29 10:09:25 Starting compiler/backend/reg_alloc
Jun 29 10:10:29 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jun 29 10:10:29 Starting compiler/backend/gc
Jun 29 10:13:54 Finished compiler/backend/gc                                   3m24s   2GB
Jun 29 10:13:54 Starting compiler/backend
Jun 29 10:18:29 Finished compiler/backend                                      4m34s   4GB
Jun 29 10:18:29 Starting compiler/encoders/asm
Jun 29 10:18:50 Finished compiler/encoders/asm                                   21s 723MB
Jun 29 10:18:51 Starting compiler/encoders/x64
Jun 29 10:19:47 Finished compiler/encoders/x64                                   56s 780MB
Jun 29 10:19:47 Starting compiler/encoders/arm7
Jun 29 10:21:36 Finished compiler/encoders/arm7                                1m48s   1GB
Jun 29 10:21:36 Starting compiler/encoders/arm8
Jun 29 10:22:10 Finished compiler/encoders/arm8                                  34s 934MB
Jun 29 10:22:10 Starting compiler/encoders/mips
Jun 29 10:23:24 Finished compiler/encoders/mips                                1m13s   1GB
Jun 29 10:23:24 Starting compiler/encoders/riscv
Jun 29 10:24:52 Finished compiler/encoders/riscv                               1m27s   1GB
Jun 29 10:24:52 Starting compiler/encoders/ag32
Jun 29 10:25:09 Finished compiler/encoders/ag32                                  16s 859MB
Jun 29 10:25:09 Starting compiler/backend/x64
Jun 29 10:25:27 Finished compiler/backend/x64                                    17s   1GB
Jun 29 10:25:27 Starting compiler/backend/arm7
Jun 29 10:25:47 Finished compiler/backend/arm7                                   20s   1GB
Jun 29 10:25:47 Starting compiler/backend/arm8
Jun 29 10:26:04 Finished compiler/backend/arm8                                   16s   1GB
Jun 29 10:26:04 Starting compiler/backend/mips
Jun 29 10:26:23 Finished compiler/backend/mips                                   18s   1GB
Jun 29 10:26:23 Starting compiler/backend/riscv
Jun 29 10:26:42 Finished compiler/backend/riscv                                  18s   1GB
Jun 29 10:26:42 Starting compiler/backend/ag32
Jun 29 10:27:50 Finished compiler/backend/ag32                                 1m07s   1GB
Jun 29 10:27:50 Starting compiler/parsing/proofs
Jun 29 10:33:28 Finished compiler/parsing/proofs                               5m37s   1GB
Jun 29 10:33:28 Starting compiler/inference/proofs
Jun 29 10:35:53 Finished compiler/inference/proofs                             2m24s   1GB
Jun 29 10:35:53 Starting compiler/backend/semantics
Jun 29 11:03:12 Finished compiler/backend/semantics                           27m18s   2GB
Jun 29 11:03:12 Starting compiler/backend/reg_alloc/proofs
Jun 29 11:06:32 Finished compiler/backend/reg_alloc/proofs                     3m20s   1GB
Jun 29 11:06:32 Starting compiler/backend/proofs
Jun 29 11:59:45 Finished compiler/backend/proofs                              53m12s  19GB
Jun 29 11:59:45 Starting compiler/encoders/x64/proofs
Jun 29 12:09:06 Finished compiler/encoders/x64/proofs                          9m20s   4GB
Jun 29 12:09:06 Starting compiler/encoders/arm7/proofs
Jun 29 12:21:35 Finished compiler/encoders/arm7/proofs                        12m29s   3GB
Jun 29 12:21:35 Starting compiler/encoders/arm8/proofs
Jun 29 12:27:54 Finished compiler/encoders/arm8/proofs                         6m18s   1GB
Jun 29 12:27:54 Starting compiler/encoders/mips/proofs
Jun 29 12:37:30 Finished compiler/encoders/mips/proofs                         9m35s   3GB
Jun 29 12:37:30 Starting compiler/encoders/riscv/proofs
Jun 29 12:45:59 Finished compiler/encoders/riscv/proofs                        8m29s   1GB
Jun 29 12:45:59 Starting compiler/encoders/ag32/proofs
Jun 29 12:48:29 Finished compiler/encoders/ag32/proofs                         2m29s 746MB
Jun 29 12:48:29 Starting compiler/backend/x64/proofs
Jun 29 12:48:49 Finished compiler/backend/x64/proofs                             19s   1GB
Jun 29 12:48:49 Starting compiler/backend/arm7/proofs
Jun 29 12:49:11 Finished compiler/backend/arm7/proofs                            22s 896MB
Jun 29 12:49:11 Starting compiler/backend/arm8/proofs
Jun 29 12:49:31 Finished compiler/backend/arm8/proofs                            19s   1GB
Jun 29 12:49:31 Starting compiler/backend/mips/proofs
Jun 29 12:49:51 Finished compiler/backend/mips/proofs                            19s   1GB
Jun 29 12:49:51 Starting compiler/backend/riscv/proofs
Jun 29 12:50:11 Finished compiler/backend/riscv/proofs                           20s   1GB
Jun 29 12:50:11 Starting compiler/backend/ag32/proofs
Jun 29 13:02:36 Finished compiler/backend/ag32/proofs                         12m24s   1GB
Jun 29 13:02:36 Starting compiler/proofs
Jun 29 13:04:19 Finished compiler/proofs                                       1m42s   2GB
Jun 29 13:04:19 Starting candle/set-theory
Jun 29 13:04:47 Finished candle/set-theory                                       27s 740MB
Jun 29 13:04:47 Starting candle/syntax-lib
Jun 29 13:04:58 Finished candle/syntax-lib                                       10s 522MB
Jun 29 13:04:58 Starting candle/standard/syntax
Jun 29 13:06:44 Finished candle/standard/syntax                                1m45s 976MB
Jun 29 13:06:44 Starting candle/standard/semantics
Jun 29 13:08:23 Finished candle/standard/semantics                             1m39s   1GB
Jun 29 13:08:23 Starting candle/standard/monadic
Jun 29 13:10:02 Finished candle/standard/monadic                               1m38s   1GB
Jun 29 13:10:02 Starting candle/standard/ml_kernel
Jun 29 13:15:21 Finished candle/standard/ml_kernel                             5m19s   7GB
Jun 29 13:15:22 Starting candle/standard/opentheory
Jun 29 13:24:08 Finished candle/standard/opentheory                            8m46s   4GB
Jun 29 13:24:08 Starting candle/standard/opentheory/compilation
Jun 29 13:55:15 Finished candle/standard/opentheory/compilation               31m06s  17GB
Jun 29 13:55:15 Starting candle/standard/opentheory/compilation/proofs
Jun 29 13:55:54 Finished candle/standard/opentheory/compilation/proofs           38s   3GB
Jun 29 13:55:54 Starting candle/overloading/syntax
Jun 29 13:58:53 Finished candle/overloading/syntax                             2m59s   1GB
Jun 29 13:58:53 Starting candle/overloading/semantics
Jun 29 14:05:44 Finished candle/overloading/semantics                          6m50s   2GB
Jun 29 14:05:45 Starting characteristic/examples
Jun 29 14:06:58 Finished characteristic/examples                               1m13s   3GB
Jun 29 14:06:58 Starting tutorial/solutions
Jun 29 14:21:00 Finished tutorial/solutions                                   14m01s   7GB
Jun 29 14:21:00 Starting translator/monadic/examples
Jun 29 14:24:10 Finished translator/monadic/examples                           3m10s   2GB
Jun 29 14:24:11 Starting examples
Jun 29 14:32:23 Finished examples                                              8m12s   3GB
Jun 29 14:32:23 Starting examples/compilation/x64
Jun 29 16:46:10 Finished examples/compilation/x64                           2h13m47s  22GB
Jun 29 16:46:11 Starting examples/compilation/x64/proofs
Jun 29 16:47:44 Finished examples/compilation/x64/proofs                       1m33s   2GB
Jun 29 16:47:45 Starting examples/compilation/ag32
Jun 29 17:18:04 Finished examples/compilation/ag32                            30m19s   6GB
Jun 29 17:18:04 Starting examples/compilation/ag32/proofs
Jun 29 17:18:46 Finished examples/compilation/ag32/proofs                        41s   2GB
Jun 29 17:18:46 Starting examples/cost
Jun 29 18:04:39 Finished examples/cost                                        45m53s   6GB
Jun 29 18:04:39 Starting examples/lpr_checker
Jun 29 18:08:27 Finished examples/lpr_checker                                  3m47s   4GB
Jun 29 18:08:27 Starting examples/lpr_checker/compilation
Jun 29 18:25:24 Finished examples/lpr_checker/compilation                     16m56s  14GB
Jun 29 18:25:24 Starting examples/lpr_checker/compilation/proofs
Jun 29 18:26:02 Finished examples/lpr_checker/compilation/proofs                 37s   2GB
Jun 29 18:26:02 Starting examples/lpr_checker/array
Jun 29 18:35:45 Finished examples/lpr_checker/array                            9m42s   4GB
Jun 29 18:35:45 Starting examples/lpr_checker/array/compilation
Jun 29 18:53:58 Finished examples/lpr_checker/array/compilation               18m12s  10GB
Jun 29 18:53:58 Starting examples/lpr_checker/array/compilation/proofs
Jun 29 18:54:42 Finished examples/lpr_checker/array/compilation/proofs           43s   2GB
Jun 29 18:54:42 Starting translator/okasaki-examples
Jun 29 18:58:57 Finished translator/okasaki-examples                           4m14s   1GB
Jun 29 18:58:57 Starting translator/other-examples
Jun 29 19:00:51 Finished translator/other-examples                             1m53s   1GB
Jun 29 19:00:51 Starting compiler/parsing/tests
Jun 29 19:01:16 Finished compiler/parsing/tests                                  25s 679MB
Jun 29 19:01:16 Starting compiler/inference/tests
Jun 29 19:05:48 Finished compiler/inference/tests                              4m31s   4GB
Jun 29 19:05:48 Starting compiler/bootstrap/translation
Jun 29 21:39:04 Finished compiler/bootstrap/translation                     2h33m15s  42GB
Jun 29 21:39:04 Starting unverified/sexpr-bootstrap/x64/64
Jun 29 21:48:33 Finished unverified/sexpr-bootstrap/x64/64                     9m27s   8GB
Jun 29 21:48:33 Starting unverified/sexpr-bootstrap/x64/32
Jun 29 21:56:11 Finished unverified/sexpr-bootstrap/x64/32                     7m37s   8GB
Jun 29 21:56:11 Starting compiler/benchmarks
Jun 29 22:35:02 Finished compiler/benchmarks                                  38m50s   2GB
Jun 29 22:35:02 Starting compiler/bootstrap/compilation/x64/64
Jun 30 13:07:20 Finished compiler/bootstrap/compilation/x64/64             14h32m16s  64GB
Jun 30 13:07:20 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 30 13:10:40 Finished compiler/bootstrap/compilation/x64/64/proofs          3m19s  14GB
Jun 30 13:10:40 Starting compiler/bootstrap/compilation/x64/32
Jul 01 02:20:34 Finished compiler/bootstrap/compilation/x64/32             13h09m53s  64GB
Jul 01 02:20:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 01 02:23:35 Finished compiler/bootstrap/compilation/x64/32/proofs          3m00s  12GB
Jul 01 02:23:35 Starting compiler/bootstrap/compilation/ag32/32
Jul 01 17:38:43 Finished compiler/bootstrap/compilation/ag32/32            15h15m06s  64GB
Jul 01 17:38:43 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 01 18:08:58 Finished compiler/bootstrap/compilation/ag32/32/proofs        30m14s  25GB
Jul 01 18:08:58 SUCCESS