Job 1701

CakeML:ebe612a7217789284dbbf9c10ed0db69bcc8e740
  Add candle/prover to build-sequence [Dec 31 09:32:45]
#851 (candle-prover)
Merging into:2c2b4c83b857a26ba3318c77300e798965c5dfed
  Refix parsing/fromSexp given unlisting of theorems in quantHeuristics [Dec 22 06:37:04]
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

Dec 31 09:49:03 Claimed job
Dec 31 09:49:11 Building HOL
Dec 31 09:59:12 Starting developers
Dec 31 09:59:16 Finished developers                                               4s 101MB
Dec 31 09:59:17 Starting developers/bin
Dec 31 09:59:22 Finished developers/bin                                           5s 670MB
Dec 31 09:59:22 Starting semantics/ffi
Dec 31 09:59:31 Finished semantics/ffi                                            8s 204MB
Dec 31 09:59:31 Starting semantics
Dec 31 10:01:08 Finished semantics                                             1m36s   1GB
Dec 31 10:01:08 Starting semantics/proofs
Dec 31 10:04:54 Finished semantics/proofs                                      3m44s   1GB
Dec 31 10:04:54 Starting semantics/alt_semantics
Dec 31 10:05:05 Finished semantics/alt_semantics                                 11s 377MB
Dec 31 10:05:06 Starting semantics/alt_semantics/proofs
Dec 31 10:07:41 Finished semantics/alt_semantics/proofs                        2m34s   1GB
Dec 31 10:07:41 Starting basis/pure
Dec 31 10:10:37 Finished basis/pure                                            2m55s 760MB
Dec 31 10:10:37 Starting translator
Dec 31 10:13:33 Finished translator                                            2m55s   1GB
Dec 31 10:13:33 Starting compiler/parsing
Dec 31 10:14:53 Finished compiler/parsing                                      1m19s   2GB
Dec 31 10:14:53 Starting characteristic
Dec 31 10:20:50 Finished characteristic                                        5m56s   1GB
Dec 31 10:20:50 Starting translator/monadic
Dec 31 10:22:34 Finished translator/monadic                                    1m43s   1GB
Dec 31 10:22:34 Starting basis
Dec 31 11:10:57 Finished basis                                                48m22s  10GB
Dec 31 11:10:57 Starting compiler/inference
Dec 31 11:12:15 Finished compiler/inference                                    1m17s   1GB
Dec 31 11:12:16 Starting compiler/backend/reg_alloc
Dec 31 11:13:24 Finished compiler/backend/reg_alloc                            1m07s   1GB
Dec 31 11:13:24 Starting compiler/backend/gc
Dec 31 11:17:08 Finished compiler/backend/gc                                   3m43s   2GB
Dec 31 11:17:08 Starting compiler/backend
Dec 31 11:21:57 Finished compiler/backend                                      4m48s   2GB
Dec 31 11:21:57 Starting compiler/encoders/asm
Dec 31 11:22:21 Finished compiler/encoders/asm                                   23s 694MB
Dec 31 11:22:21 Starting compiler/encoders/x64
Dec 31 11:23:25 Finished compiler/encoders/x64                                 1m04s   1GB
Dec 31 11:23:25 Starting compiler/encoders/arm7
Dec 31 11:25:35 Finished compiler/encoders/arm7                                2m09s   1GB
Dec 31 11:25:35 Starting compiler/encoders/arm8
Dec 31 11:26:15 Finished compiler/encoders/arm8                                  39s 907MB
Dec 31 11:26:15 Starting compiler/encoders/mips
Dec 31 11:27:51 Finished compiler/encoders/mips                                1m35s   1GB
Dec 31 11:27:51 Starting compiler/encoders/riscv
Dec 31 11:29:43 Finished compiler/encoders/riscv                               1m51s   1GB
Dec 31 11:29:43 Starting compiler/encoders/ag32
Dec 31 11:30:01 Finished compiler/encoders/ag32                                  18s 766MB
Dec 31 11:30:02 Starting compiler/backend/x64
Dec 31 11:30:22 Finished compiler/backend/x64                                    20s   1GB
Dec 31 11:30:23 Starting compiler/backend/arm7
Dec 31 11:30:44 Finished compiler/backend/arm7                                   21s   1GB
Dec 31 11:30:45 Starting compiler/backend/arm8
Dec 31 11:31:06 Finished compiler/backend/arm8                                   20s   1GB
Dec 31 11:31:06 Starting compiler/backend/mips
Dec 31 11:31:27 Finished compiler/backend/mips                                   20s   1GB
Dec 31 11:31:27 Starting compiler/backend/riscv
Dec 31 11:31:48 Finished compiler/backend/riscv                                  20s   1GB
Dec 31 11:31:48 Starting compiler/backend/ag32
Dec 31 11:33:01 Finished compiler/backend/ag32                                 1m12s   1GB
Dec 31 11:33:01 Starting compiler/parsing/proofs
Dec 31 11:37:04 Finished compiler/parsing/proofs                               4m02s   1GB
Dec 31 11:37:04 Starting compiler/inference/proofs
Dec 31 11:39:35 Finished compiler/inference/proofs                             2m31s 956MB
Dec 31 11:39:36 Starting compiler/backend/semantics
Dec 31 12:12:43 Finished compiler/backend/semantics                           33m06s   2GB
Dec 31 12:12:43 Starting compiler/backend/reg_alloc/proofs
Dec 31 12:16:29 Finished compiler/backend/reg_alloc/proofs                     3m46s 844MB
Dec 31 12:16:30 Starting compiler/backend/proofs
Dec 31 13:14:18 Finished compiler/backend/proofs                              57m47s  15GB
Dec 31 13:14:18 Starting compiler/backend/serialiser
Dec 31 13:15:32 Finished compiler/backend/serialiser                           1m13s   1GB
Dec 31 13:15:32 Starting compiler/encoders/x64/proofs
Dec 31 13:25:55 Finished compiler/encoders/x64/proofs                         10m22s   4GB
Dec 31 13:25:55 Starting compiler/encoders/arm7/proofs
Dec 31 13:40:00 Finished compiler/encoders/arm7/proofs                        14m04s   3GB
Dec 31 13:40:00 Starting compiler/encoders/arm8/proofs
Dec 31 13:47:12 Finished compiler/encoders/arm8/proofs                         7m11s   1GB
Dec 31 13:47:12 Starting compiler/encoders/mips/proofs
Dec 31 13:58:01 Finished compiler/encoders/mips/proofs                        10m48s   2GB
Dec 31 13:58:01 Starting compiler/encoders/riscv/proofs
Dec 31 14:07:28 Finished compiler/encoders/riscv/proofs                        9m26s   1GB
Dec 31 14:07:28 Starting compiler/encoders/ag32/proofs
Dec 31 14:10:17 Finished compiler/encoders/ag32/proofs                         2m48s 692MB
Dec 31 14:10:17 Starting compiler/backend/x64/proofs
Dec 31 14:10:41 Finished compiler/backend/x64/proofs                             23s   1GB
Dec 31 14:10:42 Starting compiler/backend/arm7/proofs
Dec 31 14:11:06 Finished compiler/backend/arm7/proofs                            24s   1GB
Dec 31 14:11:06 Starting compiler/backend/arm8/proofs
Dec 31 14:11:31 Finished compiler/backend/arm8/proofs                            24s   1GB
Dec 31 14:11:31 Starting compiler/backend/mips/proofs
Dec 31 14:11:55 Finished compiler/backend/mips/proofs                            23s   1GB
Dec 31 14:11:55 Starting compiler/backend/riscv/proofs
Dec 31 14:12:19 Finished compiler/backend/riscv/proofs                           23s   1GB
Dec 31 14:12:19 Starting compiler/backend/ag32/proofs
Dec 31 14:25:36 Finished compiler/backend/ag32/proofs                         13m16s   2GB
Dec 31 14:25:36 Starting compiler/proofs
Dec 31 14:27:40 Finished compiler/proofs                                       2m04s   3GB
Dec 31 14:27:40 Starting candle/set-theory
Dec 31 14:28:10 Finished candle/set-theory                                       29s 719MB
Dec 31 14:28:10 Starting candle/syntax-lib
Dec 31 14:28:22 Finished candle/syntax-lib                                       11s 484MB
Dec 31 14:28:22 Starting candle/standard/syntax
Dec 31 14:30:14 Finished candle/standard/syntax                                1m51s 903MB
Dec 31 14:30:14 Starting candle/standard/semantics
Dec 31 14:31:59 Finished candle/standard/semantics                             1m45s   1GB
Dec 31 14:32:00 Starting candle/standard/monadic
Dec 31 14:33:38 Finished candle/standard/monadic                               1m38s   1GB
Dec 31 14:33:39 Starting candle/standard/ml_kernel
Dec 31 14:40:45 Finished candle/standard/ml_kernel                             7m06s   3GB
Dec 31 14:40:45 Starting candle/overloading/syntax
Dec 31 14:43:59 Finished candle/overloading/syntax                             3m13s   1GB
Dec 31 14:43:59 Starting candle/overloading/semantics
Dec 31 14:56:31 Finished candle/overloading/semantics                         12m31s   2GB
Dec 31 14:56:31 Starting candle/prover
Dec 31 15:04:09 Finished candle/prover                                         7m37s   3GB
Dec 31 15:04:09 Starting pancake
Dec 31 15:06:05 Finished pancake                                               1m55s   2GB
Dec 31 15:06:06 Starting pancake/ffi
Dec 31 15:06:06 Finished pancake/ffi                                              0s   5MB
Dec 31 15:06:06 Starting pancake/semantics
Dec 31 15:08:33 Finished pancake/semantics                                     2m26s   1GB
Dec 31 15:08:33 Starting pancake/proofs
Dec 31 15:21:18 Finished pancake/proofs                                       12m44s   5GB
Dec 31 15:21:18 Starting characteristic/examples
Dec 31 15:22:44 Finished characteristic/examples                               1m26s   2GB
Dec 31 15:22:44 Starting tutorial/solutions
Dec 31 15:39:24 Finished tutorial/solutions                                   16m39s   9GB
Dec 31 15:39:24 Starting translator/monadic/examples
Dec 31 15:42:53 Finished translator/monadic/examples                           3m29s   3GB
Dec 31 15:42:53 Starting examples
Dec 31 15:53:03 Finished examples                                             10m08s   3GB
Dec 31 15:53:03 Starting examples/compilation/x64
Dec 31 18:26:39 Finished examples/compilation/x64                           2h33m35s  18GB
Dec 31 18:26:39 Starting examples/compilation/x64/proofs
Jan 01 20:38:28 Resuming examples/compilation/x64/proofs
Jan 01 20:38:31 Finished examples/compilation/x64/proofs                          2s  30MB
Jan 01 20:38:31 Starting examples/compilation/ag32
Jan 01 21:14:00 Finished examples/compilation/ag32                            35m28s  12GB
Jan 01 21:14:00 Starting examples/compilation/ag32/proofs
Jan 01 21:14:49 Finished examples/compilation/ag32/proofs                        48s   3GB
Jan 01 21:14:50 Starting examples/cost
Jan 01 22:15:16 Finished examples/cost                                      1h00m26s   8GB
Jan 01 22:15:17 Starting examples/lpr_checker
Jan 01 22:16:07 Finished examples/lpr_checker                                    50s   1GB
Jan 01 22:16:07 Starting examples/lpr_checker/array
Jan 01 22:47:14 Finished examples/lpr_checker/array                           31m05s   5GB
Jan 01 22:47:14 Starting examples/lpr_checker/array/compilation
Jan 02 00:15:56 Finished examples/lpr_checker/array/compilation             1h28m41s  29GB
Jan 02 00:15:56 Starting examples/lpr_checker/array/compilation/proofs
Jan 02 00:17:14 Finished examples/lpr_checker/array/compilation/proofs         1m17s   6GB
Jan 02 00:17:14 Starting examples/opentheory
Jan 02 00:27:24 Finished examples/opentheory                                  10m09s   5GB
Jan 02 00:27:24 Starting examples/opentheory
Jan 02 00:27:26 Finished examples/opentheory                                      1s  24MB
Jan 02 00:27:26 Starting examples/opentheory/compilation
Jan 02 01:09:24 Finished examples/opentheory/compilation                      41m57s  25GB
Jan 02 01:09:24 Starting examples/opentheory/compilation/proofs
Jan 02 01:10:08 Finished examples/opentheory/compilation/proofs                  43s   3GB
Jan 02 01:10:08 Starting examples/opentheory/compilation/ag32
Jan 02 01:50:38 Finished examples/opentheory/compilation/ag32                 40m29s  25GB
Jan 02 01:50:38 Starting examples/opentheory/compilation/ag32/proofs
Jan 02 01:52:19 Finished examples/opentheory/compilation/ag32/proofs           1m40s   6GB
Jan 02 01:52:19 Starting examples/sat_encodings
Jan 02 01:54:09 Finished examples/sat_encodings                                1m49s 885MB
Jan 02 01:54:10 Starting examples/sat_encodings/case_studies
Jan 02 01:55:51 Finished examples/sat_encodings/case_studies                   1m41s 744MB
Jan 02 01:55:52 Starting examples/sat_encodings/translation
Jan 02 02:01:51 Finished examples/sat_encodings/translation                    5m59s   5GB
Jan 02 02:01:51 Starting examples/sat_encodings/translation/compilation
Jan 02 02:57:15 Finished examples/sat_encodings/translation/compilation       55m23s  20GB
Jan 02 02:57:16 Starting translator/okasaki-examples
Jan 02 03:02:03 Finished translator/okasaki-examples                           4m47s   1GB
Jan 02 03:02:03 Starting translator/other-examples
Jan 02 03:04:03 Finished translator/other-examples                             1m58s   1GB
Jan 02 03:04:03 Starting compiler/parsing/tests
Jan 02 03:04:33 Finished compiler/parsing/tests                                  30s 679MB
Jan 02 03:04:33 Starting compiler/inference/tests
Jan 02 03:12:52 Finished compiler/inference/tests                              8m18s   5GB
Jan 02 03:12:53 Starting compiler/bootstrap/translation
Jan 02 06:01:18 Finished compiler/bootstrap/translation                     2h48m25s  28GB
Jan 02 06:01:19 Starting unverified/sexpr-bootstrap/x64/64
Jan 02 06:10:41 Finished unverified/sexpr-bootstrap/x64/64                     9m21s  10GB
Jan 02 06:10:41 Starting unverified/sexpr-bootstrap/x64/32
Jan 02 06:18:37 Finished unverified/sexpr-bootstrap/x64/32                     7m56s   8GB
Jan 02 06:18:37 Starting compiler/benchmarks
Jan 02 06:18:40 Finished compiler/benchmarks                                      2s  28MB
Jan 02 06:18:40 Starting compiler/bootstrap/compilation/x64/64
Jan 02 20:02:50 Finished compiler/bootstrap/compilation/x64/64             13h44m09s  64GB
Jan 02 20:02:50 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 02 20:05:31 Finished compiler/bootstrap/compilation/x64/64/proofs          2m40s  18GB
Jan 02 20:05:31 Starting compiler/bootstrap/compilation/x64/32
Jan 03 07:41:30 Finished compiler/bootstrap/compilation/x64/32             11h35m57s  64GB
Jan 03 07:41:31 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 03 07:44:34 Finished compiler/bootstrap/compilation/x64/32/proofs          3m02s  12GB
Jan 03 07:44:34 Starting compiler/bootstrap/compilation/ag32/32
Jan 03 19:42:08 Finished compiler/bootstrap/compilation/ag32/32            11h57m33s  64GB
Jan 03 19:42:09 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 03 20:03:54 Finished compiler/bootstrap/compilation/ag32/32/proofs        21m44s  18GB
Jan 03 20:03:54 SUCCESS