Job 1704

CakeML:47e09d2cf7caeaf496701b78f5aff5b4cdf98091
  Make a file easier to read [Dec 22 12:31:56]
#852 (tidy-up)
Merging into:d8dc70502a73effe17411f0d7eeaa80c1d9fab98
  Merge pull request #851 from CakeML/candle-prover [Jan 02 20:24:41]
HOL:288eed203f9e91e52a1707519ea31e41041b2f48
  Move more examples into parallel build process [Dec 23 06:36:48]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 03 20:03:59 Claimed job
Jan 03 20:04:02 Reusing HOL
Jan 03 20:04:42 Starting developers
Jan 03 20:04:47 Finished developers                                               4s 103MB
Jan 03 20:04:47 Starting developers/bin
Jan 03 20:04:53 Finished developers/bin                                           5s 670MB
Jan 03 20:04:53 Starting semantics/ffi
Jan 03 20:05:02 Finished semantics/ffi                                            8s 223MB
Jan 03 20:05:02 Starting semantics
Jan 03 20:06:30 Finished semantics                                             1m27s   1GB
Jan 03 20:06:30 Starting semantics/proofs
Jan 03 20:10:18 Finished semantics/proofs                                      3m48s   1GB
Jan 03 20:10:18 Starting semantics/alt_semantics
Jan 03 20:10:30 Finished semantics/alt_semantics                                 11s 341MB
Jan 03 20:10:30 Starting semantics/alt_semantics/proofs
Jan 03 20:13:05 Finished semantics/alt_semantics/proofs                        2m34s 872MB
Jan 03 20:13:06 Starting basis/pure
Jan 03 20:13:59 Finished basis/pure                                              52s 735MB
Jan 03 20:13:59 Starting translator
Jan 03 20:16:56 Finished translator                                            2m56s   1GB
Jan 03 20:16:56 Starting compiler/parsing
Jan 03 20:18:15 Finished compiler/parsing                                      1m19s   3GB
Jan 03 20:18:16 Starting characteristic
Jan 03 20:24:10 Finished characteristic                                        5m53s   2GB
Jan 03 20:24:10 Starting translator/monadic
Jan 03 20:25:52 Finished translator/monadic                                    1m42s   1GB
Jan 03 20:25:53 Starting basis
Jan 03 21:14:29 Finished basis                                                48m35s  10GB
Jan 03 21:14:29 Starting compiler/inference
Jan 03 21:15:38 Finished compiler/inference                                    1m09s   1GB
Jan 03 21:15:39 Starting compiler/backend/reg_alloc
Jan 03 21:16:47 Finished compiler/backend/reg_alloc                            1m08s   1GB
Jan 03 21:16:47 Starting compiler/backend/gc
Jan 03 21:20:20 Finished compiler/backend/gc                                   3m32s   2GB
Jan 03 21:20:21 Starting compiler/backend
Jan 03 21:25:10 Finished compiler/backend                                      4m48s   1GB
Jan 03 21:25:10 Starting compiler/encoders/asm
Jan 03 21:25:33 Finished compiler/encoders/asm                                   23s 630MB
Jan 03 21:25:34 Starting compiler/encoders/x64
Jan 03 21:26:01 Finished compiler/encoders/x64                                   27s 994MB
Jan 03 21:26:01 Starting compiler/encoders/arm7
Jan 03 21:26:55 Finished compiler/encoders/arm7                                  54s 756MB
Jan 03 21:26:56 Starting compiler/encoders/arm8
Jan 03 21:27:10 Finished compiler/encoders/arm8                                  13s 907MB
Jan 03 21:27:10 Starting compiler/encoders/mips
Jan 03 21:27:28 Finished compiler/encoders/mips                                  18s   1GB
Jan 03 21:27:28 Starting compiler/encoders/riscv
Jan 03 21:27:46 Finished compiler/encoders/riscv                                 17s 980MB
Jan 03 21:27:46 Starting compiler/encoders/ag32
Jan 03 21:28:05 Finished compiler/encoders/ag32                                  18s 766MB
Jan 03 21:28:05 Starting compiler/backend/x64
Jan 03 21:28:26 Finished compiler/backend/x64                                    20s   1GB
Jan 03 21:28:26 Starting compiler/backend/arm7
Jan 03 21:28:48 Finished compiler/backend/arm7                                   21s   1GB
Jan 03 21:28:48 Starting compiler/backend/arm8
Jan 03 21:29:09 Finished compiler/backend/arm8                                   20s   1GB
Jan 03 21:29:09 Starting compiler/backend/mips
Jan 03 21:29:30 Finished compiler/backend/mips                                   21s   1GB
Jan 03 21:29:31 Starting compiler/backend/riscv
Jan 03 21:29:52 Finished compiler/backend/riscv                                  21s   1GB
Jan 03 21:29:52 Starting compiler/backend/ag32
Jan 03 21:31:05 Finished compiler/backend/ag32                                 1m12s   1GB
Jan 03 21:31:05 Starting compiler/parsing/proofs
Jan 03 21:35:06 Finished compiler/parsing/proofs                               4m00s   1GB
Jan 03 21:35:06 Starting compiler/inference/proofs
Jan 03 21:37:39 Finished compiler/inference/proofs                             2m33s 980MB
Jan 03 21:37:40 Starting compiler/backend/semantics
Jan 03 22:10:36 Finished compiler/backend/semantics                           32m56s   2GB
Jan 03 22:10:36 Starting compiler/backend/reg_alloc/proofs
Jan 03 22:14:23 Finished compiler/backend/reg_alloc/proofs                     3m46s 834MB
Jan 03 22:14:23 Starting compiler/backend/proofs
Jan 03 23:12:22 Finished compiler/backend/proofs                              57m56s  14GB
Jan 03 23:12:22 Starting compiler/backend/serialiser
Jan 03 23:13:37 Finished compiler/backend/serialiser                           1m14s   1GB
Jan 03 23:13:37 Starting compiler/encoders/x64/proofs
Jan 03 23:23:55 Finished compiler/encoders/x64/proofs                         10m17s   5GB
Jan 03 23:23:55 Starting compiler/encoders/arm7/proofs
Jan 03 23:37:58 Finished compiler/encoders/arm7/proofs                        14m02s   7GB
Jan 03 23:37:58 Starting compiler/encoders/arm8/proofs
Jan 03 23:45:16 Finished compiler/encoders/arm8/proofs                         7m18s   1GB
Jan 03 23:45:17 Starting compiler/encoders/mips/proofs
Jan 03 23:56:05 Finished compiler/encoders/mips/proofs                        10m48s   3GB
Jan 03 23:56:05 Starting compiler/encoders/riscv/proofs
Jan 04 00:05:30 Finished compiler/encoders/riscv/proofs                        9m24s   1GB
Jan 04 00:05:30 Starting compiler/encoders/ag32/proofs
Jan 04 00:08:19 Finished compiler/encoders/ag32/proofs                         2m48s 682MB
Jan 04 00:08:19 Starting compiler/backend/x64/proofs
Jan 04 00:08:43 Finished compiler/backend/x64/proofs                             24s   1GB
Jan 04 00:08:44 Starting compiler/backend/arm7/proofs
Jan 04 00:09:07 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 04 00:09:07 Starting compiler/backend/arm8/proofs
Jan 04 00:09:32 Finished compiler/backend/arm8/proofs                            24s   1GB
Jan 04 00:09:32 Starting compiler/backend/mips/proofs
Jan 04 00:09:57 Finished compiler/backend/mips/proofs                            25s   1GB
Jan 04 00:09:58 Starting compiler/backend/riscv/proofs
Jan 04 00:10:22 Finished compiler/backend/riscv/proofs                           23s   1GB
Jan 04 00:10:22 Starting compiler/backend/ag32/proofs
Jan 04 00:23:56 Finished compiler/backend/ag32/proofs                         13m33s   2GB
Jan 04 00:23:56 Starting compiler/proofs
Jan 04 00:25:41 Finished compiler/proofs                                       1m44s   3GB
Jan 04 00:25:41 Starting candle/set-theory
Jan 04 00:26:10 Finished candle/set-theory                                       28s 863MB
Jan 04 00:26:10 Starting candle/syntax-lib
Jan 04 00:26:22 Finished candle/syntax-lib                                       11s 484MB
Jan 04 00:26:22 Starting candle/standard/syntax
Jan 04 00:28:13 Finished candle/standard/syntax                                1m50s 922MB
Jan 04 00:28:13 Starting candle/standard/semantics
Jan 04 00:30:00 Finished candle/standard/semantics                             1m46s   1GB
Jan 04 00:30:00 Starting candle/standard/monadic
Jan 04 00:31:39 Finished candle/standard/monadic                               1m39s   1GB
Jan 04 00:31:39 Starting candle/standard/ml_kernel
Jan 04 00:38:47 Finished candle/standard/ml_kernel                             7m07s   3GB
Jan 04 00:38:47 Starting candle/overloading/syntax
Jan 04 00:41:59 Finished candle/overloading/syntax                             3m11s   1GB
Jan 04 00:41:59 Starting candle/overloading/semantics
Jan 04 00:54:20 Finished candle/overloading/semantics                         12m20s   2GB
Jan 04 00:54:20 Starting candle/prover
Jan 04 01:01:54 Finished candle/prover                                         7m33s   2GB
Jan 04 01:01:54 Starting pancake
Jan 04 01:03:54 Finished pancake                                               1m59s   2GB
Jan 04 01:03:54 Starting pancake/ffi
Jan 04 01:03:55 Finished pancake/ffi                                              0s   4MB
Jan 04 01:03:55 Starting pancake/semantics
Jan 04 01:06:27 Finished pancake/semantics                                     2m31s 972MB
Jan 04 01:06:27 Starting pancake/proofs
Jan 04 01:19:24 Finished pancake/proofs                                       12m56s   6GB
Jan 04 01:19:24 Starting characteristic/examples
Jan 04 01:20:50 Finished characteristic/examples                               1m25s   3GB
Jan 04 01:20:50 Starting tutorial/solutions
Jan 04 01:37:26 Finished tutorial/solutions                                   16m35s  10GB
Jan 04 01:37:26 Starting translator/monadic/examples
Jan 04 01:40:51 Finished translator/monadic/examples                           3m24s   3GB
Jan 04 01:40:51 Starting examples
Jan 04 01:50:54 Finished examples                                             10m02s   3GB
Jan 04 01:50:54 Starting examples/compilation/x64
Jan 04 04:24:22 Finished examples/compilation/x64                           2h33m26s  17GB
Jan 04 04:24:22 Starting examples/compilation/x64/proofs
Jan 04 04:26:28 Finished examples/compilation/x64/proofs                       2m05s   2GB
Jan 04 04:26:28 Starting examples/compilation/ag32
Jan 04 05:01:54 Finished examples/compilation/ag32                            35m25s   8GB
Jan 04 05:01:54 Starting examples/compilation/ag32/proofs
Jan 04 05:02:43 Finished examples/compilation/ag32/proofs                        48s   4GB
Jan 04 05:02:43 Starting examples/cost
Jan 04 06:03:00 Finished examples/cost                                      1h00m16s   8GB
Jan 04 06:03:00 Starting examples/lpr_checker
Jan 04 06:03:49 Finished examples/lpr_checker                                    48s   1GB
Jan 04 06:03:50 Starting examples/lpr_checker/array
Jan 04 06:34:54 Finished examples/lpr_checker/array                           31m03s   5GB
Jan 04 06:34:54 Starting examples/lpr_checker/array/compilation
Jan 04 08:04:00 Finished examples/lpr_checker/array/compilation             1h29m05s  33GB
Jan 04 08:04:00 Starting examples/lpr_checker/array/compilation/proofs
Jan 04 08:05:18 Finished examples/lpr_checker/array/compilation/proofs         1m17s   7GB
Jan 04 08:05:18 Starting examples/opentheory
Jan 04 08:15:33 Finished examples/opentheory                                  10m15s   5GB
Jan 04 08:15:34 Starting examples/opentheory
Jan 04 08:15:35 Finished examples/opentheory                                      1s  20MB
Jan 04 08:15:35 Starting examples/opentheory/compilation
Jan 04 08:57:57 Finished examples/opentheory/compilation                      42m21s  29GB
Jan 04 08:57:57 Starting examples/opentheory/compilation/proofs
Jan 04 08:58:51 Finished examples/opentheory/compilation/proofs                  53s   2GB
Jan 04 08:58:51 Starting examples/opentheory/compilation/ag32
Jan 04 09:39:54 Finished examples/opentheory/compilation/ag32                 41m01s  26GB
Jan 04 09:39:54 Starting examples/opentheory/compilation/ag32/proofs
Jan 04 09:41:36 Finished examples/opentheory/compilation/ag32/proofs           1m41s   6GB
Jan 04 09:41:36 Starting examples/sat_encodings
Jan 04 09:43:25 Finished examples/sat_encodings                                1m48s 772MB
Jan 04 09:43:25 Starting examples/sat_encodings/case_studies
Jan 04 09:45:08 Finished examples/sat_encodings/case_studies                   1m42s 706MB
Jan 04 09:45:08 Starting examples/sat_encodings/translation
Jan 04 09:51:03 Finished examples/sat_encodings/translation                    5m54s   3GB
Jan 04 09:51:03 Starting examples/sat_encodings/translation/compilation
Jan 04 10:46:02 Finished examples/sat_encodings/translation/compilation       54m55s  20GB
Jan 04 10:46:02 Starting translator/okasaki-examples
Jan 04 10:50:51 Finished translator/okasaki-examples                           4m48s   1GB
Jan 04 10:50:51 Starting translator/other-examples
Jan 04 10:51:38 Finished translator/other-examples                               46s   1GB
Jan 04 10:51:38 Starting compiler/parsing/tests
Jan 04 10:52:08 Finished compiler/parsing/tests                                  29s 589MB
Jan 04 10:52:08 Starting compiler/inference/tests
Jan 04 11:00:27 Finished compiler/inference/tests                              8m18s   5GB
Jan 04 11:00:27 Starting compiler/bootstrap/translation
Jan 04 13:48:55 Finished compiler/bootstrap/translation                     2h48m26s  25GB
Jan 04 13:48:55 Starting unverified/sexpr-bootstrap/x64/64
Jan 04 13:58:17 Finished unverified/sexpr-bootstrap/x64/64                     9m21s   8GB
Jan 04 13:58:17 Starting unverified/sexpr-bootstrap/x64/32
Jan 04 14:06:13 Finished unverified/sexpr-bootstrap/x64/32                     7m54s   8GB
Jan 04 14:06:13 Starting compiler/benchmarks
Jan 04 14:06:15 Finished compiler/benchmarks                                      2s  38MB
Jan 04 14:06:15 Starting compiler/bootstrap/compilation/x64/64
Jan 05 03:43:39 Finished compiler/bootstrap/compilation/x64/64             13h37m21s  64GB
Jan 05 03:43:39 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 05 03:45:57 Finished compiler/bootstrap/compilation/x64/64/proofs          2m18s  15GB
Jan 05 03:45:58 Starting compiler/bootstrap/compilation/x64/32
Jan 05 15:25:09 Finished compiler/bootstrap/compilation/x64/32             11h39m10s  64GB
Jan 05 15:25:10 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 05 15:28:11 Finished compiler/bootstrap/compilation/x64/32/proofs          3m00s  12GB
Jan 05 15:28:11 Starting compiler/bootstrap/compilation/ag32/32
Jan 06 03:16:22 Finished compiler/bootstrap/compilation/ag32/32            11h48m10s  64GB
Jan 06 03:16:22 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 06 03:35:03 Finished compiler/bootstrap/compilation/ag32/32/proofs        18m40s  18GB
Jan 06 03:35:03 SUCCESS