Job 1474

CakeML:b39b4fb6cf973c84886fd436ede81ae7d70b3603
  Merge pull request #814 from CakeML/export_type [Feb 01 09:56:45]
HOL:9ff85ba156ed5501ffb3f4921ae639fb10ebb312
  Remove definitions.tex in DESCRIPTION manual's Holmakefile's EXTRA_CL [Feb 12 05:34:54]
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 15 07:10:59 Claimed job
Feb 15 07:11:07 Building HOL
Feb 15 07:25:25 Starting developers
Feb 15 07:25:26 Finished developers                                               0s  34MB
Feb 15 07:25:26 Starting developers/bin
Feb 15 07:25:32 Finished developers/bin                                           5s   1GB
Feb 15 07:25:32 Starting semantics/ffi
Feb 15 07:25:42 Finished semantics/ffi                                           10s 318MB
Feb 15 07:25:42 Starting semantics
Feb 15 07:27:15 Finished semantics                                             1m32s   1GB
Feb 15 07:27:15 Starting semantics/proofs
Feb 15 07:30:33 Finished semantics/proofs                                      3m17s   1GB
Feb 15 07:30:33 Starting semantics/alt_semantics
Feb 15 07:30:41 Finished semantics/alt_semantics                                  7s 367MB
Feb 15 07:30:41 Starting semantics/alt_semantics/proofs
Feb 15 07:32:50 Finished semantics/alt_semantics/proofs                        2m08s   1GB
Feb 15 07:32:50 Starting basis/pure
Feb 15 07:35:33 Finished basis/pure                                            2m42s   1GB
Feb 15 07:35:33 Starting translator
Feb 15 07:38:10 Finished translator                                            2m36s   2GB
Feb 15 07:38:10 Starting compiler/parsing
Feb 15 07:39:16 Finished compiler/parsing                                      1m05s   4GB
Feb 15 07:39:17 Starting characteristic
Feb 15 07:45:07 Finished characteristic                                        5m50s   3GB
Feb 15 07:45:07 Starting translator/monadic
Feb 15 07:46:49 Finished translator/monadic                                    1m41s   2GB
Feb 15 07:46:50 Starting basis
Feb 15 08:30:03 Finished basis                                                43m13s  22GB
Feb 15 08:30:03 Starting compiler/inference
Feb 15 08:31:11 Finished compiler/inference                                    1m07s   1GB
Feb 15 08:31:11 Starting compiler/backend/reg_alloc
Feb 15 08:32:15 Finished compiler/backend/reg_alloc                            1m03s   2GB
Feb 15 08:32:15 Starting compiler/backend/gc
Feb 15 08:35:50 Finished compiler/backend/gc                                   3m35s   4GB
Feb 15 08:35:50 Starting compiler/backend
Feb 15 08:40:54 Finished compiler/backend                                      5m04s   4GB
Feb 15 08:40:55 Starting compiler/encoders/asm
Feb 15 08:41:17 Finished compiler/encoders/asm                                   22s   1GB
Feb 15 08:41:17 Starting compiler/encoders/x64
Feb 15 08:42:20 Finished compiler/encoders/x64                                 1m02s   1GB
Feb 15 08:42:21 Starting compiler/encoders/arm7
Feb 15 08:44:23 Finished compiler/encoders/arm7                                2m02s   1GB
Feb 15 08:44:24 Starting compiler/encoders/arm8
Feb 15 08:45:03 Finished compiler/encoders/arm8                                  38s   1GB
Feb 15 08:45:03 Starting compiler/encoders/mips
Feb 15 08:46:28 Finished compiler/encoders/mips                                1m25s   1GB
Feb 15 08:46:28 Starting compiler/encoders/riscv
Feb 15 08:48:04 Finished compiler/encoders/riscv                               1m36s   1GB
Feb 15 08:48:05 Starting compiler/encoders/ag32
Feb 15 08:48:23 Finished compiler/encoders/ag32                                  17s 940MB
Feb 15 08:48:23 Starting compiler/backend/x64
Feb 15 08:48:42 Finished compiler/backend/x64                                    19s   1GB
Feb 15 08:48:43 Starting compiler/backend/arm7
Feb 15 08:49:04 Finished compiler/backend/arm7                                   21s   1GB
Feb 15 08:49:04 Starting compiler/backend/arm8
Feb 15 08:49:24 Finished compiler/backend/arm8                                   19s   1GB
Feb 15 08:49:25 Starting compiler/backend/mips
Feb 15 08:49:45 Finished compiler/backend/mips                                   20s   1GB
Feb 15 08:49:45 Starting compiler/backend/riscv
Feb 15 08:50:05 Finished compiler/backend/riscv                                  19s   1GB
Feb 15 08:50:05 Starting compiler/backend/ag32
Feb 15 08:51:16 Finished compiler/backend/ag32                                 1m10s   2GB
Feb 15 08:51:16 Starting compiler/parsing/proofs
Feb 15 08:56:41 Finished compiler/parsing/proofs                               5m25s   2GB
Feb 15 08:56:41 Starting compiler/inference/proofs
Feb 15 08:59:11 Finished compiler/inference/proofs                             2m29s   2GB
Feb 15 08:59:11 Starting compiler/backend/semantics
Feb 15 09:26:00 Finished compiler/backend/semantics                           26m48s   2GB
Feb 15 09:26:00 Starting compiler/backend/reg_alloc/proofs
Feb 15 09:29:17 Finished compiler/backend/reg_alloc/proofs                     3m16s   1GB
Feb 15 09:29:17 Starting compiler/backend/proofs
Feb 15 10:23:03 Finished compiler/backend/proofs                              53m45s  19GB
Feb 15 10:23:03 Starting compiler/encoders/x64/proofs
Feb 15 10:32:21 Finished compiler/encoders/x64/proofs                          9m17s   8GB
Feb 15 10:32:21 Starting compiler/encoders/arm7/proofs
Feb 15 10:45:02 Finished compiler/encoders/arm7/proofs                        12m41s  10GB
Feb 15 10:45:02 Starting compiler/encoders/arm8/proofs
Feb 15 10:51:35 Finished compiler/encoders/arm8/proofs                         6m31s   4GB
Feb 15 10:51:35 Starting compiler/encoders/mips/proofs
Feb 15 11:01:22 Finished compiler/encoders/mips/proofs                         9m47s   6GB
Feb 15 11:01:22 Starting compiler/encoders/riscv/proofs
Feb 15 11:09:41 Finished compiler/encoders/riscv/proofs                        8m18s   3GB
Feb 15 11:09:41 Starting compiler/encoders/ag32/proofs
Feb 15 11:12:01 Finished compiler/encoders/ag32/proofs                         2m20s   1GB
Feb 15 11:12:02 Starting compiler/backend/x64/proofs
Feb 15 11:12:23 Finished compiler/backend/x64/proofs                             20s   2GB
Feb 15 11:12:23 Starting compiler/backend/arm7/proofs
Feb 15 11:12:46 Finished compiler/backend/arm7/proofs                            22s   1GB
Feb 15 11:12:46 Starting compiler/backend/arm8/proofs
Feb 15 11:13:06 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 15 11:13:06 Starting compiler/backend/mips/proofs
Feb 15 11:13:28 Finished compiler/backend/mips/proofs                            21s   1GB
Feb 15 11:13:28 Starting compiler/backend/riscv/proofs
Feb 15 11:13:50 Finished compiler/backend/riscv/proofs                           22s   2GB
Feb 15 11:13:50 Starting compiler/backend/ag32/proofs
Feb 15 11:25:50 Finished compiler/backend/ag32/proofs                         11m59s   4GB
Feb 15 11:25:50 Starting compiler/proofs
Feb 15 11:27:42 Finished compiler/proofs                                       1m52s   6GB
Feb 15 11:27:43 Starting candle/set-theory
Feb 15 11:28:12 Finished candle/set-theory                                       29s   1GB
Feb 15 11:28:12 Starting candle/syntax-lib
Feb 15 11:28:23 Finished candle/syntax-lib                                       10s 828MB
Feb 15 11:28:24 Starting candle/standard/syntax
Feb 15 11:30:13 Finished candle/standard/syntax                                1m49s   1GB
Feb 15 11:30:13 Starting candle/standard/semantics
Feb 15 11:32:00 Finished candle/standard/semantics                             1m46s   2GB
Feb 15 11:32:00 Starting candle/standard/monadic
Feb 15 11:33:40 Finished candle/standard/monadic                               1m40s   1GB
Feb 15 11:33:41 Starting candle/standard/ml_kernel
Feb 15 11:39:03 Finished candle/standard/ml_kernel                             5m22s   7GB
Feb 15 11:39:03 Starting candle/overloading/syntax
Feb 15 11:42:14 Finished candle/overloading/syntax                             3m10s   1GB
Feb 15 11:42:14 Starting candle/overloading/semantics
Feb 15 11:54:17 Finished candle/overloading/semantics                         12m03s  10GB
Feb 15 11:54:18 Starting characteristic/examples
Feb 15 11:55:36 Finished characteristic/examples                               1m18s   4GB
Feb 15 11:55:36 Starting tutorial/solutions
Feb 15 12:10:34 Finished tutorial/solutions                                   14m57s  14GB
Feb 15 12:10:34 Starting translator/monadic/examples
Feb 15 12:13:51 Finished translator/monadic/examples                           3m17s   4GB
Feb 15 12:13:52 Starting examples
Feb 15 12:22:29 Finished examples                                              8m37s   7GB
Feb 15 12:22:29 Starting examples/compilation/x64
Feb 15 14:39:38 Finished examples/compilation/x64                           2h17m08s  30GB
Feb 15 14:39:38 Starting examples/compilation/x64/proofs
Feb 15 14:41:33 Finished examples/compilation/x64/proofs                       1m54s   3GB
Feb 15 14:41:33 Starting examples/compilation/ag32
Feb 15 15:14:23 Finished examples/compilation/ag32                            32m49s  17GB
Feb 15 15:14:24 Starting examples/compilation/ag32/proofs
Feb 15 15:15:18 Finished examples/compilation/ag32/proofs                        54s   4GB
Feb 15 15:15:18 Starting examples/cost
Feb 15 16:08:54 Finished examples/cost                                        53m35s  13GB
Feb 15 16:08:54 Starting examples/lpr_checker
Feb 15 16:12:44 Finished examples/lpr_checker                                  3m50s   3GB
Feb 15 16:12:44 Starting examples/lpr_checker/compilation
Feb 15 16:31:00 Finished examples/lpr_checker/compilation                     18m15s  13GB
Feb 15 16:31:00 Starting examples/lpr_checker/compilation/proofs
Feb 15 16:31:43 Finished examples/lpr_checker/compilation/proofs                 42s   4GB
Feb 15 16:31:43 Starting examples/lpr_checker/array
Feb 15 16:45:23 Finished examples/lpr_checker/array                           13m39s   5GB
Feb 15 16:45:23 Starting examples/lpr_checker/array/compilation
Feb 15 17:05:05 Finished examples/lpr_checker/array/compilation               19m41s  15GB
Feb 15 17:05:05 Starting examples/lpr_checker/array/compilation/proofs
Feb 15 17:05:54 Finished examples/lpr_checker/array/compilation/proofs           48s   4GB
Feb 15 17:05:54 Starting examples/opentheory
Feb 15 17:15:10 Finished examples/opentheory                                   9m14s   5GB
Feb 15 17:15:11 Starting examples/opentheory
Feb 15 17:15:11 Finished examples/opentheory                                      0s 100MB
Feb 15 17:15:12 Starting examples/opentheory/compilation
Feb 15 17:47:00 Finished examples/opentheory/compilation                      31m48s  20GB
Feb 15 17:47:00 Starting examples/opentheory/compilation/proofs
Feb 15 17:47:43 Finished examples/opentheory/compilation/proofs                  42s   4GB
Feb 15 17:47:43 Starting examples/opentheory/compilation/ag32
Feb 15 18:20:35 Finished examples/opentheory/compilation/ag32                 32m51s  21GB
Feb 15 18:20:36 Starting examples/opentheory/compilation/ag32/proofs
Feb 15 18:22:09 Finished examples/opentheory/compilation/ag32/proofs           1m33s   9GB
Feb 15 18:22:09 Starting translator/okasaki-examples
Feb 15 18:26:22 Finished translator/okasaki-examples                           4m12s   2GB
Feb 15 18:26:22 Starting translator/other-examples
Feb 15 18:28:27 Finished translator/other-examples                             2m04s   1GB
Feb 15 18:28:27 Starting compiler/parsing/tests
Feb 15 18:28:52 Finished compiler/parsing/tests                                  24s 713MB
Feb 15 18:28:52 Starting compiler/inference/tests
Feb 15 18:36:07 Finished compiler/inference/tests                              7m15s   6GB
Feb 15 18:36:08 Starting compiler/bootstrap/translation
Feb 15 21:11:29 Finished compiler/bootstrap/translation                     2h35m21s  48GB
Feb 15 21:11:29 Starting unverified/sexpr-bootstrap/x64/64
Feb 15 21:24:13 Finished unverified/sexpr-bootstrap/x64/64                    12m09s   8GB
Feb 15 21:24:13 Starting unverified/sexpr-bootstrap/x64/32
Feb 15 21:35:10 Finished unverified/sexpr-bootstrap/x64/32                    10m30s   8GB
Feb 15 21:35:10 Starting compiler/benchmarks
Feb 15 22:12:59 Finished compiler/benchmarks                                  37m48s   2GB
Feb 15 22:12:59 Starting compiler/bootstrap/compilation/x64/64
Feb 16 15:01:21 Finished compiler/bootstrap/compilation/x64/64             16h47m57s  64GB
Feb 16 15:01:21 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 16 15:03:34 Finished compiler/bootstrap/compilation/x64/64/proofs          2m12s  16GB
Feb 16 15:03:34 Starting compiler/bootstrap/compilation/x64/32
Feb 17 05:45:15 Finished compiler/bootstrap/compilation/x64/32             14h41m26s  64GB
Feb 17 05:45:16 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 17 05:47:23 Finished compiler/bootstrap/compilation/x64/32/proofs          2m07s  15GB
Feb 17 05:47:23 Starting compiler/bootstrap/compilation/ag32/32
Feb 17 21:01:05 Finished compiler/bootstrap/compilation/ag32/32            15h13m41s  64GB
Feb 17 21:01:05 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 17 21:15:20 Finished compiler/bootstrap/compilation/ag32/32/proofs        14m14s  56GB
Feb 17 21:15:21 SUCCESS