Job 1519

CakeML:dcd58cdc43ac870ace95e4a30c7e59f5e555d533
  Merge pull request #827 from CakeML/hex [May 06 07:47:53]
HOL:42c6babbdc8d94d05727b183c188c11aefdbcd80
  Revise name-carrying FOL system to have explicit "weakening" option [May 04 07:07:23]
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

May 06 14:52:33 Claimed job
May 06 14:52:38 Building HOL
May 06 15:09:03 Starting developers
May 06 15:09:07 Finished developers                                               4s 119MB
May 06 15:09:07 Starting developers/bin
May 06 15:09:14 Finished developers/bin                                           6s   1GB
May 06 15:09:15 Starting semantics/ffi
May 06 15:09:26 Finished semantics/ffi                                           11s 232MB
May 06 15:09:26 Starting semantics
May 06 15:11:03 Finished semantics                                             1m36s   1GB
May 06 15:11:04 Starting semantics/proofs
May 06 15:14:57 Finished semantics/proofs                                      3m53s   1GB
May 06 15:14:57 Starting semantics/alt_semantics
May 06 15:15:07 Finished semantics/alt_semantics                                  9s 295MB
May 06 15:15:07 Starting semantics/alt_semantics/proofs
May 06 15:17:30 Finished semantics/alt_semantics/proofs                        2m22s 839MB
May 06 15:17:30 Starting basis/pure
May 06 15:20:41 Finished basis/pure                                            3m10s 875MB
May 06 15:20:41 Starting translator
May 06 15:24:17 Finished translator                                            3m36s   1GB
May 06 15:24:18 Starting compiler/parsing
May 06 15:25:34 Finished compiler/parsing                                      1m16s   2GB
May 06 15:25:34 Starting characteristic
May 06 15:31:28 Finished characteristic                                        5m53s   2GB
May 06 15:31:28 Starting translator/monadic
May 06 15:33:10 Finished translator/monadic                                    1m41s   1GB
May 06 15:33:10 Starting basis
May 06 16:20:42 Finished basis                                                47m31s  14GB
May 06 16:20:42 Starting compiler/inference
May 06 16:22:01 Finished compiler/inference                                    1m18s   1GB
May 06 16:22:02 Starting compiler/backend/reg_alloc
May 06 16:23:12 Finished compiler/backend/reg_alloc                            1m09s   1GB
May 06 16:23:12 Starting compiler/backend/gc
May 06 16:27:02 Finished compiler/backend/gc                                   3m50s   2GB
May 06 16:27:02 Starting compiler/backend
May 06 16:32:14 Finished compiler/backend                                      5m11s   3GB
May 06 16:32:14 Starting compiler/encoders/asm
May 06 16:32:37 Finished compiler/encoders/asm                                   22s 741MB
May 06 16:32:37 Starting compiler/encoders/x64
May 06 16:33:44 Finished compiler/encoders/x64                                 1m06s 820MB
May 06 16:33:44 Starting compiler/encoders/arm7
May 06 16:35:58 Finished compiler/encoders/arm7                                2m13s   1GB
May 06 16:35:58 Starting compiler/encoders/arm8
May 06 16:36:38 Finished compiler/encoders/arm8                                  39s 953MB
May 06 16:36:38 Starting compiler/encoders/mips
May 06 16:38:15 Finished compiler/encoders/mips                                1m36s   1GB
May 06 16:38:15 Starting compiler/encoders/riscv
May 06 16:40:03 Finished compiler/encoders/riscv                               1m47s 958MB
May 06 16:40:04 Starting compiler/encoders/ag32
May 06 16:40:22 Finished compiler/encoders/ag32                                  18s 765MB
May 06 16:40:23 Starting compiler/backend/x64
May 06 16:40:43 Finished compiler/backend/x64                                    19s   1GB
May 06 16:40:43 Starting compiler/backend/arm7
May 06 16:41:04 Finished compiler/backend/arm7                                   21s   1GB
May 06 16:41:04 Starting compiler/backend/arm8
May 06 16:41:24 Finished compiler/backend/arm8                                   19s   1GB
May 06 16:41:25 Starting compiler/backend/mips
May 06 16:41:45 Finished compiler/backend/mips                                   19s   1GB
May 06 16:41:45 Starting compiler/backend/riscv
May 06 16:42:06 Finished compiler/backend/riscv                                  20s   1GB
May 06 16:42:06 Starting compiler/backend/ag32
May 06 16:43:19 Finished compiler/backend/ag32                                 1m12s   1GB
May 06 16:43:19 Starting compiler/parsing/proofs
May 06 16:49:30 Finished compiler/parsing/proofs                               6m10s   1GB
May 06 16:49:30 Starting compiler/inference/proofs
May 06 16:52:11 Finished compiler/inference/proofs                             2m40s   1GB
May 06 16:52:11 Starting compiler/backend/semantics
May 06 17:25:24 Finished compiler/backend/semantics                           33m12s   2GB
May 06 17:25:24 Starting compiler/backend/reg_alloc/proofs
May 06 17:29:13 Finished compiler/backend/reg_alloc/proofs                     3m48s   1GB
May 06 17:29:13 Starting compiler/backend/proofs
May 06 18:28:39 Finished compiler/backend/proofs                              59m25s  17GB
May 06 18:28:39 Starting compiler/encoders/x64/proofs
May 06 18:39:09 Finished compiler/encoders/x64/proofs                         10m28s   5GB
May 06 18:39:09 Starting compiler/encoders/arm7/proofs
May 06 18:53:36 Finished compiler/encoders/arm7/proofs                        14m26s   3GB
May 06 18:53:36 Starting compiler/encoders/arm8/proofs
May 06 19:01:02 Finished compiler/encoders/arm8/proofs                         7m25s   1GB
May 06 19:01:02 Starting compiler/encoders/mips/proofs
May 06 19:11:51 Finished compiler/encoders/mips/proofs                        10m49s   2GB
May 06 19:11:52 Starting compiler/encoders/riscv/proofs
May 06 19:21:27 Finished compiler/encoders/riscv/proofs                        9m34s   1GB
May 06 19:21:27 Starting compiler/encoders/ag32/proofs
May 06 19:24:18 Finished compiler/encoders/ag32/proofs                         2m50s 894MB
May 06 19:24:18 Starting compiler/backend/x64/proofs
May 06 19:24:41 Finished compiler/backend/x64/proofs                             22s   1GB
May 06 19:24:41 Starting compiler/backend/arm7/proofs
May 06 19:25:05 Finished compiler/backend/arm7/proofs                            24s   1GB
May 06 19:25:06 Starting compiler/backend/arm8/proofs
May 06 19:25:28 Finished compiler/backend/arm8/proofs                            22s   1GB
May 06 19:25:29 Starting compiler/backend/mips/proofs
May 06 19:25:51 Finished compiler/backend/mips/proofs                            22s   1GB
May 06 19:25:52 Starting compiler/backend/riscv/proofs
May 06 19:26:15 Finished compiler/backend/riscv/proofs                           23s   1GB
May 06 19:26:16 Starting compiler/backend/ag32/proofs
May 06 19:39:58 Finished compiler/backend/ag32/proofs                         13m42s   2GB
May 06 19:39:59 Starting compiler/proofs
May 06 19:41:59 Finished compiler/proofs                                       1m59s   5GB
May 06 19:41:59 Starting candle/set-theory
May 06 19:42:29 Finished candle/set-theory                                       29s 996MB
May 06 19:42:29 Starting candle/syntax-lib
May 06 19:42:40 Finished candle/syntax-lib                                       11s 444MB
May 06 19:42:40 Starting candle/standard/syntax
May 06 19:44:36 Finished candle/standard/syntax                                1m55s 875MB
May 06 19:44:36 Starting candle/standard/semantics
May 06 19:46:24 Finished candle/standard/semantics                             1m48s   1GB
May 06 19:46:25 Starting candle/standard/monadic
May 06 19:48:15 Finished candle/standard/monadic                               1m49s   1GB
May 06 19:48:15 Starting candle/standard/ml_kernel
May 06 19:54:26 Finished candle/standard/ml_kernel                             6m10s   5GB
May 06 19:54:26 Starting candle/overloading/syntax
May 06 19:57:48 Finished candle/overloading/syntax                             3m22s   1GB
May 06 19:57:48 Starting candle/overloading/semantics
May 06 20:10:47 Finished candle/overloading/semantics                         12m58s   3GB
May 06 20:10:48 Starting characteristic/examples
May 06 20:12:11 Finished characteristic/examples                               1m22s   2GB
May 06 20:12:11 Starting tutorial/solutions
May 06 20:28:28 Finished tutorial/solutions                                   16m16s   9GB
May 06 20:28:28 Starting translator/monadic/examples
May 06 20:31:52 Finished translator/monadic/examples                           3m24s   2GB
May 06 20:31:53 Starting examples
May 06 20:41:01 Finished examples                                              9m08s   4GB
May 06 20:41:01 Starting examples/compilation/x64
May 06 23:10:47 Finished examples/compilation/x64                           2h29m45s  17GB
May 06 23:10:47 Starting examples/compilation/x64/proofs
May 06 23:12:41 Finished examples/compilation/x64/proofs                       1m53s   2GB
May 06 23:12:41 Starting examples/compilation/ag32
May 06 23:48:00 Finished examples/compilation/ag32                            35m18s   7GB
May 06 23:48:01 Starting examples/compilation/ag32/proofs
May 06 23:48:49 Finished examples/compilation/ag32/proofs                        48s   3GB
May 06 23:48:50 Starting examples/cost
May 07 00:48:02 Finished examples/cost                                        59m12s   8GB
May 07 00:48:02 Starting examples/lpr_checker
May 07 00:52:11 Finished examples/lpr_checker                                  4m08s   3GB
May 07 00:52:11 Starting examples/lpr_checker/compilation
May 07 01:11:31 Finished examples/lpr_checker/compilation                     19m19s   9GB
May 07 01:11:31 Starting examples/lpr_checker/compilation/proofs
May 07 01:12:15 Finished examples/lpr_checker/compilation/proofs                 43s   3GB
May 07 01:12:15 Starting examples/lpr_checker/array
May 07 01:27:43 Finished examples/lpr_checker/array                           15m27s   3GB
May 07 01:27:43 Starting examples/lpr_checker/array/compilation
May 07 01:48:56 Finished examples/lpr_checker/array/compilation               21m12s  13GB
May 07 01:48:56 Starting examples/lpr_checker/array/compilation/proofs
May 07 01:50:10 Finished examples/lpr_checker/array/compilation/proofs         1m13s   3GB
May 07 01:50:10 Starting examples/opentheory
May 07 02:00:29 Finished examples/opentheory                                  10m18s   5GB
May 07 02:00:29 Starting examples/opentheory
May 07 02:00:30 Finished examples/opentheory                                      1s  17MB
May 07 02:00:30 Starting examples/opentheory/compilation
May 07 02:33:32 Finished examples/opentheory/compilation                      33m00s  20GB
May 07 02:33:32 Starting examples/opentheory/compilation/proofs
May 07 02:34:16 Finished examples/opentheory/compilation/proofs                  43s   4GB
May 07 02:34:16 Starting examples/opentheory/compilation/ag32
May 07 03:09:53 Finished examples/opentheory/compilation/ag32                 35m36s  17GB
May 07 03:09:53 Starting examples/opentheory/compilation/ag32/proofs
May 07 03:11:31 Finished examples/opentheory/compilation/ag32/proofs           1m38s   5GB
May 07 03:11:32 Starting translator/okasaki-examples
May 07 03:16:19 Finished translator/okasaki-examples                           4m47s   1GB
May 07 03:16:19 Starting translator/other-examples
May 07 03:18:30 Finished translator/other-examples                             2m10s   1GB
May 07 03:18:30 Starting compiler/parsing/tests
May 07 03:18:57 Finished compiler/parsing/tests                                  26s 591MB
May 07 03:18:58 Starting compiler/inference/tests
May 07 03:27:10 Finished compiler/inference/tests                              8m12s   4GB
May 07 03:27:10 Starting compiler/bootstrap/translation
May 07 06:12:01 Finished compiler/bootstrap/translation                     2h44m50s  25GB
May 07 06:12:01 Starting unverified/sexpr-bootstrap/x64/64
May 07 06:23:43 Finished unverified/sexpr-bootstrap/x64/64                    11m36s   9GB
May 07 06:23:43 Starting unverified/sexpr-bootstrap/x64/32
May 07 06:33:45 Finished unverified/sexpr-bootstrap/x64/32                     9m57s   8GB
May 07 06:33:46 Starting compiler/benchmarks
May 07 06:33:48 Finished compiler/benchmarks                                      1s  31MB
May 07 06:33:48 Starting compiler/bootstrap/compilation/x64/64
May 07 19:43:43 Finished compiler/bootstrap/compilation/x64/64             13h09m51s  64GB
May 07 19:43:44 Starting compiler/bootstrap/compilation/x64/64/proofs
May 07 19:46:51 Finished compiler/bootstrap/compilation/x64/64/proofs          3m07s  12GB
May 07 19:46:51 Starting compiler/bootstrap/compilation/x64/32
May 08 07:22:22 Finished compiler/bootstrap/compilation/x64/32             11h35m27s  64GB
May 08 07:22:22 Starting compiler/bootstrap/compilation/x64/32/proofs
May 08 07:25:20 Finished compiler/bootstrap/compilation/x64/32/proofs          2m57s  12GB
May 08 07:25:20 Starting compiler/bootstrap/compilation/ag32/32
May 08 19:46:20 Finished compiler/bootstrap/compilation/ag32/32            12h20m59s  64GB
May 08 19:46:20 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 08 20:04:28 Finished compiler/bootstrap/compilation/ag32/32/proofs        18m08s  20GB
May 08 20:04:29 SUCCESS