Job 1143

CakeML:6f499a68f2500e7f937b3254c9da6f93a9b62670
  Merge pull request #716 from CakeML/stack-opt-2 [Jan 09 03:33:21]
HOL:1f867f177143c9ba9b92ec32d874c1f2514b5322
  Optimise DefnBase.one_line_ify slightly in presence of many literals [Jan 11 05:29:17]
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

Jan 12 19:55:24 Claimed job
Jan 12 19:55:31 Building HOL
Jan 12 20:06:57 Starting developers
Jan 12 20:07:01 Finished developers                                               4s  95MB
Jan 12 20:07:01 Starting developers/bin
Jan 12 20:07:08 Finished developers/bin                                           6s 960MB
Jan 12 20:07:08 Starting semantics/ffi
Jan 12 20:07:18 Finished semantics/ffi                                            9s 204MB
Jan 12 20:07:18 Starting semantics
Jan 12 20:08:49 Finished semantics                                             1m30s   1GB
Jan 12 20:08:49 Starting semantics/proofs
Jan 12 20:12:09 Finished semantics/proofs                                      3m20s 936MB
Jan 12 20:12:09 Starting semantics/alt_semantics
Jan 12 20:12:17 Finished semantics/alt_semantics                                  7s 260MB
Jan 12 20:12:17 Starting semantics/alt_semantics/proofs
Jan 12 20:14:24 Finished semantics/alt_semantics/proofs                        2m06s 797MB
Jan 12 20:14:24 Starting basis/pure
Jan 12 20:17:25 Finished basis/pure                                            3m00s 715MB
Jan 12 20:17:25 Starting translator
Jan 12 20:20:01 Finished translator                                            2m36s   1GB
Jan 12 20:20:01 Starting compiler/parsing
Jan 12 20:21:13 Finished compiler/parsing                                      1m11s   2GB
Jan 12 20:21:13 Starting characteristic
Jan 12 20:27:00 Finished characteristic                                        5m47s   1GB
Jan 12 20:27:00 Starting translator/monadic
Jan 12 20:28:35 Finished translator/monadic                                    1m34s   1GB
Jan 12 20:28:35 Starting basis
Jan 12 21:03:22 Finished basis                                                34m47s  12GB
Jan 12 21:03:23 Starting compiler/inference
Jan 12 21:05:20 Finished compiler/inference                                    1m57s   1GB
Jan 12 21:05:20 Starting compiler/backend/reg_alloc
Jan 12 21:06:23 Finished compiler/backend/reg_alloc                            1m02s   1GB
Jan 12 21:06:23 Starting compiler/backend/gc
Jan 12 21:09:51 Finished compiler/backend/gc                                   3m28s   2GB
Jan 12 21:09:52 Starting compiler/backend
Jan 12 21:14:20 Finished compiler/backend                                      4m28s   3GB
Jan 12 21:14:20 Starting compiler/encoders/asm
Jan 12 21:14:41 Finished compiler/encoders/asm                                   21s 842MB
Jan 12 21:14:42 Starting compiler/encoders/x64
Jan 12 21:15:39 Finished compiler/encoders/x64                                   57s 948MB
Jan 12 21:15:39 Starting compiler/encoders/arm7
Jan 12 21:17:28 Finished compiler/encoders/arm7                                1m48s   1GB
Jan 12 21:17:28 Starting compiler/encoders/arm8
Jan 12 21:18:01 Finished compiler/encoders/arm8                                  32s 555MB
Jan 12 21:18:02 Starting compiler/encoders/mips
Jan 12 21:19:15 Finished compiler/encoders/mips                                1m12s 947MB
Jan 12 21:19:15 Starting compiler/encoders/riscv
Jan 12 21:20:42 Finished compiler/encoders/riscv                               1m26s 797MB
Jan 12 21:20:42 Starting compiler/encoders/ag32
Jan 12 21:20:59 Finished compiler/encoders/ag32                                  17s 774MB
Jan 12 21:20:59 Starting compiler/backend/x64
Jan 12 21:21:17 Finished compiler/backend/x64                                    16s 895MB
Jan 12 21:21:17 Starting compiler/backend/arm7
Jan 12 21:21:37 Finished compiler/backend/arm7                                   19s   1GB
Jan 12 21:21:37 Starting compiler/backend/arm8
Jan 12 21:21:55 Finished compiler/backend/arm8                                   18s   1GB
Jan 12 21:21:56 Starting compiler/backend/mips
Jan 12 21:22:14 Finished compiler/backend/mips                                   18s   1GB
Jan 12 21:22:14 Starting compiler/backend/riscv
Jan 12 21:22:33 Finished compiler/backend/riscv                                  18s   1GB
Jan 12 21:22:33 Starting compiler/backend/ag32
Jan 12 21:23:44 Finished compiler/backend/ag32                                 1m11s   1GB
Jan 12 21:23:44 Starting compiler/parsing/proofs
Jan 12 21:29:38 Finished compiler/parsing/proofs                               5m53s   1GB
Jan 12 21:29:38 Starting compiler/inference/proofs
Jan 12 21:32:39 Finished compiler/inference/proofs                             3m00s   1GB
Jan 12 21:32:39 Starting compiler/backend/semantics
Jan 12 22:02:43 Finished compiler/backend/semantics                           30m04s   2GB
Jan 12 22:02:43 Starting compiler/backend/reg_alloc/proofs
Jan 12 22:06:22 Finished compiler/backend/reg_alloc/proofs                     3m38s   1GB
Jan 12 22:06:22 Starting compiler/backend/proofs
Jan 12 23:13:04 Finished compiler/backend/proofs                            1h06m41s  14GB
Jan 12 23:13:04 Starting compiler/encoders/x64/proofs
Jan 12 23:22:53 Finished compiler/encoders/x64/proofs                          9m48s   4GB
Jan 12 23:22:53 Starting compiler/encoders/arm7/proofs
Jan 12 23:36:06 Finished compiler/encoders/arm7/proofs                        13m12s   3GB
Jan 12 23:36:06 Starting compiler/encoders/arm8/proofs
Jan 12 23:42:46 Finished compiler/encoders/arm8/proofs                         6m40s   1GB
Jan 12 23:42:46 Starting compiler/encoders/mips/proofs
Jan 12 23:52:55 Finished compiler/encoders/mips/proofs                        10m08s   2GB
Jan 12 23:52:55 Starting compiler/encoders/riscv/proofs
Jan 13 00:01:57 Finished compiler/encoders/riscv/proofs                        9m01s   1GB
Jan 13 00:01:57 Starting compiler/encoders/ag32/proofs
Jan 13 00:04:38 Finished compiler/encoders/ag32/proofs                         2m40s 676MB
Jan 13 00:04:38 Starting compiler/backend/x64/proofs
Jan 13 00:04:56 Finished compiler/backend/x64/proofs                             18s 807MB
Jan 13 00:04:56 Starting compiler/backend/arm7/proofs
Jan 13 00:05:20 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 13 00:05:21 Starting compiler/backend/arm8/proofs
Jan 13 00:05:38 Finished compiler/backend/arm8/proofs                            17s 829MB
Jan 13 00:05:38 Starting compiler/backend/mips/proofs
Jan 13 00:05:57 Finished compiler/backend/mips/proofs                            18s 931MB
Jan 13 00:05:57 Starting compiler/backend/riscv/proofs
Jan 13 00:06:17 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 13 00:06:17 Starting compiler/backend/ag32/proofs
Jan 13 00:16:00 Finished compiler/backend/ag32/proofs                          9m42s   2GB
Jan 13 00:16:00 Starting compiler/proofs
Jan 13 00:18:11 Finished compiler/proofs                                       2m10s   3GB
Jan 13 00:18:11 Starting candle/set-theory
Jan 13 00:18:39 Finished candle/set-theory                                       27s 672MB
Jan 13 00:18:39 Starting candle/syntax-lib
Jan 13 00:18:50 Finished candle/syntax-lib                                       10s 584MB
Jan 13 00:18:50 Starting candle/standard/syntax
Jan 13 00:20:40 Finished candle/standard/syntax                                1m50s 976MB
Jan 13 00:20:40 Starting candle/standard/semantics
Jan 13 00:22:22 Finished candle/standard/semantics                             1m41s   1GB
Jan 13 00:22:22 Starting candle/standard/monadic
Jan 13 00:24:03 Finished candle/standard/monadic                               1m40s   1GB
Jan 13 00:24:04 Starting candle/standard/ml_kernel
Jan 13 00:29:34 Finished candle/standard/ml_kernel                             5m30s   4GB
Jan 13 00:29:34 Starting candle/standard/opentheory
Jan 13 00:39:28 Finished candle/standard/opentheory                            9m53s   4GB
Jan 13 00:39:28 Starting candle/standard/opentheory/compilation
Jan 13 01:12:26 Finished candle/standard/opentheory/compilation               32m58s  17GB
Jan 13 01:12:27 Starting candle/standard/opentheory/compilation/proofs
Jan 13 01:13:18 Finished candle/standard/opentheory/compilation/proofs           51s   2GB
Jan 13 01:13:18 Starting characteristic/examples
Jan 13 01:14:49 Finished characteristic/examples                               1m31s   2GB
Jan 13 01:14:49 Starting tutorial/solutions
Jan 13 01:29:28 Finished tutorial/solutions                                   14m37s   7GB
Jan 13 01:29:28 Starting translator/monadic/examples
Jan 13 01:32:31 Finished translator/monadic/examples                           3m02s   2GB
Jan 13 01:32:31 Starting examples
Jan 13 01:42:08 Finished examples                                              9m36s   3GB
Jan 13 01:42:08 Starting examples/compilation/x64
Jan 13 04:00:54 Finished examples/compilation/x64                           2h18m45s  12GB
Jan 13 04:00:54 Starting examples/compilation/x64/proofs
Jan 13 04:03:26 Finished examples/compilation/x64/proofs                       2m32s   2GB
Jan 13 04:03:27 Starting examples/compilation/ag32
Jan 13 04:34:58 Finished examples/compilation/ag32                            31m30s   5GB
Jan 13 04:34:58 Starting examples/compilation/ag32/proofs
Jan 13 04:35:49 Finished examples/compilation/ag32/proofs                        50s   4GB
Jan 13 04:35:49 Starting examples/cost
Jan 13 05:05:13 Finished examples/cost                                        29m23s   6GB
Jan 13 05:05:13 Starting examples/lrat_checker
Jan 13 05:08:48 Finished examples/lrat_checker                                 3m34s   2GB
Jan 13 05:08:48 Starting examples/lrat_checker/compilation
Jan 13 05:25:35 Finished examples/lrat_checker/compilation                    16m46s   8GB
Jan 13 05:25:35 Starting examples/lrat_checker/compilation/proofs
Jan 13 05:26:13 Finished examples/lrat_checker/compilation/proofs                37s   3GB
Jan 13 05:26:13 Starting examples/lrat_checker/array
Jan 13 05:32:50 Finished examples/lrat_checker/array                           6m37s   4GB
Jan 13 05:32:51 Starting examples/lrat_checker/array/compilation
Jan 13 05:47:59 Finished examples/lrat_checker/array/compilation              15m08s   8GB
Jan 13 05:47:59 Starting examples/lrat_checker/array/compilation/proofs
Jan 13 05:48:59 Finished examples/lrat_checker/array/compilation/proofs          59s   2GB
Jan 13 05:48:59 Starting translator/okasaki-examples
Jan 13 05:53:18 Finished translator/okasaki-examples                           4m18s   1GB
Jan 13 05:53:18 Starting translator/other-examples
Jan 13 05:55:18 Finished translator/other-examples                             1m59s   1GB
Jan 13 05:55:18 Starting compiler/parsing/tests
Jan 13 05:55:44 Finished compiler/parsing/tests                                  26s 436MB
Jan 13 05:55:44 Starting compiler/inference/tests
Jan 13 06:00:18 Finished compiler/inference/tests                              4m33s   3GB
Jan 13 06:00:18 Starting compiler/bootstrap/translation
Jan 13 09:43:19 Finished compiler/bootstrap/translation                     3h42m58s  42GB
Jan 13 09:43:20 Starting unverified/sexpr-bootstrap/x64/64
Jan 13 09:57:17 Finished unverified/sexpr-bootstrap/x64/64                    13m56s   3GB
Jan 13 09:57:17 Starting unverified/sexpr-bootstrap/x64/32
Jan 13 10:07:21 Finished unverified/sexpr-bootstrap/x64/32                    10m03s   6GB
Jan 13 10:07:21 Starting compiler/benchmarks
Jan 13 10:07:23 Finished compiler/benchmarks                                      2s  23MB
Jan 13 10:07:23 Starting compiler/bootstrap/compilation/x64/64
Jan 14 01:02:47 Finished compiler/bootstrap/compilation/x64/64             14h55m22s  64GB
Jan 14 01:02:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 14 01:06:55 Finished compiler/bootstrap/compilation/x64/64/proofs          4m07s   5GB
Jan 14 01:06:55 Starting compiler/bootstrap/compilation/x64/32
Jan 14 13:56:45 Finished compiler/bootstrap/compilation/x64/32             12h49m48s  64GB
Jan 14 13:56:45 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 14 14:01:16 Finished compiler/bootstrap/compilation/x64/32/proofs          4m31s   8GB
Jan 14 14:01:16 Starting compiler/bootstrap/compilation/ag32/32
Jan 15 04:02:37 Finished compiler/bootstrap/compilation/ag32/32            14h01m19s  64GB
Jan 15 04:02:37 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 15 04:31:15 Finished compiler/bootstrap/compilation/ag32/32/proofs        28m37s  18GB
Jan 15 04:31:15 SUCCESS