Job 1016

CakeML:86c2abbb141f61cf7ade8ae8811ebf3db24365a4
  Remove all uses of store_thm (progress on #681) [Aug 22 15:30:03]
#682 (ban-store-thm)
Merging into: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 23 06:30:02 Claimed job
Aug 23 06:30:06 Reusing HOL
Aug 23 06:31:00 Starting developers
Aug 23 06:31:03 Finished developers                                               3s 105MB
Aug 23 06:31:03 Starting developers/bin
Aug 23 06:31:13 Finished developers/bin                                           9s 960MB
Aug 23 06:31:14 Starting semantics/ffi
Aug 23 06:31:24 Finished semantics/ffi                                           10s 233MB
Aug 23 06:31:24 Starting semantics
Aug 23 06:32:45 Finished semantics                                             1m20s   1GB
Aug 23 06:32:45 Starting semantics/proofs
Aug 23 06:35:49 Finished semantics/proofs                                      3m04s   1GB
Aug 23 06:35:49 Starting semantics/alt_semantics
Aug 23 06:35:58 Finished semantics/alt_semantics                                  8s 253MB
Aug 23 06:35:58 Starting semantics/alt_semantics/proofs
Aug 23 06:37:45 Finished semantics/alt_semantics/proofs                        1m46s 749MB
Aug 23 06:37:45 Starting basis/pure
Aug 23 06:38:33 Finished basis/pure                                              47s 662MB
Aug 23 06:38:33 Starting translator
Aug 23 06:40:20 Finished translator                                            1m46s   1GB
Aug 23 06:40:20 Starting compiler/parsing
Aug 23 06:41:18 Finished compiler/parsing                                        57s   2GB
Aug 23 06:41:18 Starting characteristic
Aug 23 06:46:36 Finished characteristic                                        5m17s   1GB
Aug 23 06:46:36 Starting translator/monadic
Aug 23 06:48:04 Finished translator/monadic                                    1m28s   1GB
Aug 23 06:48:04 Starting basis
Aug 23 07:06:02 Finished basis                                                17m57s   2GB
Aug 23 07:06:02 Starting compiler/inference
Aug 23 07:07:39 Finished compiler/inference                                    1m36s   1GB
Aug 23 07:07:39 Starting compiler/backend/reg_alloc
Aug 23 07:08:39 Finished compiler/backend/reg_alloc                              59s   1GB
Aug 23 07:08:39 Starting compiler/backend/gc
Aug 23 07:16:45 Finished compiler/backend/gc                                   8m05s   2GB
Aug 23 07:16:45 Starting compiler/backend
Aug 23 07:16:47 Finished compiler/backend                                         2s  15MB
Aug 23 07:16:47 Starting compiler/encoders/asm
Aug 23 07:16:49 Finished compiler/encoders/asm                                    1s  12MB
Aug 23 07:16:49 Starting compiler/encoders/x64
Aug 23 07:17:13 Finished compiler/encoders/x64                                   24s 580MB
Aug 23 07:17:14 Starting compiler/encoders/arm7
Aug 23 07:18:00 Finished compiler/encoders/arm7                                  45s 773MB
Aug 23 07:18:00 Starting compiler/encoders/arm8
Aug 23 07:18:13 Finished compiler/encoders/arm8                                  12s 892MB
Aug 23 07:18:13 Starting compiler/encoders/mips
Aug 23 07:18:31 Finished compiler/encoders/mips                                  17s   1GB
Aug 23 07:18:31 Starting compiler/encoders/riscv
Aug 23 07:18:46 Finished compiler/encoders/riscv                                 15s 768MB
Aug 23 07:18:46 Starting compiler/encoders/ag32
Aug 23 07:19:04 Finished compiler/encoders/ag32                                  16s 793MB
Aug 23 07:19:04 Starting compiler/backend/x64
Aug 23 07:19:22 Finished compiler/backend/x64                                    18s   1GB
Aug 23 07:19:22 Starting compiler/backend/arm7
Aug 23 07:19:43 Finished compiler/backend/arm7                                   20s   1GB
Aug 23 07:19:43 Starting compiler/backend/arm8
Aug 23 07:20:03 Finished compiler/backend/arm8                                   18s   1GB
Aug 23 07:20:03 Starting compiler/backend/mips
Aug 23 07:20:22 Finished compiler/backend/mips                                   18s   1GB
Aug 23 07:20:22 Starting compiler/backend/riscv
Aug 23 07:20:42 Finished compiler/backend/riscv                                  19s   1GB
Aug 23 07:20:42 Starting compiler/backend/ag32
Aug 23 07:21:50 Finished compiler/backend/ag32                                 1m08s   1GB
Aug 23 07:21:51 Starting compiler/parsing/proofs
Aug 23 07:27:29 Finished compiler/parsing/proofs                               5m38s   1GB
Aug 23 07:27:29 Starting compiler/inference/proofs
Aug 23 07:30:17 Finished compiler/inference/proofs                             2m47s   1GB
Aug 23 07:30:17 Starting compiler/backend/semantics
Aug 23 07:36:06 Finished compiler/backend/semantics                            5m49s   1GB
Aug 23 07:36:06 Starting compiler/backend/reg_alloc/proofs
Aug 23 07:39:20 Finished compiler/backend/reg_alloc/proofs                     3m13s 801MB
Aug 23 07:39:20 Starting compiler/backend/proofs
Aug 23 08:16:42 Finished compiler/backend/proofs                              37m20s   5GB
Aug 23 08:16:42 Starting compiler/encoders/x64/proofs
Aug 23 08:25:38 Finished compiler/encoders/x64/proofs                          8m55s   5GB
Aug 23 08:25:38 Starting compiler/encoders/arm7/proofs
Aug 23 08:37:48 Finished compiler/encoders/arm7/proofs                        12m09s   3GB
Aug 23 08:37:48 Starting compiler/encoders/arm8/proofs
Aug 23 08:44:12 Finished compiler/encoders/arm8/proofs                         6m24s   1GB
Aug 23 08:44:13 Starting compiler/encoders/mips/proofs
Aug 23 08:53:35 Finished compiler/encoders/mips/proofs                         9m22s   2GB
Aug 23 08:53:35 Starting compiler/encoders/riscv/proofs
Aug 23 09:01:46 Finished compiler/encoders/riscv/proofs                        8m10s   1GB
Aug 23 09:01:46 Starting compiler/encoders/ag32/proofs
Aug 23 09:04:14 Finished compiler/encoders/ag32/proofs                         2m27s 892MB
Aug 23 09:04:14 Starting compiler/backend/x64/proofs
Aug 23 09:04:34 Finished compiler/backend/x64/proofs                             19s   1GB
Aug 23 09:04:34 Starting compiler/backend/arm7/proofs
Aug 23 09:04:55 Finished compiler/backend/arm7/proofs                            20s 820MB
Aug 23 09:04:55 Starting compiler/backend/arm8/proofs
Aug 23 09:05:13 Finished compiler/backend/arm8/proofs                            18s 812MB
Aug 23 09:05:14 Starting compiler/backend/mips/proofs
Aug 23 09:05:34 Finished compiler/backend/mips/proofs                            20s   1GB
Aug 23 09:05:34 Starting compiler/backend/riscv/proofs
Aug 23 09:05:54 Finished compiler/backend/riscv/proofs                           19s   1GB
Aug 23 09:05:55 Starting compiler/backend/ag32/proofs
Aug 23 09:14:37 Finished compiler/backend/ag32/proofs                          8m42s   2GB
Aug 23 09:14:38 Starting compiler/proofs
Aug 23 09:16:10 Finished compiler/proofs                                       1m32s   2GB
Aug 23 09:16:10 Starting candle/set-theory
Aug 23 09:16:37 Finished candle/set-theory                                       26s 799MB
Aug 23 09:16:37 Starting candle/syntax-lib
Aug 23 09:16:48 Finished candle/syntax-lib                                       10s 621MB
Aug 23 09:16:48 Starting candle/standard/syntax
Aug 23 09:18:31 Finished candle/standard/syntax                                1m43s   1GB
Aug 23 09:18:31 Starting candle/standard/semantics
Aug 23 09:20:09 Finished candle/standard/semantics                             1m36s   1GB
Aug 23 09:20:09 Starting candle/standard/monadic
Aug 23 09:21:42 Finished candle/standard/monadic                               1m33s   1GB
Aug 23 09:21:42 Starting candle/standard/ml_kernel
Aug 23 09:25:32 Finished candle/standard/ml_kernel                             3m49s   6GB
Aug 23 09:25:32 Starting candle/standard/opentheory
Aug 23 09:34:01 Finished candle/standard/opentheory                            8m28s   4GB
Aug 23 09:34:01 Starting candle/standard/opentheory/compilation
Aug 23 10:03:59 Finished candle/standard/opentheory/compilation               29m57s  17GB
Aug 23 10:03:59 Starting candle/standard/opentheory/compilation/proofs
Aug 23 10:04:51 Finished candle/standard/opentheory/compilation/proofs           52s   2GB
Aug 23 10:04:51 Starting characteristic/examples
Aug 23 10:06:22 Finished characteristic/examples                               1m30s   2GB
Aug 23 10:06:22 Starting tutorial/solutions
Aug 23 10:19:30 Finished tutorial/solutions                                   13m07s   6GB
Aug 23 10:19:30 Starting translator/monadic/examples
Aug 23 15:05:27 Resuming translator/monadic/examples
Aug 23 15:06:12 Finished translator/monadic/examples                             45s   2GB
Aug 23 15:06:12 Starting examples
Aug 23 15:14:58 Finished examples                                              8m45s   4GB
Aug 23 15:14:58 Starting examples/compilation/x64
Aug 23 17:17:51 Finished examples/compilation/x64                           2h02m52s  11GB
Aug 23 17:17:51 Starting examples/compilation/x64/proofs
Aug 23 17:19:21 Finished examples/compilation/x64/proofs                       1m29s   2GB
Aug 23 17:19:21 Starting examples/compilation/ag32
Aug 23 17:47:59 Finished examples/compilation/ag32                            28m38s   6GB
Aug 23 17:48:00 Starting examples/compilation/ag32/proofs
Aug 23 17:48:49 Finished examples/compilation/ag32/proofs                        48s   2GB
Aug 23 17:48:49 Starting translator/okasaki-examples
Aug 23 17:52:51 Finished translator/okasaki-examples                           4m02s   1GB
Aug 23 17:52:51 Starting translator/other-examples
Aug 23 17:53:35 Finished translator/other-examples                               43s   1GB
Aug 23 17:53:35 Starting compiler/parsing/tests
Aug 23 17:54:01 Finished compiler/parsing/tests                                  25s 507MB
Aug 23 17:54:01 Starting compiler/inference/tests
Aug 23 17:58:09 Finished compiler/inference/tests                              4m07s   3GB
Aug 23 17:58:09 Starting compiler/bootstrap/translation
Aug 23 20:25:51 Finished compiler/bootstrap/translation                     2h27m41s  41GB
Aug 23 20:25:51 Starting unverified/sexpr-bootstrap/x64/64
Aug 23 20:38:14 Finished unverified/sexpr-bootstrap/x64/64                    12m22s   3GB
Aug 23 20:38:14 Starting unverified/sexpr-bootstrap/x64/32
Aug 23 20:46:54 Finished unverified/sexpr-bootstrap/x64/32                     8m40s   6GB
Aug 23 20:46:54 Starting compiler/benchmarks
Aug 23 20:47:01 Finished compiler/benchmarks                                      6s  22MB
Aug 23 20:47:02 Starting compiler/bootstrap/compilation/x64/64
Aug 24 09:57:31 Finished compiler/bootstrap/compilation/x64/64             13h10m28s  64GB
Aug 24 09:57:31 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 24 10:01:11 Finished compiler/bootstrap/compilation/x64/64/proofs          3m39s   4GB
Aug 24 10:01:11 Starting compiler/bootstrap/compilation/x64/32
Aug 24 21:11:20 Finished compiler/bootstrap/compilation/x64/32             11h10m08s  64GB
Aug 24 21:11:20 Starting compiler/bootstrap/compilation/x64/32/proofs
Aug 24 21:13:53 Finished compiler/bootstrap/compilation/x64/32/proofs          2m32s  10GB
Aug 24 21:13:53 Starting compiler/bootstrap/compilation/ag32/32
Aug 25 09:12:12 Finished compiler/bootstrap/compilation/ag32/32            11h58m18s  64GB
Aug 25 09:12:12 Starting compiler/bootstrap/compilation/ag32/32/proofs
Aug 25 09:38:45 Finished compiler/bootstrap/compilation/ag32/32/proofs        26m33s  16GB
Aug 25 09:38:45 SUCCESS