Job 1014

CakeML:b8905595f576715a674870c6acfe2977561a7a36
  Merge pull request #677 from CakeML/clos-install [Aug 21 17:07:21]
HOL:e82f681da267a0f96134a92b4fea9d962cae182e
  Remove redundant theorem from temporal_deep example's set_lemmata [Aug 19 02:05:33]
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

Aug 22 11:19:10 Claimed job
Aug 22 11:19:13 Reusing HOL
Aug 22 11:19:19 Starting developers
Aug 22 11:19:20 Finished developers                                               0s  38MB
Aug 22 11:19:20 Starting developers/bin
Aug 22 11:20:45 Finished developers/bin                                        1m24s 164MB
Aug 22 11:20:46 Starting semantics/ffi
Aug 22 11:21:19 Finished semantics/ffi                                           33s 337MB
Aug 22 11:21:20 Starting semantics
Aug 22 11:22:50 Finished semantics                                             1m30s   1GB
Aug 22 11:22:51 Starting semantics/proofs
Aug 22 11:25:50 Finished semantics/proofs                                      2m59s   1GB
Aug 22 11:25:50 Starting semantics/alt_semantics
Aug 22 11:25:57 Finished semantics/alt_semantics                                  6s 261MB
Aug 22 11:25:57 Starting semantics/alt_semantics/proofs
Aug 22 11:27:44 Finished semantics/alt_semantics/proofs                        1m46s 808MB
Aug 22 11:27:44 Starting basis/pure
Aug 22 11:31:17 Finished basis/pure                                            3m32s 673MB
Aug 22 11:31:17 Starting translator
Aug 22 11:33:01 Finished translator                                            1m43s   1GB
Aug 22 11:33:02 Starting compiler/parsing
Aug 22 11:34:00 Finished compiler/parsing                                        57s   2GB
Aug 22 11:34:00 Starting characteristic
Aug 22 11:39:14 Finished characteristic                                        5m13s   1GB
Aug 22 11:39:14 Starting translator/monadic
Aug 22 11:40:41 Finished translator/monadic                                    1m26s   1GB
Aug 22 11:40:41 Starting basis
Aug 22 11:58:39 Finished basis                                                17m56s   2GB
Aug 22 11:58:39 Starting compiler/inference
Aug 22 12:00:27 Finished compiler/inference                                    1m48s   1GB
Aug 22 12:00:28 Starting compiler/backend/reg_alloc
Aug 22 12:01:25 Finished compiler/backend/reg_alloc                              57s   1GB
Aug 22 12:01:25 Starting compiler/backend/gc
Aug 22 12:10:27 Finished compiler/backend/gc                                   9m00s   1GB
Aug 22 12:10:27 Starting compiler/backend
Aug 22 12:10:28 Finished compiler/backend                                         0s  42MB
Aug 22 12:10:29 Starting compiler/encoders/asm
Aug 22 12:10:29 Finished compiler/encoders/asm                                    0s  38MB
Aug 22 12:10:30 Starting compiler/encoders/x64
Aug 22 12:11:27 Finished compiler/encoders/x64                                   56s 708MB
Aug 22 12:11:27 Starting compiler/encoders/arm7
Aug 22 12:13:06 Finished compiler/encoders/arm7                                1m38s   1GB
Aug 22 12:13:06 Starting compiler/encoders/arm8
Aug 22 12:13:35 Finished compiler/encoders/arm8                                  28s 886MB
Aug 22 12:13:36 Starting compiler/encoders/mips
Aug 22 12:14:39 Finished compiler/encoders/mips                                1m02s   1GB
Aug 22 12:14:39 Starting compiler/encoders/riscv
Aug 22 12:15:55 Finished compiler/encoders/riscv                               1m15s   1GB
Aug 22 12:15:56 Starting compiler/encoders/ag32
Aug 22 12:16:11 Finished compiler/encoders/ag32                                  14s 730MB
Aug 22 12:16:11 Starting compiler/backend/x64
Aug 22 12:16:27 Finished compiler/backend/x64                                    15s   1GB
Aug 22 12:16:28 Starting compiler/backend/arm7
Aug 22 12:16:45 Finished compiler/backend/arm7                                   17s   1GB
Aug 22 12:16:46 Starting compiler/backend/arm8
Aug 22 12:17:02 Finished compiler/backend/arm8                                   16s   1GB
Aug 22 12:17:03 Starting compiler/backend/mips
Aug 22 12:17:20 Finished compiler/backend/mips                                   16s   1GB
Aug 22 12:17:20 Starting compiler/backend/riscv
Aug 22 12:17:37 Finished compiler/backend/riscv                                  16s   1GB
Aug 22 12:17:37 Starting compiler/backend/ag32
Aug 22 12:18:44 Finished compiler/backend/ag32                                 1m07s   1GB
Aug 22 12:18:45 Starting compiler/parsing/proofs
Aug 22 12:24:10 Finished compiler/parsing/proofs                               5m24s   1GB
Aug 22 12:24:10 Starting compiler/inference/proofs
Aug 22 12:26:50 Finished compiler/inference/proofs                             2m39s   1GB
Aug 22 12:26:50 Starting compiler/backend/semantics
Aug 22 12:32:39 Finished compiler/backend/semantics                            5m48s   2GB
Aug 22 12:32:40 Starting compiler/backend/reg_alloc/proofs
Aug 22 12:35:51 Finished compiler/backend/reg_alloc/proofs                     3m10s 773MB
Aug 22 12:35:51 Starting compiler/backend/proofs
Aug 22 13:12:59 Finished compiler/backend/proofs                              37m07s   3GB
Aug 22 13:12:59 Starting compiler/encoders/x64/proofs
Aug 22 13:23:02 Finished compiler/encoders/x64/proofs                         10m02s   4GB
Aug 22 13:23:03 Starting compiler/encoders/arm7/proofs
Aug 22 13:36:20 Finished compiler/encoders/arm7/proofs                        13m16s   6GB
Aug 22 13:36:20 Starting compiler/encoders/arm8/proofs
Aug 22 13:43:04 Finished compiler/encoders/arm8/proofs                         6m43s   1GB
Aug 22 13:43:04 Starting compiler/encoders/mips/proofs
Aug 22 13:53:13 Finished compiler/encoders/mips/proofs                        10m08s   1GB
Aug 22 13:53:13 Starting compiler/encoders/riscv/proofs
Aug 22 14:01:35 Finished compiler/encoders/riscv/proofs                        8m21s   1GB
Aug 22 14:01:35 Starting compiler/encoders/ag32/proofs
Aug 22 14:04:03 Finished compiler/encoders/ag32/proofs                         2m27s 675MB
Aug 22 14:04:03 Starting compiler/backend/x64/proofs
Aug 22 14:04:20 Finished compiler/backend/x64/proofs                             16s   1GB
Aug 22 14:04:20 Starting compiler/backend/arm7/proofs
Aug 22 14:04:38 Finished compiler/backend/arm7/proofs                            17s 811MB
Aug 22 14:04:38 Starting compiler/backend/arm8/proofs
Aug 22 14:04:55 Finished compiler/backend/arm8/proofs                            16s   1GB
Aug 22 14:04:55 Starting compiler/backend/mips/proofs
Aug 22 14:05:12 Finished compiler/backend/mips/proofs                            16s   1GB
Aug 22 14:05:12 Starting compiler/backend/riscv/proofs
Aug 22 14:05:29 Finished compiler/backend/riscv/proofs                           15s   1GB
Aug 22 14:05:29 Starting compiler/backend/ag32/proofs
Aug 22 14:14:21 Finished compiler/backend/ag32/proofs                          8m51s   2GB
Aug 22 14:14:21 Starting compiler/proofs
Aug 22 14:15:49 Finished compiler/proofs                                       1m27s   3GB
Aug 22 14:15:50 Starting candle/set-theory
Aug 22 14:16:14 Finished candle/set-theory                                       24s 748MB
Aug 22 14:16:15 Starting candle/syntax-lib
Aug 22 14:16:24 Finished candle/syntax-lib                                        9s 647MB
Aug 22 14:16:25 Starting candle/standard/syntax
Aug 22 14:18:05 Finished candle/standard/syntax                                1m39s 930MB
Aug 22 14:18:06 Starting candle/standard/semantics
Aug 22 14:19:38 Finished candle/standard/semantics                             1m32s   1GB
Aug 22 14:19:39 Starting candle/standard/monadic
Aug 22 14:21:10 Finished candle/standard/monadic                               1m31s   1GB
Aug 22 14:21:11 Starting candle/standard/ml_kernel
Aug 22 14:24:56 Finished candle/standard/ml_kernel                             3m45s   5GB
Aug 22 14:24:57 Starting candle/standard/opentheory
Aug 22 14:33:20 Finished candle/standard/opentheory                            8m22s   3GB
Aug 22 14:33:20 Starting candle/standard/opentheory/compilation
Aug 22 15:03:06 Finished candle/standard/opentheory/compilation               29m45s  19GB
Aug 22 15:03:06 Starting candle/standard/opentheory/compilation/proofs
Aug 22 15:03:41 Finished candle/standard/opentheory/compilation/proofs           34s   3GB
Aug 22 15:03:41 Starting characteristic/examples
Aug 22 15:05:13 Finished characteristic/examples                               1m31s   2GB
Aug 22 15:05:14 Starting tutorial/solutions
Aug 22 15:17:56 Finished tutorial/solutions                                   12m41s   6GB
Aug 22 15:17:56 Starting translator/monadic/examples
Aug 22 15:20:46 Finished translator/monadic/examples                           2m49s   2GB
Aug 22 15:20:47 Starting examples
Aug 22 15:29:36 Finished examples                                              8m48s   4GB
Aug 22 15:29:36 Starting examples/compilation/x64
Aug 22 17:33:34 Finished examples/compilation/x64                           2h03m58s  10GB
Aug 22 17:33:35 Starting examples/compilation/x64/proofs
Aug 22 17:35:45 Finished examples/compilation/x64/proofs                       2m10s   2GB
Aug 22 17:35:46 Starting examples/compilation/ag32
Aug 22 18:08:17 Finished examples/compilation/ag32                            32m30s   6GB
Aug 22 18:08:17 Starting examples/compilation/ag32/proofs
Aug 22 18:09:20 Finished examples/compilation/ag32/proofs                      1m02s   3GB
Aug 22 18:09:20 Starting translator/okasaki-examples
Aug 22 18:15:25 Finished translator/okasaki-examples                           6m04s   2GB
Aug 22 18:15:26 Starting translator/other-examples
Aug 22 18:20:38 Finished translator/other-examples                             5m12s   1GB
Aug 22 18:20:39 Starting compiler/parsing/tests
Aug 22 18:21:13 Finished compiler/parsing/tests                                  34s 523MB
Aug 22 18:21:13 Starting compiler/inference/tests
Aug 22 18:27:39 Finished compiler/inference/tests                              6m25s   2GB
Aug 22 18:27:39 Starting compiler/bootstrap/translation
Aug 22 21:00:25 Finished compiler/bootstrap/translation                     2h32m44s  34GB
Aug 22 21:00:25 Starting unverified/sexpr-bootstrap/x64/64
Aug 22 21:12:21 Finished unverified/sexpr-bootstrap/x64/64                    11m54s   2GB
Aug 22 21:12:21 Starting unverified/sexpr-bootstrap/x64/32
Aug 22 21:21:09 Finished unverified/sexpr-bootstrap/x64/32                     8m46s   6GB
Aug 22 21:21:10 Starting compiler/benchmarks
Aug 22 21:58:24 Finished compiler/benchmarks                                  37m14s   1GB
Aug 22 21:58:25 Starting compiler/bootstrap/compilation/x64/64
Aug 23 10:35:36 Finished compiler/bootstrap/compilation/x64/64             12h37m10s  63GB
Aug 23 10:35:37 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 23 10:38:17 Finished compiler/bootstrap/compilation/x64/64/proofs          2m40s  11GB
Aug 23 10:38:18 Starting compiler/bootstrap/compilation/x64/32
Aug 23 22:34:15 Finished compiler/bootstrap/compilation/x64/32             11h55m54s  64GB
Aug 23 22:34:16 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 23 22:37:57 Finished compiler/bootstrap/compilation/x64/32/proofs          3m40s   4GB
Aug 23 22:37:57 Starting compiler/bootstrap/compilation/ag32/32
Aug 24 10:59:56 Finished compiler/bootstrap/compilation/ag32/32            12h21m58s  64GB
Aug 24 10:59:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 24 11:33:11 Finished compiler/bootstrap/compilation/ag32/32/proofs        33m14s  16GB
Aug 24 11:33:12 SUCCESS