Job 1472

CakeML:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:583808f6196b34844469aa95cb78bf855a62d80a
  Provide machinery for storing ssfragments by name in global db [Feb 08 06:30:26]
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

Feb 09 11:45:09 Claimed job
Feb 09 11:45:12 Building HOL
Feb 09 12:00:55 Starting developers
Feb 09 12:00:59 Finished developers                                               4s  81MB
Feb 09 12:00:59 Starting developers/bin
Feb 09 12:01:06 Finished developers/bin                                           6s   1GB
Feb 09 12:01:07 Starting semantics/ffi
Feb 09 12:01:18 Finished semantics/ffi                                           11s 230MB
Feb 09 12:01:18 Starting semantics
Feb 09 12:02:53 Finished semantics                                             1m34s   1GB
Feb 09 12:02:53 Starting semantics/proofs
Feb 09 12:06:30 Finished semantics/proofs                                      3m36s 938MB
Feb 09 12:06:30 Starting semantics/alt_semantics
Feb 09 12:06:39 Finished semantics/alt_semantics                                  8s 271MB
Feb 09 12:06:39 Starting semantics/alt_semantics/proofs
Feb 09 12:08:54 Finished semantics/alt_semantics/proofs                        2m14s   1GB
Feb 09 12:08:54 Starting basis/pure
Feb 09 12:11:58 Finished basis/pure                                            3m04s 929MB
Feb 09 12:11:59 Starting translator
Feb 09 12:14:45 Finished translator                                            2m46s   1GB
Feb 09 12:14:46 Starting compiler/parsing
Feb 09 12:15:59 Finished compiler/parsing                                      1m13s   3GB
Feb 09 12:16:00 Starting characteristic
Feb 09 12:22:13 Finished characteristic                                        6m13s   2GB
Feb 09 12:22:13 Starting translator/monadic
Feb 09 12:23:56 Finished translator/monadic                                    1m42s   1GB
Feb 09 12:23:56 Starting basis
Feb 09 13:10:44 Finished basis                                                46m47s  12GB
Feb 09 13:10:44 Starting compiler/inference
Feb 09 13:11:56 Finished compiler/inference                                    1m11s 934MB
Feb 09 13:11:56 Starting compiler/backend/reg_alloc
Feb 09 13:13:02 Finished compiler/backend/reg_alloc                            1m06s   1GB
Feb 09 13:13:03 Starting compiler/backend/gc
Feb 09 13:16:51 Finished compiler/backend/gc                                   3m48s   2GB
Feb 09 13:16:51 Starting compiler/backend
Feb 09 13:21:53 Finished compiler/backend                                      5m01s   4GB
Feb 09 13:21:53 Starting compiler/encoders/asm
Feb 09 13:22:16 Finished compiler/encoders/asm                                   23s 651MB
Feb 09 13:22:16 Starting compiler/encoders/x64
Feb 09 13:23:20 Finished compiler/encoders/x64                                 1m03s   1GB
Feb 09 13:23:20 Starting compiler/encoders/arm7
Feb 09 13:25:33 Finished compiler/encoders/arm7                                2m12s   1GB
Feb 09 13:25:33 Starting compiler/encoders/arm8
Feb 09 13:26:13 Finished compiler/encoders/arm8                                  40s 604MB
Feb 09 13:26:14 Starting compiler/encoders/mips
Feb 09 13:27:51 Finished compiler/encoders/mips                                1m37s   1GB
Feb 09 13:27:51 Starting compiler/encoders/riscv
Feb 09 13:29:41 Finished compiler/encoders/riscv                               1m49s   1GB
Feb 09 13:29:41 Starting compiler/encoders/ag32
Feb 09 13:30:00 Finished compiler/encoders/ag32                                  18s 840MB
Feb 09 13:30:00 Starting compiler/backend/x64
Feb 09 13:30:20 Finished compiler/backend/x64                                    19s   1GB
Feb 09 13:30:20 Starting compiler/backend/arm7
Feb 09 13:30:40 Finished compiler/backend/arm7                                   20s   1GB
Feb 09 13:30:40 Starting compiler/backend/arm8
Feb 09 13:30:59 Finished compiler/backend/arm8                                   18s   1GB
Feb 09 13:30:59 Starting compiler/backend/mips
Feb 09 13:31:19 Finished compiler/backend/mips                                   19s   1GB
Feb 09 13:31:20 Starting compiler/backend/riscv
Feb 09 13:31:40 Finished compiler/backend/riscv                                  19s   1GB
Feb 09 13:31:40 Starting compiler/backend/ag32
Feb 09 13:32:52 Finished compiler/backend/ag32                                 1m12s   1GB
Feb 09 13:32:52 Starting compiler/parsing/proofs
Feb 09 13:38:42 Finished compiler/parsing/proofs                               5m49s   1GB
Feb 09 13:38:42 Starting compiler/inference/proofs
Feb 09 13:41:18 Finished compiler/inference/proofs                             2m35s   1GB
Feb 09 13:41:18 Starting compiler/backend/semantics
Feb 09 14:14:52 Finished compiler/backend/semantics                           33m32s   2GB
Feb 09 14:14:52 Starting compiler/backend/reg_alloc/proofs
Feb 09 14:18:39 Finished compiler/backend/reg_alloc/proofs                     3m46s   1GB
Feb 09 14:18:39 Starting compiler/backend/proofs
Feb 09 15:17:19 Finished compiler/backend/proofs                              58m40s  16GB
Feb 09 15:17:20 Starting compiler/encoders/x64/proofs
Feb 09 15:27:45 Finished compiler/encoders/x64/proofs                         10m24s   4GB
Feb 09 15:27:45 Starting compiler/encoders/arm7/proofs
Feb 09 15:42:01 Finished compiler/encoders/arm7/proofs                        14m15s   2GB
Feb 09 15:42:01 Starting compiler/encoders/arm8/proofs
Feb 09 15:49:07 Finished compiler/encoders/arm8/proofs                         7m05s   1GB
Feb 09 15:49:07 Starting compiler/encoders/mips/proofs
Feb 09 15:59:54 Finished compiler/encoders/mips/proofs                        10m47s   1GB
Feb 09 15:59:54 Starting compiler/encoders/riscv/proofs
Feb 09 16:09:19 Finished compiler/encoders/riscv/proofs                        9m24s   1GB
Feb 09 16:09:20 Starting compiler/encoders/ag32/proofs
Feb 09 16:12:10 Finished compiler/encoders/ag32/proofs                         2m50s 649MB
Feb 09 16:12:10 Starting compiler/backend/x64/proofs
Feb 09 16:12:32 Finished compiler/backend/x64/proofs                             21s   1GB
Feb 09 16:12:33 Starting compiler/backend/arm7/proofs
Feb 09 16:12:55 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 09 16:12:56 Starting compiler/backend/arm8/proofs
Feb 09 16:13:16 Finished compiler/backend/arm8/proofs                            20s   1GB
Feb 09 16:13:16 Starting compiler/backend/mips/proofs
Feb 09 16:13:39 Finished compiler/backend/mips/proofs                            22s   1GB
Feb 09 16:13:39 Starting compiler/backend/riscv/proofs
Feb 09 16:14:01 Finished compiler/backend/riscv/proofs                           21s   1GB
Feb 09 16:14:01 Starting compiler/backend/ag32/proofs
Feb 09 16:27:25 Finished compiler/backend/ag32/proofs                         13m23s   3GB
Feb 09 16:27:25 Starting compiler/proofs
Feb 09 16:29:22 Finished compiler/proofs                                       1m56s   5GB
Feb 09 16:29:23 Starting candle/set-theory
Feb 09 16:29:52 Finished candle/set-theory                                       28s 754MB
Feb 09 16:29:52 Starting candle/syntax-lib
Feb 09 16:30:05 Finished candle/syntax-lib                                       11s 727MB
Feb 09 16:30:05 Starting candle/standard/syntax
Feb 09 16:32:00 Finished candle/standard/syntax                                1m55s 934MB
Feb 09 16:32:01 Starting candle/standard/semantics
Feb 09 16:33:51 Finished candle/standard/semantics                             1m49s   1GB
Feb 09 16:33:51 Starting candle/standard/monadic
Feb 09 16:35:40 Finished candle/standard/monadic                               1m48s   1GB
Feb 09 16:35:40 Starting candle/standard/ml_kernel
Feb 09 16:41:39 Finished candle/standard/ml_kernel                             5m58s   4GB
Feb 09 16:41:39 Starting candle/overloading/syntax
Feb 09 16:45:00 Finished candle/overloading/syntax                             3m20s   1GB
Feb 09 16:45:00 Starting candle/overloading/semantics
Feb 09 16:57:49 Finished candle/overloading/semantics                         12m49s   3GB
Feb 09 16:57:49 Starting characteristic/examples
Feb 09 16:59:09 Finished characteristic/examples                               1m19s   3GB
Feb 09 16:59:09 Starting tutorial/solutions
Feb 09 17:14:36 Finished tutorial/solutions                                   15m26s  10GB
Feb 09 17:14:36 Starting translator/monadic/examples
Feb 09 17:17:53 Finished translator/monadic/examples                           3m16s   2GB
Feb 09 17:17:53 Starting examples
Feb 09 17:26:53 Finished examples                                              8m59s   3GB
Feb 09 17:26:54 Starting examples/compilation/x64
Feb 09 19:53:28 Finished examples/compilation/x64                           2h26m34s  17GB
Feb 09 19:53:28 Starting examples/compilation/x64/proofs
Feb 09 19:55:14 Finished examples/compilation/x64/proofs                       1m45s   3GB
Feb 09 19:55:14 Starting examples/compilation/ag32
Feb 09 20:29:14 Finished examples/compilation/ag32                            33m59s   7GB
Feb 09 20:29:15 Starting examples/compilation/ag32/proofs
Feb 09 20:30:10 Finished examples/compilation/ag32/proofs                        55s   2GB
Feb 09 20:30:10 Starting examples/cost
Feb 09 21:28:10 Finished examples/cost                                        57m59s   8GB
Feb 09 21:28:10 Starting examples/lpr_checker
Feb 09 21:32:24 Finished examples/lpr_checker                                  4m12s   4GB
Feb 09 21:32:24 Starting examples/lpr_checker/compilation
Feb 09 21:51:08 Finished examples/lpr_checker/compilation                     18m44s  10GB
Feb 09 21:51:09 Starting examples/lpr_checker/compilation/proofs
Feb 09 21:51:48 Finished examples/lpr_checker/compilation/proofs                 39s   2GB
Feb 09 21:51:48 Starting examples/lpr_checker/array
Feb 09 22:07:16 Finished examples/lpr_checker/array                           15m27s   3GB
Feb 09 22:07:16 Starting examples/lpr_checker/array/compilation
Feb 09 22:27:51 Finished examples/lpr_checker/array/compilation               20m34s   9GB
Feb 09 22:27:51 Starting examples/lpr_checker/array/compilation/proofs
Feb 09 22:28:39 Finished examples/lpr_checker/array/compilation/proofs           47s   3GB
Feb 09 22:28:39 Starting examples/opentheory
Feb 09 22:38:53 Finished examples/opentheory                                  10m13s   4GB
Feb 09 22:38:53 Starting examples/opentheory
Feb 09 22:38:54 Finished examples/opentheory                                      1s  24MB
Feb 09 22:38:54 Starting examples/opentheory/compilation
Feb 09 23:12:30 Finished examples/opentheory/compilation                      33m35s  19GB
Feb 09 23:12:30 Starting examples/opentheory/compilation/proofs
Feb 09 23:13:11 Finished examples/opentheory/compilation/proofs                  41s   3GB
Feb 09 23:13:12 Starting examples/opentheory/compilation/ag32
Feb 09 23:47:35 Finished examples/opentheory/compilation/ag32                 34m23s  22GB
Feb 09 23:47:35 Starting examples/opentheory/compilation/ag32/proofs
Feb 09 23:49:15 Finished examples/opentheory/compilation/ag32/proofs           1m39s   6GB
Feb 09 23:49:15 Starting translator/okasaki-examples
Feb 09 23:53:42 Finished translator/okasaki-examples                           4m26s   1GB
Feb 09 23:53:42 Starting translator/other-examples
Feb 09 23:55:52 Finished translator/other-examples                             2m09s   1GB
Feb 09 23:55:52 Starting compiler/parsing/tests
Feb 09 23:56:19 Finished compiler/parsing/tests                                  27s 589MB
Feb 09 23:56:19 Starting compiler/inference/tests
Feb 10 00:04:12 Finished compiler/inference/tests                              7m51s   5GB
Feb 10 00:04:12 Starting compiler/bootstrap/translation
Feb 10 02:56:00 Finished compiler/bootstrap/translation                     2h51m47s  52GB
Feb 10 02:56:00 Starting unverified/sexpr-bootstrap/x64/64
Feb 10 03:08:39 Finished unverified/sexpr-bootstrap/x64/64                    12m00s   8GB
Feb 10 03:08:39 Starting unverified/sexpr-bootstrap/x64/32
Feb 10 03:19:04 Finished unverified/sexpr-bootstrap/x64/32                     9m52s  10GB
Feb 10 03:19:04 Starting compiler/benchmarks
Feb 10 03:19:06 Finished compiler/benchmarks                                      1s  27MB
Feb 10 03:19:06 Starting compiler/bootstrap/compilation/x64/64
Feb 10 15:53:07 Finished compiler/bootstrap/compilation/x64/64             12h33m35s  64GB
Feb 10 15:53:07 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 10 15:56:13 Finished compiler/bootstrap/compilation/x64/64/proofs          3m05s  13GB
Feb 10 15:56:13 Starting compiler/bootstrap/compilation/x64/32
Feb 11 03:07:24 Finished compiler/bootstrap/compilation/x64/32             11h10m48s  64GB
Feb 11 03:07:25 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 11 03:10:19 Finished compiler/bootstrap/compilation/x64/32/proofs          2m53s  11GB
Feb 11 03:10:19 Starting compiler/bootstrap/compilation/ag32/32
Feb 11 14:39:00 Finished compiler/bootstrap/compilation/ag32/32            11h28m40s  64GB
Feb 11 14:39:00 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 11 15:12:16 Finished compiler/bootstrap/compilation/ag32/32/proofs        33m16s  22GB
Feb 11 15:12:16 SUCCESS