Job 1012

CakeML:6217a49acea35e3698ec35c342033a1137a43768
  Fix compiler/encoders/monadic_enc for drule change [Aug 18 04:12:33]
HOL:e82f681da267a0f96134a92b4fea9d962cae182e
  Remove redundant theorem from temporal_deep example's set_lemmata [Aug 19 02:05:33]
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

Aug 21 08:45:24 Claimed job
Aug 21 08:45:31 Building HOL
Aug 21 08:54:56 Starting developers
Aug 21 08:54:59 Finished developers                                               2s  20MB
Aug 21 08:54:59 Starting developers/bin
Aug 21 08:55:06 Finished developers/bin                                           6s 960MB
Aug 21 08:55:06 Starting semantics/ffi
Aug 21 08:55:44 Finished semantics/ffi                                           37s 604MB
Aug 21 08:55:44 Starting semantics
Aug 21 08:57:19 Finished semantics                                             1m34s   1GB
Aug 21 08:57:19 Starting semantics/proofs
Aug 21 09:00:19 Finished semantics/proofs                                      2m59s   1GB
Aug 21 09:00:19 Starting semantics/alt_semantics
Aug 21 09:00:27 Finished semantics/alt_semantics                                  8s 254MB
Aug 21 09:00:28 Starting semantics/alt_semantics/proofs
Aug 21 09:02:18 Finished semantics/alt_semantics/proofs                        1m49s 730MB
Aug 21 09:02:18 Starting basis/pure
Aug 21 09:05:52 Finished basis/pure                                            3m34s 613MB
Aug 21 09:05:52 Starting translator
Aug 21 09:07:39 Finished translator                                            1m46s   1GB
Aug 21 09:07:39 Starting compiler/parsing
Aug 21 09:08:36 Finished compiler/parsing                                        57s   2GB
Aug 21 09:08:37 Starting characteristic
Aug 21 09:13:51 Finished characteristic                                        5m14s   1GB
Aug 21 09:13:51 Starting translator/monadic
Aug 21 09:15:20 Finished translator/monadic                                    1m28s   1GB
Aug 21 09:15:20 Starting basis
Aug 21 09:33:21 Finished basis                                                18m00s   2GB
Aug 21 09:33:21 Starting compiler/inference
Aug 21 09:35:17 Finished compiler/inference                                    1m56s   1GB
Aug 21 09:35:17 Starting compiler/backend/reg_alloc
Aug 21 09:36:18 Finished compiler/backend/reg_alloc                            1m00s   1GB
Aug 21 09:36:18 Starting compiler/backend/gc
Aug 21 09:45:34 Finished compiler/backend/gc                                   9m15s   2GB
Aug 21 09:45:34 Starting compiler/backend
Aug 21 09:45:37 Finished compiler/backend                                         2s  18MB
Aug 21 09:45:37 Starting compiler/encoders/asm
Aug 21 09:45:39 Finished compiler/encoders/asm                                    1s  14MB
Aug 21 09:45:39 Starting compiler/encoders/x64
Aug 21 09:46:38 Finished compiler/encoders/x64                                   59s 680MB
Aug 21 09:46:38 Starting compiler/encoders/arm7
Aug 21 09:48:19 Finished compiler/encoders/arm7                                1m40s   1GB
Aug 21 09:48:19 Starting compiler/encoders/arm8
Aug 21 09:48:52 Finished compiler/encoders/arm8                                  32s 526MB
Aug 21 09:48:52 Starting compiler/encoders/mips
Aug 21 09:49:59 Finished compiler/encoders/mips                                1m07s   1GB
Aug 21 09:49:59 Starting compiler/encoders/riscv
Aug 21 09:51:22 Finished compiler/encoders/riscv                               1m22s 882MB
Aug 21 09:51:22 Starting compiler/encoders/ag32
Aug 21 09:51:39 Finished compiler/encoders/ag32                                  17s 710MB
Aug 21 09:51:39 Starting compiler/backend/x64
Aug 21 09:51:58 Finished compiler/backend/x64                                    18s   1GB
Aug 21 09:51:58 Starting compiler/backend/arm7
Aug 21 09:52:19 Finished compiler/backend/arm7                                   20s   1GB
Aug 21 09:52:19 Starting compiler/backend/arm8
Aug 21 09:52:38 Finished compiler/backend/arm8                                   18s   1GB
Aug 21 09:52:38 Starting compiler/backend/mips
Aug 21 09:52:58 Finished compiler/backend/mips                                   19s   1GB
Aug 21 09:52:58 Starting compiler/backend/riscv
Aug 21 09:53:16 Finished compiler/backend/riscv                                  17s 843MB
Aug 21 09:53:16 Starting compiler/backend/ag32
Aug 21 09:54:22 Finished compiler/backend/ag32                                 1m06s   1GB
Aug 21 09:54:23 Starting compiler/parsing/proofs
Aug 21 09:59:56 Finished compiler/parsing/proofs                               5m32s   1GB
Aug 21 09:59:56 Starting compiler/inference/proofs
Aug 21 10:02:46 Finished compiler/inference/proofs                             2m49s   1GB
Aug 21 10:02:46 Starting compiler/backend/semantics
Aug 21 10:09:52 Finished compiler/backend/semantics                            7m05s   1GB
Aug 21 10:09:52 Starting compiler/backend/reg_alloc/proofs
Aug 21 10:13:08 Finished compiler/backend/reg_alloc/proofs                     3m16s 782MB
Aug 21 10:13:09 Starting compiler/backend/proofs
Aug 21 10:51:39 Finished compiler/backend/proofs                              38m29s   4GB
Aug 21 10:51:39 Starting compiler/encoders/x64/proofs
Aug 21 11:01:40 Finished compiler/encoders/x64/proofs                         10m00s   4GB
Aug 21 11:01:40 Starting compiler/encoders/arm7/proofs
Aug 21 11:14:50 Finished compiler/encoders/arm7/proofs                        13m10s   3GB
Aug 21 11:14:51 Starting compiler/encoders/arm8/proofs
Aug 21 11:21:28 Finished compiler/encoders/arm8/proofs                         6m37s   1GB
Aug 21 11:21:29 Starting compiler/encoders/mips/proofs
Aug 21 11:31:06 Finished compiler/encoders/mips/proofs                         9m36s   2GB
Aug 21 11:31:06 Starting compiler/encoders/riscv/proofs
Aug 21 11:39:26 Finished compiler/encoders/riscv/proofs                        8m20s   1GB
Aug 21 11:39:27 Starting compiler/encoders/ag32/proofs
Aug 21 11:41:51 Finished compiler/encoders/ag32/proofs                         2m24s 647MB
Aug 21 11:41:51 Starting compiler/backend/x64/proofs
Aug 21 11:42:11 Finished compiler/backend/x64/proofs                             19s   1GB
Aug 21 11:42:11 Starting compiler/backend/arm7/proofs
Aug 21 11:42:32 Finished compiler/backend/arm7/proofs                            20s   1GB
Aug 21 11:42:32 Starting compiler/backend/arm8/proofs
Aug 21 11:42:52 Finished compiler/backend/arm8/proofs                            19s   1GB
Aug 21 11:42:52 Starting compiler/backend/mips/proofs
Aug 21 11:43:12 Finished compiler/backend/mips/proofs                            19s   1GB
Aug 21 11:43:12 Starting compiler/backend/riscv/proofs
Aug 21 11:43:32 Finished compiler/backend/riscv/proofs                           19s   1GB
Aug 21 11:43:32 Starting compiler/backend/ag32/proofs
Aug 21 11:52:20 Finished compiler/backend/ag32/proofs                          8m47s   2GB
Aug 21 11:52:20 Starting compiler/proofs
Aug 21 11:54:00 Finished compiler/proofs                                       1m39s   3GB
Aug 21 11:54:00 Starting candle/set-theory
Aug 21 11:54:27 Finished candle/set-theory                                       26s 706MB
Aug 21 11:54:27 Starting candle/syntax-lib
Aug 21 11:54:38 Finished candle/syntax-lib                                       10s 447MB
Aug 21 11:54:38 Starting candle/standard/syntax
Aug 21 11:56:22 Finished candle/standard/syntax                                1m43s 865MB
Aug 21 11:56:22 Starting candle/standard/semantics
Aug 21 11:58:00 Finished candle/standard/semantics                             1m37s   1GB
Aug 21 11:58:00 Starting candle/standard/monadic
Aug 21 11:59:33 Finished candle/standard/monadic                               1m33s   1GB
Aug 21 11:59:33 Starting candle/standard/ml_kernel
Aug 21 12:03:19 Finished candle/standard/ml_kernel                             3m45s   3GB
Aug 21 12:03:19 Starting candle/standard/opentheory
Aug 21 12:12:04 Finished candle/standard/opentheory                            8m44s   4GB
Aug 21 12:12:04 Starting candle/standard/opentheory/compilation
Aug 21 12:40:35 Finished candle/standard/opentheory/compilation               28m31s  14GB
Aug 21 12:40:36 Starting candle/standard/opentheory/compilation/proofs
Aug 21 12:41:39 Finished candle/standard/opentheory/compilation/proofs         1m03s   2GB
Aug 21 12:41:40 Starting characteristic/examples
Aug 21 12:43:05 Finished characteristic/examples                               1m25s   2GB
Aug 21 12:43:05 Starting tutorial/solutions
Aug 21 12:56:12 Finished tutorial/solutions                                   13m06s   6GB
Aug 21 12:56:12 Starting translator/monadic/examples
Aug 21 12:59:08 Finished translator/monadic/examples                           2m55s   2GB
Aug 21 12:59:09 Starting examples
Aug 21 13:07:59 Finished examples                                              8m50s   3GB
Aug 21 13:07:59 Starting examples/compilation/x64
Aug 21 15:10:38 Finished examples/compilation/x64                           2h02m38s  15GB
Aug 21 15:10:39 Starting examples/compilation/x64/proofs
Aug 21 15:12:18 Finished examples/compilation/x64/proofs                       1m38s   2GB
Aug 21 15:12:18 Starting examples/compilation/ag32
Aug 21 15:40:47 Finished examples/compilation/ag32                            28m29s   5GB
Aug 21 15:40:47 Starting examples/compilation/ag32/proofs
Aug 21 15:41:38 Finished examples/compilation/ag32/proofs                        50s   2GB
Aug 21 15:41:38 Starting translator/okasaki-examples
Aug 21 15:45:40 Finished translator/okasaki-examples                           4m01s   1GB
Aug 21 15:45:40 Starting translator/other-examples
Aug 21 15:49:18 Finished translator/other-examples                             3m37s   1GB
Aug 21 15:49:18 Starting compiler/parsing/tests
Aug 21 15:49:43 Finished compiler/parsing/tests                                  25s 542MB
Aug 21 15:49:44 Starting compiler/inference/tests
Aug 21 15:53:52 Finished compiler/inference/tests                              4m07s   5GB
Aug 21 15:53:52 Starting compiler/bootstrap/translation
Aug 21 18:22:18 Finished compiler/bootstrap/translation                     2h28m26s  41GB
Aug 21 18:22:18 Starting unverified/sexpr-bootstrap/x64/64
Aug 21 18:34:42 Finished unverified/sexpr-bootstrap/x64/64                    12m22s   2GB
Aug 21 18:34:42 Starting unverified/sexpr-bootstrap/x64/32
Aug 21 18:43:38 Finished unverified/sexpr-bootstrap/x64/32                     8m54s   5GB
Aug 21 18:43:38 Starting compiler/benchmarks
Aug 21 18:43:45 Finished compiler/benchmarks                                      6s  23MB
Aug 21 18:43:45 Starting compiler/bootstrap/compilation/x64/64
Aug 22 06:41:33 Finished compiler/bootstrap/compilation/x64/64             11h57m46s  64GB
Aug 22 06:41:34 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 22 06:44:48 Finished compiler/bootstrap/compilation/x64/64/proofs          3m13s   7GB
Aug 22 06:44:48 Starting compiler/bootstrap/compilation/x64/32
Aug 22 17:29:48 Finished compiler/bootstrap/compilation/x64/32             10h44m59s  64GB
Aug 22 17:29:48 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 22 17:32:57 Finished compiler/bootstrap/compilation/x64/32/proofs          3m08s   5GB
Aug 22 17:32:57 Starting compiler/bootstrap/compilation/ag32/32
Aug 23 05:50:02 Finished compiler/bootstrap/compilation/ag32/32            12h17m03s  64GB
Aug 23 05:50:02 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 23 06:18:55 Finished compiler/bootstrap/compilation/ag32/32/proofs        28m52s  28GB
Aug 23 06:18:55 SUCCESS