Job 816

CakeML:508d7a343895a77b21740222cd97d822e3c35b28
  Fixes following changes to file names [Apr 24 12:58:23]
#627 (monadic-trans-cleanup)
Merging into: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:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 25 02:37:10 Claimed job
Apr 25 02:37:21 Reusing HOL
Apr 25 02:37:27 Starting developers
Apr 25 02:37:27 Finished developers                                               0s  28MB
Apr 25 02:37:28 Starting developers/bin
Apr 25 02:38:04 Finished developers/bin                                          35s 205MB
Apr 25 02:38:04 Starting semantics/ffi
Apr 25 02:38:12 Finished semantics/ffi                                            7s 212MB
Apr 25 02:38:12 Starting semantics
Apr 25 02:39:32 Finished semantics                                             1m18s   1GB
Apr 25 02:39:32 Starting semantics/proofs
Apr 25 02:42:28 Finished semantics/proofs                                      2m55s 934MB
Apr 25 02:42:29 Starting basis/pure
Apr 25 02:43:15 Finished basis/pure                                              45s 649MB
Apr 25 02:43:15 Starting translator
Apr 25 02:44:54 Finished translator                                            1m39s   1GB
Apr 25 02:44:55 Starting compiler/parsing
Apr 25 02:45:54 Finished compiler/parsing                                        58s   1GB
Apr 25 02:45:55 Starting characteristic
Apr 25 02:51:03 Finished characteristic                                        5m08s   2GB
Apr 25 02:51:03 Starting translator/monadic
Apr 25 02:52:27 Finished translator/monadic                                    1m23s   1GB
Apr 25 02:52:27 Starting basis
Apr 25 03:09:16 Finished basis                                                16m48s   2GB
Apr 25 03:09:16 Starting compiler/inference
Apr 25 03:10:46 Finished compiler/inference                                    1m30s   1GB
Apr 25 03:10:47 Starting compiler/backend/reg_alloc
Apr 25 03:11:45 Finished compiler/backend/reg_alloc                              57s   1GB
Apr 25 03:11:46 Starting compiler/backend/gc
Apr 25 03:19:51 Finished compiler/backend/gc                                   8m05s   2GB
Apr 25 03:19:52 Starting compiler/backend
Apr 25 03:19:53 Finished compiler/backend                                         0s  42MB
Apr 25 03:19:53 Starting compiler/encoders/asm
Apr 25 03:19:54 Finished compiler/encoders/asm                                    0s  32MB
Apr 25 03:19:54 Starting compiler/encoders/x64
Apr 25 03:20:17 Finished compiler/encoders/x64                                   22s 961MB
Apr 25 03:20:17 Starting compiler/encoders/arm6
Apr 25 03:21:02 Finished compiler/encoders/arm6                                  44s 754MB
Apr 25 03:21:02 Starting compiler/encoders/arm8
Apr 25 03:21:14 Finished compiler/encoders/arm8                                  11s 899MB
Apr 25 03:21:14 Starting compiler/encoders/mips
Apr 25 03:21:30 Finished compiler/encoders/mips                                  15s   1GB
Apr 25 03:21:31 Starting compiler/encoders/riscv
Apr 25 03:21:44 Finished compiler/encoders/riscv                                 13s 876MB
Apr 25 03:21:44 Starting compiler/encoders/ag32
Apr 25 03:22:00 Finished compiler/encoders/ag32                                  15s 665MB
Apr 25 03:22:00 Starting compiler/backend/x64
Apr 25 03:22:16 Finished compiler/backend/x64                                    14s 860MB
Apr 25 03:22:16 Starting compiler/backend/arm6
Apr 25 03:22:35 Finished compiler/backend/arm6                                   17s   1GB
Apr 25 03:22:35 Starting compiler/backend/arm8
Apr 25 03:22:50 Finished compiler/backend/arm8                                   14s 971MB
Apr 25 03:22:51 Starting compiler/backend/mips
Apr 25 03:23:07 Finished compiler/backend/mips                                   16s   1GB
Apr 25 03:23:08 Starting compiler/backend/riscv
Apr 25 03:23:24 Finished compiler/backend/riscv                                  16s   1GB
Apr 25 03:23:25 Starting compiler/backend/ag32
Apr 25 03:24:33 Finished compiler/backend/ag32                                 1m08s   1GB
Apr 25 03:24:34 Starting compiler/parsing/proofs
Apr 25 03:30:07 Finished compiler/parsing/proofs                               5m32s 904MB
Apr 25 03:30:07 Starting compiler/inference/proofs
Apr 25 03:32:48 Finished compiler/inference/proofs                             2m40s   1GB
Apr 25 03:32:48 Starting compiler/backend/semantics
Apr 25 03:39:59 Finished compiler/backend/semantics                            7m10s   1GB
Apr 25 03:39:59 Starting compiler/backend/reg_alloc/proofs
Apr 25 03:43:18 Finished compiler/backend/reg_alloc/proofs                     3m18s 910MB
Apr 25 03:43:19 Starting compiler/backend/proofs
Apr 25 04:21:53 Finished compiler/backend/proofs                              38m34s   3GB
Apr 25 04:21:54 Starting compiler/encoders/x64/proofs
Apr 25 04:31:04 Finished compiler/encoders/x64/proofs                          9m09s   5GB
Apr 25 04:31:04 Starting compiler/encoders/arm6/proofs
Apr 25 04:43:39 Finished compiler/encoders/arm6/proofs                        12m33s   3GB
Apr 25 04:43:39 Starting compiler/encoders/arm8/proofs
Apr 25 04:49:19 Finished compiler/encoders/arm8/proofs                         5m39s   1GB
Apr 25 04:49:19 Starting compiler/encoders/mips/proofs
Apr 25 04:58:52 Finished compiler/encoders/mips/proofs                         9m32s   2GB
Apr 25 04:58:52 Starting compiler/encoders/riscv/proofs
Apr 25 05:07:27 Finished compiler/encoders/riscv/proofs                        8m33s   1GB
Apr 25 05:07:27 Starting compiler/encoders/ag32/proofs
Apr 25 05:09:57 Finished compiler/encoders/ag32/proofs                         2m29s 890MB
Apr 25 05:09:57 Starting compiler/backend/x64/proofs
Apr 25 05:10:14 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 25 05:10:14 Starting compiler/backend/arm6/proofs
Apr 25 05:10:34 Finished compiler/backend/arm6/proofs                            19s   1GB
Apr 25 05:10:34 Starting compiler/backend/arm8/proofs
Apr 25 05:10:50 Finished compiler/backend/arm8/proofs                            15s   1GB
Apr 25 05:10:51 Starting compiler/backend/mips/proofs
Apr 25 05:11:08 Finished compiler/backend/mips/proofs                            17s   1GB
Apr 25 05:11:08 Starting compiler/backend/riscv/proofs
Apr 25 05:11:25 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 25 05:11:26 Starting compiler/backend/ag32/proofs
Apr 25 05:20:41 Finished compiler/backend/ag32/proofs                          9m14s   3GB
Apr 25 05:20:41 Starting compiler/proofs
Apr 25 05:22:01 Finished compiler/proofs                                       1m19s   2GB
Apr 25 05:22:01 Starting candle/set-theory
Apr 25 05:22:27 Finished candle/set-theory                                       25s 676MB
Apr 25 05:22:27 Starting candle/syntax-lib
Apr 25 05:22:37 Finished candle/syntax-lib                                        9s 614MB
Apr 25 05:22:37 Starting candle/standard/syntax
Apr 25 05:24:19 Finished candle/standard/syntax                                1m41s   1GB
Apr 25 05:24:19 Starting candle/standard/semantics
Apr 25 05:25:53 Finished candle/standard/semantics                             1m33s   1GB
Apr 25 05:25:54 Starting candle/standard/monadic
Apr 25 05:27:28 Finished candle/standard/monadic                               1m34s   1GB
Apr 25 05:27:28 Starting candle/standard/ml_kernel
Apr 25 05:31:14 Finished candle/standard/ml_kernel                             3m44s   3GB
Apr 25 05:31:14 Starting candle/standard/opentheory
Apr 25 05:39:44 Finished candle/standard/opentheory                            8m29s   3GB
Apr 25 05:39:44 Starting candle/standard/opentheory/compilation
Apr 25 06:10:26 Finished candle/standard/opentheory/compilation               30m41s  22GB
Apr 25 06:10:26 Starting candle/standard/opentheory/compilation/proofs
Apr 25 06:11:01 Finished candle/standard/opentheory/compilation/proofs           34s   2GB
Apr 25 06:11:02 Starting characteristic/examples
Apr 25 06:12:27 Finished characteristic/examples                               1m24s   2GB
Apr 25 06:12:27 Starting tutorial/solutions
Apr 25 06:25:29 Finished tutorial/solutions                                   13m01s   6GB
Apr 25 06:25:30 Starting translator/monadic/examples
Apr 25 06:28:23 Finished translator/monadic/examples                           2m53s   2GB
Apr 25 06:28:24 Starting examples
Apr 25 06:36:57 Finished examples                                              8m32s   3GB
Apr 25 06:36:57 Starting examples/compilation/x64
Apr 25 08:34:00 Finished examples/compilation/x64                           1h57m02s  11GB
Apr 25 08:34:01 Starting examples/compilation/x64/proofs
Apr 25 08:35:32 Finished examples/compilation/x64/proofs                       1m30s   2GB
Apr 25 08:35:32 Starting examples/compilation/ag32
Apr 25 09:03:54 Finished examples/compilation/ag32                            28m21s   6GB
Apr 25 09:03:54 Starting examples/compilation/ag32/proofs
Apr 25 09:04:53 Finished examples/compilation/ag32/proofs                        58s   2GB
Apr 25 09:04:53 Starting translator/okasaki-examples
Apr 25 09:09:05 Finished translator/okasaki-examples                           4m11s   1GB
Apr 25 09:09:05 Starting translator/other-examples
Apr 25 09:09:46 Finished translator/other-examples                               40s   1GB
Apr 25 09:09:46 Starting compiler/parsing/tests
Apr 25 09:10:11 Finished compiler/parsing/tests                                  24s 525MB
Apr 25 09:10:11 Starting compiler/inference/tests
Apr 25 09:14:24 Finished compiler/inference/tests                              4m12s   3GB
Apr 25 09:14:25 Starting compiler/bootstrap/translation
Apr 25 11:44:26 Finished compiler/bootstrap/translation                     2h30m00s  54GB
Apr 25 11:44:26 Starting unverified/sexpr-bootstrap/x64/64
Apr 25 11:51:59 Finished unverified/sexpr-bootstrap/x64/64                     7m32s   2GB
Apr 25 11:52:00 Starting unverified/sexpr-bootstrap/x64/32
Apr 25 11:56:31 Finished unverified/sexpr-bootstrap/x64/32                     4m30s   4GB
Apr 25 11:56:32 Starting compiler/benchmarks
Apr 25 12:33:22 Finished compiler/benchmarks                                  36m49s   2GB
Apr 25 12:33:22 Starting compiler/bootstrap/compilation/x64/64
Apr 26 00:12:03 Finished compiler/bootstrap/compilation/x64/64             11h38m40s  64GB
Apr 26 00:12:03 Starting compiler/bootstrap/compilation/x64/64/proofs
Apr 26 00:15:49 Finished compiler/bootstrap/compilation/x64/64/proofs          3m44s   7GB
Apr 26 00:15:49 Starting compiler/bootstrap/compilation/x64/32
Apr 26 09:32:05 Finished compiler/bootstrap/compilation/x64/32              9h16m15s  63GB
Apr 26 09:32:05 Starting compiler/bootstrap/compilation/x64/32/proofs
Apr 26 09:35:30 Finished compiler/bootstrap/compilation/x64/32/proofs          3m24s   6GB
Apr 26 09:35:30 Starting compiler/bootstrap/compilation/ag32/32
Apr 26 20:16:40 Finished compiler/bootstrap/compilation/ag32/32            10h41m08s  64GB
Apr 26 20:16:40 Starting compiler/bootstrap/compilation/ag32/32/proofs
Apr 26 20:38:03 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m22s  11GB
Apr 26 20:38:03 SUCCESS