Job 815

CakeML:ccd4671556758a3ad5ce925a7688e8618e915248
  Merge pull request #630 from talsewell/compute-thmset [Apr 20 03:03:19]
HOL:d9d262ad8402d865a72735480268b9f2da63fcd9
  Change ThmSetData to store just theorem names in .dat files [Apr 21 04:26: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

Apr 24 05:30:01 Claimed job
Apr 24 05:30:10 Reusing HOL
Apr 24 05:31:04 Starting developers
Apr 24 05:31:06 Finished developers                                               2s  20MB
Apr 24 05:31:07 Starting developers/bin
Apr 24 05:32:20 Finished developers/bin                                        1m12s 918MB
Apr 24 05:32:20 Starting semantics/ffi
Apr 24 05:32:30 Finished semantics/ffi                                           10s 230MB
Apr 24 05:32:30 Starting semantics
Apr 24 05:33:52 Finished semantics                                             1m21s   1GB
Apr 24 05:33:52 Starting semantics/proofs
Apr 24 05:36:47 Finished semantics/proofs                                      2m55s   1GB
Apr 24 05:36:48 Starting basis/pure
Apr 24 05:37:35 Finished basis/pure                                              47s 653MB
Apr 24 05:37:35 Starting translator
Apr 24 05:39:16 Finished translator                                            1m40s   1GB
Apr 24 05:39:16 Starting compiler/parsing
Apr 24 05:40:14 Finished compiler/parsing                                        57s   2GB
Apr 24 05:40:14 Starting characteristic
Apr 24 05:45:28 Finished characteristic                                        5m14s   1GB
Apr 24 05:45:29 Starting translator/monadic
Apr 24 05:46:57 Finished translator/monadic                                    1m28s   1GB
Apr 24 05:46:58 Starting basis
Apr 24 06:03:11 Finished basis                                                16m13s   2GB
Apr 24 06:03:11 Starting compiler/inference
Apr 24 06:04:43 Finished compiler/inference                                    1m31s   1GB
Apr 24 06:04:44 Starting compiler/backend/reg_alloc
Apr 24 06:05:36 Finished compiler/backend/reg_alloc                              52s   1GB
Apr 24 06:05:37 Starting compiler/backend/gc
Apr 24 06:13:35 Finished compiler/backend/gc                                   7m58s   2GB
Apr 24 06:13:36 Starting compiler/backend
Apr 24 06:13:38 Finished compiler/backend                                         2s  17MB
Apr 24 06:13:39 Starting compiler/encoders/asm
Apr 24 06:13:40 Finished compiler/encoders/asm                                    1s  23MB
Apr 24 06:13:40 Starting compiler/encoders/x64
Apr 24 06:14:06 Finished compiler/encoders/x64                                   25s 596MB
Apr 24 06:14:06 Starting compiler/encoders/arm6
Apr 24 06:14:52 Finished compiler/encoders/arm6                                  45s 715MB
Apr 24 06:14:52 Starting compiler/encoders/arm8
Apr 24 06:15:06 Finished compiler/encoders/arm8                                  13s 546MB
Apr 24 06:15:06 Starting compiler/encoders/mips
Apr 24 06:15:23 Finished compiler/encoders/mips                                  17s   1GB
Apr 24 06:15:24 Starting compiler/encoders/riscv
Apr 24 06:15:39 Finished compiler/encoders/riscv                                 15s 810MB
Apr 24 06:15:40 Starting compiler/encoders/ag32
Apr 24 06:15:57 Finished compiler/encoders/ag32                                  16s 810MB
Apr 24 06:15:57 Starting compiler/backend/x64
Apr 24 06:16:15 Finished compiler/backend/x64                                    17s   1GB
Apr 24 06:16:15 Starting compiler/backend/arm6
Apr 24 06:16:35 Finished compiler/backend/arm6                                   19s   1GB
Apr 24 06:16:35 Starting compiler/backend/arm8
Apr 24 06:16:52 Finished compiler/backend/arm8                                   16s 908MB
Apr 24 06:16:53 Starting compiler/backend/mips
Apr 24 06:17:11 Finished compiler/backend/mips                                   18s   1GB
Apr 24 06:17:12 Starting compiler/backend/riscv
Apr 24 06:17:31 Finished compiler/backend/riscv                                  18s   1GB
Apr 24 06:17:31 Starting compiler/backend/ag32
Apr 24 06:18:38 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 24 06:18:38 Starting compiler/parsing/proofs
Apr 24 06:24:08 Finished compiler/parsing/proofs                               5m29s   1GB
Apr 24 06:24:08 Starting compiler/inference/proofs
Apr 24 06:26:48 Finished compiler/inference/proofs                             2m39s   1GB
Apr 24 06:26:48 Starting compiler/backend/semantics
Apr 24 06:33:39 Finished compiler/backend/semantics                            6m50s   2GB
Apr 24 06:33:39 Starting compiler/backend/reg_alloc/proofs
Apr 24 06:36:17 Finished compiler/backend/reg_alloc/proofs                     2m37s 763MB
Apr 24 06:36:17 Starting compiler/backend/proofs
Apr 24 07:13:14 Finished compiler/backend/proofs                              36m56s   5GB
Apr 24 07:13:15 Starting compiler/encoders/x64/proofs
Apr 24 07:22:10 Finished compiler/encoders/x64/proofs                          8m55s   4GB
Apr 24 07:22:11 Starting compiler/encoders/arm6/proofs
Apr 24 07:34:06 Finished compiler/encoders/arm6/proofs                        11m55s   3GB
Apr 24 07:34:07 Starting compiler/encoders/arm8/proofs
Apr 24 07:39:29 Finished compiler/encoders/arm8/proofs                         5m21s   1GB
Apr 24 07:39:29 Starting compiler/encoders/mips/proofs
Apr 24 07:48:42 Finished compiler/encoders/mips/proofs                         9m12s   2GB
Apr 24 07:48:42 Starting compiler/encoders/riscv/proofs
Apr 24 07:57:00 Finished compiler/encoders/riscv/proofs                        8m17s   1GB
Apr 24 07:57:00 Starting compiler/encoders/ag32/proofs
Apr 24 07:59:26 Finished compiler/encoders/ag32/proofs                         2m25s 956MB
Apr 24 07:59:26 Starting compiler/backend/x64/proofs
Apr 24 07:59:46 Finished compiler/backend/x64/proofs                             19s   1GB
Apr 24 07:59:46 Starting compiler/backend/arm6/proofs
Apr 24 08:00:08 Finished compiler/backend/arm6/proofs                            21s   1GB
Apr 24 08:00:09 Starting compiler/backend/arm8/proofs
Apr 24 08:00:27 Finished compiler/backend/arm8/proofs                            18s 819MB
Apr 24 08:00:27 Starting compiler/backend/mips/proofs
Apr 24 08:00:47 Finished compiler/backend/mips/proofs                            19s   1GB
Apr 24 08:00:48 Starting compiler/backend/riscv/proofs
Apr 24 08:01:08 Finished compiler/backend/riscv/proofs                           19s   1GB
Apr 24 08:01:08 Starting compiler/backend/ag32/proofs
Apr 24 08:09:52 Finished compiler/backend/ag32/proofs                          8m44s   1GB
Apr 24 08:09:53 Starting compiler/proofs
Apr 24 08:11:23 Finished compiler/proofs                                       1m29s   2GB
Apr 24 08:11:23 Starting candle/set-theory
Apr 24 08:11:50 Finished candle/set-theory                                       26s 819MB
Apr 24 08:11:50 Starting candle/syntax-lib
Apr 24 08:12:01 Finished candle/syntax-lib                                       10s 605MB
Apr 24 08:12:01 Starting candle/standard/syntax
Apr 24 08:13:45 Finished candle/standard/syntax                                1m43s   1GB
Apr 24 08:13:45 Starting candle/standard/semantics
Apr 24 08:15:22 Finished candle/standard/semantics                             1m36s   1GB
Apr 24 08:15:22 Starting candle/standard/monadic
Apr 24 08:16:55 Finished candle/standard/monadic                               1m32s   1GB
Apr 24 08:16:56 Starting candle/standard/ml_kernel
Apr 24 08:20:35 Finished candle/standard/ml_kernel                             3m38s   4GB
Apr 24 08:20:35 Starting candle/standard/opentheory
Apr 24 08:28:49 Finished candle/standard/opentheory                            8m14s   3GB
Apr 24 08:28:50 Starting candle/standard/opentheory/compilation
Apr 24 08:58:50 Finished candle/standard/opentheory/compilation               30m00s  13GB
Apr 24 08:58:51 Starting candle/standard/opentheory/compilation/proofs
Apr 24 08:59:27 Finished candle/standard/opentheory/compilation/proofs           36s   2GB
Apr 24 08:59:28 Starting characteristic/examples
Apr 24 09:00:55 Finished characteristic/examples                               1m26s   2GB
Apr 24 09:00:55 Starting tutorial/solutions
Apr 24 09:14:14 Finished tutorial/solutions                                   13m18s   5GB
Apr 24 09:14:14 Starting translator/monadic/examples
Apr 24 09:16:41 Finished translator/monadic/examples                           2m26s   2GB
Apr 24 09:16:41 Starting examples
Apr 24 09:24:57 Finished examples                                              8m16s   3GB
Apr 24 09:24:57 Starting examples/compilation/x64
Apr 24 11:17:12 Finished examples/compilation/x64                           1h52m13s  10GB
Apr 24 11:17:12 Starting examples/compilation/x64/proofs
Apr 24 11:18:38 Finished examples/compilation/x64/proofs                       1m25s   3GB
Apr 24 11:18:38 Starting examples/compilation/ag32
Apr 24 11:46:47 Finished examples/compilation/ag32                            28m08s   5GB
Apr 24 11:46:47 Starting examples/compilation/ag32/proofs
Apr 24 11:47:44 Finished examples/compilation/ag32/proofs                        56s   3GB
Apr 24 11:47:45 Starting translator/okasaki-examples
Apr 24 11:51:46 Finished translator/okasaki-examples                           4m00s   1GB
Apr 24 11:51:46 Starting translator/other-examples
Apr 24 11:52:29 Finished translator/other-examples                               42s   1GB
Apr 24 11:52:29 Starting compiler/parsing/tests
Apr 24 11:52:55 Finished compiler/parsing/tests                                  25s 581MB
Apr 24 11:52:55 Starting compiler/inference/tests
Apr 24 11:56:53 Finished compiler/inference/tests                              3m57s   4GB
Apr 24 11:56:53 Starting compiler/bootstrap/translation
Apr 24 14:17:11 Finished compiler/bootstrap/translation                     2h20m17s  41GB
Apr 24 14:17:11 Starting unverified/sexpr-bootstrap/x64/64
Apr 24 14:25:02 Finished unverified/sexpr-bootstrap/x64/64                     7m49s   3GB
Apr 24 14:25:02 Starting unverified/sexpr-bootstrap/x64/32
Apr 24 14:29:22 Finished unverified/sexpr-bootstrap/x64/32                     4m19s   5GB
Apr 24 14:29:22 Starting compiler/benchmarks
Apr 24 14:29:29 Finished compiler/benchmarks                                      6s  25MB
Apr 24 14:29:29 Starting compiler/bootstrap/compilation/x64/64
Apr 25 00:35:36 Finished compiler/bootstrap/compilation/x64/64             10h06m05s  64GB
Apr 25 00:35:36 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 25 00:38:52 Finished compiler/bootstrap/compilation/x64/64/proofs          3m15s   5GB
Apr 25 00:38:52 Starting compiler/bootstrap/compilation/x64/32
Apr 25 10:50:07 Finished compiler/bootstrap/compilation/x64/32             10h11m13s  64GB
Apr 25 10:50:07 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 25 10:53:26 Finished compiler/bootstrap/compilation/x64/32/proofs          3m18s   6GB
Apr 25 10:53:27 Starting compiler/bootstrap/compilation/ag32/32
Apr 25 20:37:52 Finished compiler/bootstrap/compilation/ag32/32             9h44m24s  64GB
Apr 25 20:37:52 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 25 20:53:44 Finished compiler/bootstrap/compilation/ag32/32/proofs        15m51s  13GB
Apr 25 20:53:44 SUCCESS