Job 542

CakeML:33e99acd8473d0f3b26811cff129818bb6b04743
  Merge pull request #545 from CakeML/explorer [Oct 21 01:02:30]
HOL:06df083877b529892a4a72756c28eadd543bb754
  Add fold to sptree and a few lemmas about size [Oct 20 19:25:48]
Machine:oven1 4.15.9-300.fc27.x86_64 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

Oct 21 05:32:05 Claimed job
Oct 21 05:32:08 Reusing HOL
Oct 21 05:33:01 Starting developers/bin
Oct 21 05:34:13 Finished developers/bin                                        1m11s 914MB
Oct 21 05:34:14 Starting semantics/ffi
Oct 21 05:34:26 Finished semantics/ffi                                           11s 248MB
Oct 21 05:34:26 Starting semantics
Oct 21 05:35:40 Finished semantics                                             1m12s 767MB
Oct 21 05:35:41 Starting semantics/proofs
Oct 21 05:38:23 Finished semantics/proofs                                      2m41s   1GB
Oct 21 05:38:24 Starting basis/pure
Oct 21 05:39:14 Finished basis/pure                                              49s 666MB
Oct 21 05:39:15 Starting translator
Oct 21 05:42:17 Finished translator                                            3m00s   1GB
Oct 21 05:42:17 Starting compiler/parsing
Oct 21 05:43:32 Finished compiler/parsing                                      1m14s   1GB
Oct 21 05:43:33 Starting characteristic
Oct 21 05:46:02 Finished characteristic                                        2m28s   1GB
Oct 21 05:46:03 Starting translator/monadic
Oct 21 05:47:27 Finished translator/monadic                                    1m23s   1GB
Oct 21 05:47:28 Starting basis
Oct 21 06:03:59 Finished basis                                                16m30s   3GB
Oct 21 06:03:59 Starting compiler/inference
Oct 21 06:05:42 Finished compiler/inference                                    1m41s   1GB
Oct 21 06:05:42 Starting compiler/backend/reg_alloc
Oct 21 06:06:30 Finished compiler/backend/reg_alloc                              47s   1GB
Oct 21 06:06:31 Starting compiler/backend/gc
Oct 21 06:13:45 Finished compiler/backend/gc                                   7m13s   1GB
Oct 21 06:13:46 Starting compiler/backend
Oct 21 06:13:50 Finished compiler/backend                                         3s  16MB
Oct 21 06:13:50 Starting compiler/encoders/asm
Oct 21 06:13:52 Finished compiler/encoders/asm                                    1s  14MB
Oct 21 06:13:53 Starting compiler/encoders/x64
Oct 21 06:14:45 Finished compiler/encoders/x64                                   51s 609MB
Oct 21 06:14:46 Starting compiler/encoders/arm6
Oct 21 06:16:29 Finished compiler/encoders/arm6                                1m42s   1GB
Oct 21 06:16:30 Starting compiler/encoders/arm8
Oct 21 06:16:56 Finished compiler/encoders/arm8                                  25s 492MB
Oct 21 06:16:57 Starting compiler/encoders/mips
Oct 21 06:17:56 Finished compiler/encoders/mips                                  58s 766MB
Oct 21 06:17:56 Starting compiler/encoders/riscv
Oct 21 06:18:57 Finished compiler/encoders/riscv                               1m00s 889MB
Oct 21 06:18:58 Starting compiler/backend/x64
Oct 21 06:19:16 Finished compiler/backend/x64                                    17s 867MB
Oct 21 06:19:16 Starting compiler/backend/arm6
Oct 21 06:19:37 Finished compiler/backend/arm6                                   20s 972MB
Oct 21 06:19:38 Starting compiler/backend/arm8
Oct 21 06:19:57 Finished compiler/backend/arm8                                   18s   1GB
Oct 21 06:19:57 Starting compiler/backend/mips
Oct 21 06:20:17 Finished compiler/backend/mips                                   18s   1GB
Oct 21 06:20:18 Starting compiler/backend/riscv
Oct 21 06:20:37 Finished compiler/backend/riscv                                  18s   1GB
Oct 21 06:20:38 Starting compiler/parsing/proofs
Oct 21 06:26:44 Finished compiler/parsing/proofs                               6m05s 779MB
Oct 21 06:26:44 Starting compiler/inference/proofs
Oct 21 06:29:35 Finished compiler/inference/proofs                             2m49s   1GB
Oct 21 06:29:36 Starting compiler/backend/semantics
Oct 21 06:38:26 Finished compiler/backend/semantics                            8m49s   2GB
Oct 21 06:38:27 Starting compiler/backend/reg_alloc/proofs
Oct 21 06:45:40 Finished compiler/backend/reg_alloc/proofs                     7m12s 547MB
Oct 21 06:45:41 Starting compiler/backend/proofs
Oct 21 07:26:15 Finished compiler/backend/proofs                              40m33s   3GB
Oct 21 07:26:16 Starting compiler/encoders/x64/proofs
Oct 21 07:33:37 Finished compiler/encoders/x64/proofs                          7m20s   4GB
Oct 21 07:33:37 Starting compiler/encoders/arm6/proofs
Oct 21 07:41:10 Finished compiler/encoders/arm6/proofs                         7m32s   3GB
Oct 21 07:41:11 Starting compiler/encoders/arm8/proofs
Oct 21 07:46:36 Finished compiler/encoders/arm8/proofs                         5m24s 951MB
Oct 21 07:46:36 Starting compiler/encoders/mips/proofs
Oct 21 07:54:00 Finished compiler/encoders/mips/proofs                         7m22s   1GB
Oct 21 07:54:00 Starting compiler/encoders/riscv/proofs
Oct 21 08:01:54 Finished compiler/encoders/riscv/proofs                        7m52s 784MB
Oct 21 08:01:54 Starting compiler/backend/x64/proofs
Oct 21 08:02:16 Finished compiler/backend/x64/proofs                             20s   1GB
Oct 21 08:02:17 Starting compiler/backend/arm6/proofs
Oct 21 08:02:40 Finished compiler/backend/arm6/proofs                            23s   1GB
Oct 21 08:02:41 Starting compiler/backend/arm8/proofs
Oct 21 08:03:03 Finished compiler/backend/arm8/proofs                            20s   1GB
Oct 21 08:03:03 Starting compiler/backend/mips/proofs
Oct 21 08:03:24 Finished compiler/backend/mips/proofs                            20s 925MB
Oct 21 08:03:25 Starting compiler/backend/riscv/proofs
Oct 21 08:03:47 Finished compiler/backend/riscv/proofs                           20s   1GB
Oct 21 08:03:47 Starting compiler/proofs
Oct 21 08:05:08 Finished compiler/proofs                                       1m20s   2GB
Oct 21 08:05:09 Starting candle/set-theory
Oct 21 08:05:35 Finished candle/set-theory                                       25s 603MB
Oct 21 08:05:36 Starting candle/syntax-lib
Oct 21 08:05:47 Finished candle/syntax-lib                                       10s 662MB
Oct 21 08:05:47 Starting candle/standard/syntax
Oct 21 08:07:21 Finished candle/standard/syntax                                1m32s 664MB
Oct 21 08:07:22 Starting candle/standard/semantics
Oct 21 08:08:43 Finished candle/standard/semantics                             1m21s   1GB
Oct 21 08:08:44 Starting candle/standard/monadic
Oct 21 08:10:18 Finished candle/standard/monadic                               1m33s 855MB
Oct 21 08:10:19 Starting candle/standard/ml_kernel
Oct 21 08:26:23 Finished candle/standard/ml_kernel                            16m03s   4GB
Oct 21 08:26:23 Starting candle/standard/opentheory
Oct 21 08:35:07 Finished candle/standard/opentheory                            8m42s   5GB
Oct 21 08:35:07 Starting candle/standard/opentheory/compilation
Oct 21 09:08:57 Finished candle/standard/opentheory/compilation               33m49s  17GB
Oct 21 09:08:58 Starting candle/standard/opentheory/compilation/proofs
Oct 21 09:09:36 Finished candle/standard/opentheory/compilation/proofs           37s   4GB
Oct 21 09:09:36 Starting characteristic/examples
Oct 21 09:11:12 Finished characteristic/examples                               1m35s   2GB
Oct 21 09:11:13 Starting tutorial/solutions
Oct 21 09:24:26 Finished tutorial/solutions                                   13m12s   6GB
Oct 21 09:24:26 Starting translator/monadic/examples
Oct 21 09:26:14 Finished translator/monadic/examples                           1m47s   2GB
Oct 21 09:26:15 Starting examples
Oct 21 09:31:57 Finished examples                                              5m41s   3GB
Oct 21 09:31:58 Starting examples/compilation
Oct 21 11:27:05 Finished examples/compilation                               1h55m06s  10GB
Oct 21 11:27:06 Starting examples/compilation/proofs
Oct 21 11:29:11 Finished examples/compilation/proofs                           2m04s   3GB
Oct 21 11:29:11 Starting compiler/benchmarks
Oct 21 11:29:13 Finished compiler/benchmarks                                      0s   4MB
Oct 21 11:29:13 Starting translator/okasaki-examples
Oct 21 11:32:42 Finished translator/okasaki-examples                           3m28s   1GB
Oct 21 11:32:43 Starting translator/other-examples
Oct 21 11:36:13 Finished translator/other-examples                             3m29s 750MB
Oct 21 11:36:14 Starting compiler/parsing/tests
Oct 21 11:36:39 Finished compiler/parsing/tests                                  24s 341MB
Oct 21 11:36:40 Starting compiler/inference/tests
Oct 21 11:40:34 Finished compiler/inference/tests                              3m53s   4GB
Oct 21 11:40:35 Starting compiler/bootstrap/translation
Oct 21 18:35:57 Finished compiler/bootstrap/translation                     6h55m19s  53GB
Oct 21 18:35:58 Starting unverified/sexpr-bootstrap/x64/64
Oct 21 18:44:09 Finished unverified/sexpr-bootstrap/x64/64                     8m09s  15GB
Oct 21 18:44:09 Starting unverified/sexpr-bootstrap/x64/32
Oct 21 18:49:35 Finished unverified/sexpr-bootstrap/x64/32                     5m24s  18GB
Oct 21 18:49:36 Starting compiler/bootstrap/compilation/x64/64
Oct 22 13:20:03 Finished compiler/bootstrap/compilation/x64/64             18h30m25s  64GB
Oct 22 13:20:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 22 13:23:23 Finished compiler/bootstrap/compilation/x64/64/proofs          3m18s  25GB
Oct 22 13:23:24 Starting compiler/bootstrap/compilation/x64/32
Oct 22 23:39:14 Finished compiler/bootstrap/compilation/x64/32             10h15m48s  64GB
Oct 22 23:39:15 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 22 23:43:22 Finished compiler/bootstrap/compilation/x64/32/proofs          4m06s  21GB
Oct 22 23:43:23 SUCCESS