Job 1469

CakeML:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:684b665d7eb337ccab2173351f6356213e6d7e54
  Adjust signature names [Feb 05 04:46:20]
Machine:oven2 4.15.0-34-generic 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

Feb 06 20:50:05 Claimed job
Feb 06 20:50:09 Building HOL
Feb 06 21:04:19 Starting developers
Feb 06 21:04:19 Finished developers                                               0s  35MB
Feb 06 21:04:19 Starting developers/bin
Feb 06 21:04:25 Finished developers/bin                                           5s   1GB
Feb 06 21:04:26 Starting semantics/ffi
Feb 06 21:04:36 Finished semantics/ffi                                            9s 318MB
Feb 06 21:04:36 Starting semantics
Feb 06 21:06:07 Finished semantics                                             1m30s   1GB
Feb 06 21:06:07 Starting semantics/proofs
Feb 06 21:09:26 Finished semantics/proofs                                      3m18s   2GB
Feb 06 21:09:26 Starting semantics/alt_semantics
Feb 06 21:09:35 Finished semantics/alt_semantics                                  8s 411MB
Feb 06 21:09:35 Starting semantics/alt_semantics/proofs
Feb 06 21:11:42 Finished semantics/alt_semantics/proofs                        2m07s   1GB
Feb 06 21:11:43 Starting basis/pure
Feb 06 21:14:25 Finished basis/pure                                            2m42s   1GB
Feb 06 21:14:26 Starting translator
Feb 06 21:17:00 Finished translator                                            2m34s   2GB
Feb 06 21:17:00 Starting compiler/parsing
Feb 06 21:18:06 Finished compiler/parsing                                      1m05s   4GB
Feb 06 21:18:06 Starting characteristic
Feb 06 21:24:00 Finished characteristic                                        5m53s   3GB
Feb 06 21:24:00 Starting translator/monadic
Feb 06 21:25:43 Finished translator/monadic                                    1m42s   1GB
Feb 06 21:25:43 Starting basis
Feb 06 22:08:55 Finished basis                                                43m11s  24GB
Feb 06 22:08:55 Starting compiler/inference
Feb 06 22:10:03 Finished compiler/inference                                    1m07s   1GB
Feb 06 22:10:03 Starting compiler/backend/reg_alloc
Feb 06 22:11:07 Finished compiler/backend/reg_alloc                            1m03s   1GB
Feb 06 22:11:07 Starting compiler/backend/gc
Feb 06 22:14:40 Finished compiler/backend/gc                                   3m33s   3GB
Feb 06 22:14:40 Starting compiler/backend
Feb 06 22:19:42 Finished compiler/backend                                      5m01s   5GB
Feb 06 22:19:42 Starting compiler/encoders/asm
Feb 06 22:20:04 Finished compiler/encoders/asm                                   21s   1GB
Feb 06 22:20:04 Starting compiler/encoders/x64
Feb 06 22:21:07 Finished compiler/encoders/x64                                 1m02s   1GB
Feb 06 22:21:07 Starting compiler/encoders/arm7
Feb 06 22:23:11 Finished compiler/encoders/arm7                                2m03s   1GB
Feb 06 22:23:11 Starting compiler/encoders/arm8
Feb 06 22:23:50 Finished compiler/encoders/arm8                                  38s   1GB
Feb 06 22:23:50 Starting compiler/encoders/mips
Feb 06 22:25:16 Finished compiler/encoders/mips                                1m25s   1GB
Feb 06 22:25:16 Starting compiler/encoders/riscv
Feb 06 22:26:53 Finished compiler/encoders/riscv                               1m36s   1GB
Feb 06 22:26:53 Starting compiler/encoders/ag32
Feb 06 22:27:12 Finished compiler/encoders/ag32                                  18s 954MB
Feb 06 22:27:12 Starting compiler/backend/x64
Feb 06 22:27:32 Finished compiler/backend/x64                                    19s   1GB
Feb 06 22:27:32 Starting compiler/backend/arm7
Feb 06 22:27:54 Finished compiler/backend/arm7                                   22s   1GB
Feb 06 22:27:54 Starting compiler/backend/arm8
Feb 06 22:28:13 Finished compiler/backend/arm8                                   18s   1GB
Feb 06 22:28:13 Starting compiler/backend/mips
Feb 06 22:28:33 Finished compiler/backend/mips                                   19s   1GB
Feb 06 22:28:33 Starting compiler/backend/riscv
Feb 06 22:28:53 Finished compiler/backend/riscv                                  19s   1GB
Feb 06 22:28:53 Starting compiler/backend/ag32
Feb 06 22:30:02 Finished compiler/backend/ag32                                 1m08s   2GB
Feb 06 22:30:02 Starting compiler/parsing/proofs
Feb 06 22:35:30 Finished compiler/parsing/proofs                               5m27s   2GB
Feb 06 22:35:30 Starting compiler/inference/proofs
Feb 06 22:38:00 Finished compiler/inference/proofs                             2m29s   2GB
Feb 06 22:38:00 Starting compiler/backend/semantics
Feb 06 23:05:06 Finished compiler/backend/semantics                           27m05s   4GB
Feb 06 23:05:06 Starting compiler/backend/reg_alloc/proofs
Feb 06 23:08:22 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Feb 06 23:08:22 Starting compiler/backend/proofs
Feb 07 00:01:39 Finished compiler/backend/proofs                              53m16s  18GB
Feb 07 00:01:39 Starting compiler/encoders/x64/proofs
Feb 07 00:10:57 Finished compiler/encoders/x64/proofs                          9m18s   5GB
Feb 07 00:10:57 Starting compiler/encoders/arm7/proofs
Feb 07 00:23:24 Finished compiler/encoders/arm7/proofs                        12m26s   8GB
Feb 07 00:23:24 Starting compiler/encoders/arm8/proofs
Feb 07 00:29:52 Finished compiler/encoders/arm8/proofs                         6m27s   3GB
Feb 07 00:29:52 Starting compiler/encoders/mips/proofs
Feb 07 00:39:44 Finished compiler/encoders/mips/proofs                         9m51s   6GB
Feb 07 00:39:44 Starting compiler/encoders/riscv/proofs
Feb 07 00:48:12 Finished compiler/encoders/riscv/proofs                        8m27s   3GB
Feb 07 00:48:12 Starting compiler/encoders/ag32/proofs
Feb 07 00:50:32 Finished compiler/encoders/ag32/proofs                         2m19s   1GB
Feb 07 00:50:32 Starting compiler/backend/x64/proofs
Feb 07 00:50:53 Finished compiler/backend/x64/proofs                             21s   2GB
Feb 07 00:50:54 Starting compiler/backend/arm7/proofs
Feb 07 00:51:16 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 07 00:51:16 Starting compiler/backend/arm8/proofs
Feb 07 00:51:37 Finished compiler/backend/arm8/proofs                            20s   1GB
Feb 07 00:51:37 Starting compiler/backend/mips/proofs
Feb 07 00:51:59 Finished compiler/backend/mips/proofs                            21s   1GB
Feb 07 00:51:59 Starting compiler/backend/riscv/proofs
Feb 07 00:52:21 Finished compiler/backend/riscv/proofs                           21s   2GB
Feb 07 00:52:21 Starting compiler/backend/ag32/proofs
Feb 07 01:04:23 Finished compiler/backend/ag32/proofs                         12m01s   5GB
Feb 07 01:04:23 Starting compiler/proofs
Feb 07 01:06:19 Finished compiler/proofs                                       1m55s   6GB
Feb 07 01:06:19 Starting candle/set-theory
Feb 07 01:06:49 Finished candle/set-theory                                       29s   1GB
Feb 07 01:06:49 Starting candle/syntax-lib
Feb 07 01:07:01 Finished candle/syntax-lib                                       11s 793MB
Feb 07 01:07:01 Starting candle/standard/syntax
Feb 07 01:08:50 Finished candle/standard/syntax                                1m48s   1GB
Feb 07 01:08:50 Starting candle/standard/semantics
Feb 07 01:10:35 Finished candle/standard/semantics                             1m44s   2GB
Feb 07 01:10:35 Starting candle/standard/monadic
Feb 07 01:12:16 Finished candle/standard/monadic                               1m40s   1GB
Feb 07 01:12:16 Starting candle/standard/ml_kernel
Feb 07 01:17:31 Finished candle/standard/ml_kernel                             5m15s   6GB
Feb 07 01:17:31 Starting candle/overloading/syntax
Feb 07 01:20:40 Finished candle/overloading/syntax                             3m08s   1GB
Feb 07 01:20:40 Starting candle/overloading/semantics
Feb 07 01:32:45 Finished candle/overloading/semantics                         12m04s   8GB
Feb 07 01:32:45 Starting characteristic/examples
Feb 07 01:34:04 Finished characteristic/examples                               1m18s   4GB
Feb 07 01:34:04 Starting tutorial/solutions
Feb 07 01:49:04 Finished tutorial/solutions                                   14m59s  11GB
Feb 07 01:49:04 Starting translator/monadic/examples
Feb 07 01:52:24 Finished translator/monadic/examples                           3m19s   3GB
Feb 07 01:52:24 Starting examples
Feb 07 02:01:05 Finished examples                                              8m41s   9GB
Feb 07 02:01:05 Starting examples/compilation/x64
Feb 07 04:20:08 Finished examples/compilation/x64                           2h19m02s  19GB
Feb 07 04:20:08 Starting examples/compilation/x64/proofs
Feb 07 04:22:04 Finished examples/compilation/x64/proofs                       1m55s   3GB
Feb 07 04:22:04 Starting examples/compilation/ag32
Feb 07 04:54:50 Finished examples/compilation/ag32                            32m46s  17GB
Feb 07 04:54:50 Starting examples/compilation/ag32/proofs
Feb 07 04:55:40 Finished examples/compilation/ag32/proofs                        49s   5GB
Feb 07 04:55:40 Starting examples/cost
Feb 07 05:49:06 Finished examples/cost                                        53m25s  12GB
Feb 07 05:49:07 Starting examples/lpr_checker
Feb 07 05:52:55 Finished examples/lpr_checker                                  3m47s   5GB
Feb 07 05:52:55 Starting examples/lpr_checker/compilation
Feb 07 06:11:18 Finished examples/lpr_checker/compilation                     18m23s  15GB
Feb 07 06:11:19 Starting examples/lpr_checker/compilation/proofs
Feb 07 06:12:00 Finished examples/lpr_checker/compilation/proofs                 41s   4GB
Feb 07 06:12:00 Starting examples/lpr_checker/array
Feb 07 06:25:32 Finished examples/lpr_checker/array                           13m31s   5GB
Feb 07 06:25:32 Starting examples/lpr_checker/array/compilation
Feb 07 06:44:38 Finished examples/lpr_checker/array/compilation               19m05s  22GB
Feb 07 06:44:38 Starting examples/lpr_checker/array/compilation/proofs
Feb 07 06:45:28 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Feb 07 06:45:28 Starting examples/opentheory
Feb 07 06:54:46 Finished examples/opentheory                                   9m15s   8GB
Feb 07 06:54:47 Starting examples/opentheory
Feb 07 06:54:47 Finished examples/opentheory                                      0s 100MB
Feb 07 06:54:49 Starting examples/opentheory/compilation
Feb 07 07:26:41 Finished examples/opentheory/compilation                      31m51s  39GB
Feb 07 07:26:41 Starting examples/opentheory/compilation/proofs
Feb 07 07:27:23 Finished examples/opentheory/compilation/proofs                  42s   3GB
Feb 07 07:27:23 Starting examples/opentheory/compilation/ag32
Feb 07 07:59:30 Finished examples/opentheory/compilation/ag32                 32m04s  24GB
Feb 07 07:59:30 Starting examples/opentheory/compilation/ag32/proofs
Feb 07 08:01:06 Finished examples/opentheory/compilation/ag32/proofs           1m36s   8GB
Feb 07 08:01:06 Starting translator/okasaki-examples
Feb 07 08:05:12 Finished translator/okasaki-examples                           4m05s   3GB
Feb 07 08:05:12 Starting translator/other-examples
Feb 07 08:07:16 Finished translator/other-examples                             2m03s   1GB
Feb 07 08:07:16 Starting compiler/parsing/tests
Feb 07 08:07:41 Finished compiler/parsing/tests                                  24s 627MB
Feb 07 08:07:41 Starting compiler/inference/tests
Feb 07 08:14:45 Finished compiler/inference/tests                              7m03s   5GB
Feb 07 08:14:45 Starting compiler/bootstrap/translation
Feb 07 10:51:21 Finished compiler/bootstrap/translation                     2h36m35s  47GB
Feb 07 10:51:21 Starting unverified/sexpr-bootstrap/x64/64
Feb 07 11:04:09 Finished unverified/sexpr-bootstrap/x64/64                    12m06s   8GB
Feb 07 11:04:09 Starting unverified/sexpr-bootstrap/x64/32
Feb 07 11:15:10 Finished unverified/sexpr-bootstrap/x64/32                    10m25s   8GB
Feb 07 11:15:10 Starting compiler/benchmarks
Feb 07 11:53:26 Finished compiler/benchmarks                                  38m16s   2GB
Feb 07 11:53:26 Starting compiler/bootstrap/compilation/x64/64
Feb 08 04:41:28 Finished compiler/bootstrap/compilation/x64/64             16h47m34s  64GB
Feb 08 04:41:28 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 08 04:43:50 Finished compiler/bootstrap/compilation/x64/64/proofs          2m21s  14GB
Feb 08 04:43:50 Starting compiler/bootstrap/compilation/x64/32
Feb 08 18:42:08 Finished compiler/bootstrap/compilation/x64/32             13h57m56s  64GB
Feb 08 18:42:08 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 08 18:44:19 Finished compiler/bootstrap/compilation/x64/32/proofs          2m10s  18GB
Feb 08 18:44:19 Starting compiler/bootstrap/compilation/ag32/32
Feb 09 10:33:34 Finished compiler/bootstrap/compilation/ag32/32            15h49m14s  64GB
Feb 09 10:33:34 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 09 10:43:09 Finished compiler/bootstrap/compilation/ag32/32/proofs         9m35s  56GB
Feb 09 10:43:09 SUCCESS