Job 1295

CakeML:cc5ed8c9e8e71417da0d2d8a7867d0e4a3331beb
  comments describing memory layout in basis_ffi.c [Jun 29 14:46:03]
HOL:0aae6443b97e2d1bd0ea728d27ca72d0913aa763
  Prove a chunk of Rutten's Theorem 7.1 (First Isomorphism theorem) [Jun 23 08:07:27]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64
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 14:55:04 Claimed job
Jun 29 14:55:11 Reusing HOL
Jun 29 14:55:58 Starting developers
Jun 29 14:56:02 Finished developers                                               4s  84MB
Jun 29 14:56:02 Starting developers/bin
Jun 29 14:56:10 Finished developers/bin                                           7s   1GB
Jun 29 14:56:10 Starting semantics/ffi
Jun 29 14:56:23 Finished semantics/ffi                                           13s 243MB
Jun 29 14:56:23 Starting semantics
Jun 29 14:57:58 Finished semantics                                             1m34s   1GB
Jun 29 14:57:58 Starting semantics/proofs
Jun 29 15:01:43 Finished semantics/proofs                                      3m44s   1GB
Jun 29 15:01:43 Starting semantics/alt_semantics
Jun 29 15:01:53 Finished semantics/alt_semantics                                  9s 293MB
Jun 29 15:01:53 Starting semantics/alt_semantics/proofs
Jun 29 15:04:14 Finished semantics/alt_semantics/proofs                        2m20s   1GB
Jun 29 15:04:14 Starting basis/pure
Jun 29 15:05:09 Finished basis/pure                                              55s 793MB
Jun 29 15:05:09 Starting translator
Jun 29 15:08:10 Finished translator                                            3m00s   1GB
Jun 29 15:08:11 Starting compiler/parsing
Jun 29 15:09:36 Finished compiler/parsing                                      1m25s   2GB
Jun 29 15:09:36 Starting characteristic
Jun 29 15:16:10 Finished characteristic                                        6m33s   2GB
Jun 29 15:16:10 Starting translator/monadic
Jun 29 15:17:55 Finished translator/monadic                                    1m45s   1GB
Jun 29 15:17:55 Starting basis
Jun 29 15:54:37 Finished basis                                                36m41s  15GB
Jun 29 15:54:38 Starting compiler/inference
Jun 29 15:55:47 Finished compiler/inference                                    1m09s   1GB
Jun 29 15:55:47 Starting compiler/backend/reg_alloc
Jun 29 15:56:59 Finished compiler/backend/reg_alloc                            1m11s   1GB
Jun 29 15:56:59 Starting compiler/backend/gc
Jun 29 16:00:56 Finished compiler/backend/gc                                   3m56s   2GB
Jun 29 16:00:56 Starting compiler/backend
Jun 29 16:06:28 Finished compiler/backend                                      5m32s   4GB
Jun 29 16:06:28 Starting compiler/encoders/asm
Jun 29 16:06:53 Finished compiler/encoders/asm                                   24s 665MB
Jun 29 16:06:53 Starting compiler/encoders/x64
Jun 29 16:07:20 Finished compiler/encoders/x64                                   27s 876MB
Jun 29 16:07:21 Starting compiler/encoders/arm7
Jun 29 16:08:14 Finished compiler/encoders/arm7                                  53s 701MB
Jun 29 16:08:14 Starting compiler/encoders/arm8
Jun 29 16:08:28 Finished compiler/encoders/arm8                                  14s 935MB
Jun 29 16:08:29 Starting compiler/encoders/mips
Jun 29 16:08:48 Finished compiler/encoders/mips                                  19s   1GB
Jun 29 16:08:48 Starting compiler/encoders/riscv
Jun 29 16:09:05 Finished compiler/encoders/riscv                                 17s 754MB
Jun 29 16:09:05 Starting compiler/encoders/ag32
Jun 29 16:09:26 Finished compiler/encoders/ag32                                  20s 591MB
Jun 29 16:09:26 Starting compiler/backend/x64
Jun 29 16:09:45 Finished compiler/backend/x64                                    19s 964MB
Jun 29 16:09:46 Starting compiler/backend/arm7
Jun 29 16:10:08 Finished compiler/backend/arm7                                   22s   1GB
Jun 29 16:10:08 Starting compiler/backend/arm8
Jun 29 16:10:29 Finished compiler/backend/arm8                                   20s   1GB
Jun 29 16:10:30 Starting compiler/backend/mips
Jun 29 16:10:51 Finished compiler/backend/mips                                   21s   1GB
Jun 29 16:10:52 Starting compiler/backend/riscv
Jun 29 16:11:13 Finished compiler/backend/riscv                                  20s   1GB
Jun 29 16:11:13 Starting compiler/backend/ag32
Jun 29 16:12:30 Finished compiler/backend/ag32                                 1m17s   1GB
Jun 29 16:12:30 Starting compiler/parsing/proofs
Jun 29 16:18:35 Finished compiler/parsing/proofs                               6m03s   1GB
Jun 29 16:18:35 Starting compiler/inference/proofs
Jun 29 16:21:24 Finished compiler/inference/proofs                             2m48s   1GB
Jun 29 16:21:24 Starting compiler/backend/semantics
Jun 29 16:55:22 Finished compiler/backend/semantics                           33m58s   2GB
Jun 29 16:55:22 Starting compiler/backend/reg_alloc/proofs
Jun 29 16:59:17 Finished compiler/backend/reg_alloc/proofs                     3m55s   1GB
Jun 29 16:59:18 Starting compiler/backend/proofs
Jun 29 18:07:44 Finished compiler/backend/proofs                            1h08m26s  14GB
Jun 29 18:07:44 Starting compiler/encoders/x64/proofs
Jun 29 18:18:32 Finished compiler/encoders/x64/proofs                         10m48s   4GB
Jun 29 18:18:32 Starting compiler/encoders/arm7/proofs
Jun 29 18:32:54 Finished compiler/encoders/arm7/proofs                        14m21s   3GB
Jun 29 18:32:54 Starting compiler/encoders/arm8/proofs
Jun 29 18:40:11 Finished compiler/encoders/arm8/proofs                         7m16s   1GB
Jun 29 18:40:11 Starting compiler/encoders/mips/proofs
Jun 29 18:51:19 Finished compiler/encoders/mips/proofs                        11m07s   2GB
Jun 29 18:51:19 Starting compiler/encoders/riscv/proofs
Jun 29 19:00:52 Finished compiler/encoders/riscv/proofs                        9m33s   1GB
Jun 29 19:00:52 Starting compiler/encoders/ag32/proofs
Jun 29 19:03:47 Finished compiler/encoders/ag32/proofs                         2m54s 691MB
Jun 29 19:03:47 Starting compiler/backend/x64/proofs
Jun 29 19:04:09 Finished compiler/backend/x64/proofs                             21s   1GB
Jun 29 19:04:09 Starting compiler/backend/arm7/proofs
Jun 29 19:04:33 Finished compiler/backend/arm7/proofs                            23s   1GB
Jun 29 19:04:33 Starting compiler/backend/arm8/proofs
Jun 29 19:04:54 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 29 19:04:55 Starting compiler/backend/mips/proofs
Jun 29 19:05:18 Finished compiler/backend/mips/proofs                            23s   1GB
Jun 29 19:05:18 Starting compiler/backend/riscv/proofs
Jun 29 19:05:40 Finished compiler/backend/riscv/proofs                           21s   1GB
Jun 29 19:05:40 Starting compiler/backend/ag32/proofs
Jun 29 19:20:15 Finished compiler/backend/ag32/proofs                         14m34s   2GB
Jun 29 19:20:16 Starting compiler/proofs
Jun 29 19:21:55 Finished compiler/proofs                                       1m39s   3GB
Jun 29 19:21:55 Starting candle/set-theory
Jun 29 19:22:27 Finished candle/set-theory                                       31s 721MB
Jun 29 19:22:27 Starting candle/syntax-lib
Jun 29 19:22:39 Finished candle/syntax-lib                                       11s 684MB
Jun 29 19:22:39 Starting candle/standard/syntax
Jun 29 19:24:41 Finished candle/standard/syntax                                2m01s   1GB
Jun 29 19:24:41 Starting candle/standard/semantics
Jun 29 19:26:36 Finished candle/standard/semantics                             1m54s   1GB
Jun 29 19:26:36 Starting candle/standard/monadic
Jun 29 19:28:30 Finished candle/standard/monadic                               1m53s   1GB
Jun 29 19:28:30 Starting candle/standard/ml_kernel
Jun 29 19:34:29 Finished candle/standard/ml_kernel                             5m58s   5GB
Jun 29 19:34:29 Starting candle/standard/opentheory
Jun 29 19:44:57 Finished candle/standard/opentheory                           10m27s   4GB
Jun 29 19:44:57 Starting candle/standard/opentheory/compilation
Jun 29 20:19:29 Finished candle/standard/opentheory/compilation               34m31s  21GB
Jun 29 20:19:29 Starting candle/standard/opentheory/compilation/proofs
Jun 29 20:20:32 Finished candle/standard/opentheory/compilation/proofs         1m03s   1GB
Jun 29 20:20:33 Starting candle/overloading/syntax
Jun 29 20:23:59 Finished candle/overloading/syntax                             3m26s   1GB
Jun 29 20:23:59 Starting candle/overloading/semantics
Jun 29 20:31:45 Finished candle/overloading/semantics                          7m43s   3GB
Jun 29 20:31:45 Starting characteristic/examples
Jun 29 20:33:08 Finished characteristic/examples                               1m22s   2GB
Jun 29 20:33:08 Starting tutorial/solutions
Jun 29 20:48:36 Finished tutorial/solutions                                   15m27s   6GB
Jun 29 20:48:36 Starting translator/monadic/examples
Jun 29 20:52:31 Finished translator/monadic/examples                           3m54s   2GB
Jun 29 20:52:31 Starting examples
Jun 29 21:02:59 Finished examples                                             10m27s   3GB
Jun 29 21:02:59 Starting examples/compilation/x64
Jun 29 23:30:48 Finished examples/compilation/x64                           2h27m48s  16GB
Jun 29 23:30:48 Starting examples/compilation/x64/proofs
Jun 29 23:32:39 Finished examples/compilation/x64/proofs                       1m51s   2GB
Jun 29 23:32:40 Starting examples/compilation/ag32
Jun 30 00:05:39 Finished examples/compilation/ag32                            32m59s   6GB
Jun 30 00:05:39 Starting examples/compilation/ag32/proofs
Jun 30 00:06:28 Finished examples/compilation/ag32/proofs                        48s   2GB
Jun 30 00:06:28 Starting examples/cost
Jun 30 01:01:51 Finished examples/cost                                        55m22s   6GB
Jun 30 01:01:51 Starting examples/lpr_checker
Jun 30 01:06:01 Finished examples/lpr_checker                                  4m10s   3GB
Jun 30 01:06:01 Starting examples/lpr_checker/compilation
Jun 30 01:25:44 Finished examples/lpr_checker/compilation                     19m42s   8GB
Jun 30 01:25:44 Starting examples/lpr_checker/compilation/proofs
Jun 30 01:26:24 Finished examples/lpr_checker/compilation/proofs                 39s   2GB
Jun 30 01:26:24 Starting examples/lpr_checker/array
Jun 30 01:37:41 Finished examples/lpr_checker/array                           11m17s   3GB
Jun 30 01:37:41 Starting examples/lpr_checker/array/compilation
Jun 30 01:57:39 Finished examples/lpr_checker/array/compilation               19m57s  11GB
Jun 30 01:57:39 Starting examples/lpr_checker/array/compilation/proofs
Jun 30 01:58:32 Finished examples/lpr_checker/array/compilation/proofs           52s   4GB
Jun 30 01:58:32 Starting translator/okasaki-examples
Jun 30 02:03:33 Finished translator/okasaki-examples                           5m00s   1GB
Jun 30 02:03:33 Starting translator/other-examples
Jun 30 02:04:26 Finished translator/other-examples                               52s   1GB
Jun 30 02:04:26 Starting compiler/parsing/tests
Jun 30 02:04:54 Finished compiler/parsing/tests                                  27s 598MB
Jun 30 02:04:54 Starting compiler/inference/tests
Jun 30 02:09:53 Finished compiler/inference/tests                              4m58s   5GB
Jun 30 02:09:53 Starting compiler/bootstrap/translation
Jun 30 05:17:22 Finished compiler/bootstrap/translation                     3h07m27s  28GB
Jun 30 05:17:22 Starting unverified/sexpr-bootstrap/x64/64
Jun 30 05:27:00 Finished unverified/sexpr-bootstrap/x64/64                     9m37s   8GB
Jun 30 05:27:00 Starting unverified/sexpr-bootstrap/x64/32
Jun 30 05:34:36 Finished unverified/sexpr-bootstrap/x64/32                     7m35s   8GB
Jun 30 05:34:36 Starting compiler/benchmarks
Jun 30 05:34:39 Finished compiler/benchmarks                                      3s  24MB
Jun 30 05:34:40 Starting compiler/bootstrap/compilation/x64/64
Jun 30 23:47:28 Finished compiler/bootstrap/compilation/x64/64             18h12m47s  37GB
Jun 30 23:47:28 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 30 23:51:00 Finished compiler/bootstrap/compilation/x64/64/proofs          3m31s  14GB
Jun 30 23:51:00 Starting compiler/bootstrap/compilation/x64/32
Jul 01 16:27:48 Finished compiler/bootstrap/compilation/x64/32             16h36m46s  36GB
Jul 01 16:27:48 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 01 16:31:17 Finished compiler/bootstrap/compilation/x64/32/proofs          3m28s  13GB
Jul 01 16:31:17 Starting compiler/bootstrap/compilation/ag32/32
Jul 02 11:37:34 Finished compiler/bootstrap/compilation/ag32/32            19h06m17s  35GB
Jul 02 11:37:34 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 02 12:08:45 Finished compiler/bootstrap/compilation/ag32/32/proofs        31m10s  26GB
Jul 02 12:08:45 SUCCESS