Job 1540

CakeML:36d5c13ef89908d2c2bf082c13186087bd1502f6
  Merge pull request #828 from CakeML/sat_encodings [Jun 04 08:57:36]
HOL:d441797f18535e1792c7d946c10bcdf174c66121
  Prove SET and MAP axioms for new algebraic type [Jun 03 11:50:47]
Machine:stove 4.15.0-143-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

Jun 04 09:11:04 Claimed job
Jun 04 09:11:08 Building HOL
Jun 04 09:26:03 Starting developers
Jun 04 09:26:08 Finished developers                                               4s  93MB
Jun 04 09:26:08 Starting developers/bin
Jun 04 09:26:14 Finished developers/bin                                           6s   1GB
Jun 04 09:26:14 Starting semantics/ffi
Jun 04 09:26:25 Finished semantics/ffi                                           10s 253MB
Jun 04 09:26:25 Starting semantics
Jun 04 09:27:57 Finished semantics                                             1m31s   1GB
Jun 04 09:27:57 Starting semantics/proofs
Jun 04 09:32:40 Finished semantics/proofs                                      4m42s   1GB
Jun 04 09:32:40 Starting semantics/alt_semantics
Jun 04 09:32:50 Finished semantics/alt_semantics                                  9s 324MB
Jun 04 09:32:50 Starting semantics/alt_semantics/proofs
Jun 04 09:35:03 Finished semantics/alt_semantics/proofs                        2m13s 900MB
Jun 04 09:35:03 Starting basis/pure
Jun 04 09:38:00 Finished basis/pure                                            2m56s   1GB
Jun 04 09:38:00 Starting translator
Jun 04 09:41:17 Finished translator                                            3m17s   1GB
Jun 04 09:41:17 Starting compiler/parsing
Jun 04 09:42:26 Finished compiler/parsing                                      1m08s   2GB
Jun 04 09:42:26 Starting characteristic
Jun 04 09:48:05 Finished characteristic                                        5m39s   1GB
Jun 04 09:48:06 Starting translator/monadic
Jun 04 09:49:44 Finished translator/monadic                                    1m38s   1GB
Jun 04 09:49:44 Starting basis
Jun 04 10:33:26 Finished basis                                                43m41s  15GB
Jun 04 10:33:26 Starting compiler/inference
Jun 04 10:34:41 Finished compiler/inference                                    1m15s   1GB
Jun 04 10:34:41 Starting compiler/backend/reg_alloc
Jun 04 10:35:50 Finished compiler/backend/reg_alloc                            1m08s   1GB
Jun 04 10:35:50 Starting compiler/backend/gc
Jun 04 10:39:20 Finished compiler/backend/gc                                   3m30s   2GB
Jun 04 10:39:20 Starting compiler/backend
Jun 04 10:44:07 Finished compiler/backend                                      4m46s   4GB
Jun 04 10:44:07 Starting compiler/encoders/asm
Jun 04 10:44:30 Finished compiler/encoders/asm                                   22s 674MB
Jun 04 10:44:30 Starting compiler/encoders/x64
Jun 04 10:45:30 Finished compiler/encoders/x64                                 1m00s 793MB
Jun 04 10:45:31 Starting compiler/encoders/arm7
Jun 04 10:47:32 Finished compiler/encoders/arm7                                2m01s   1GB
Jun 04 10:47:32 Starting compiler/encoders/arm8
Jun 04 10:48:10 Finished compiler/encoders/arm8                                  37s 691MB
Jun 04 10:48:10 Starting compiler/encoders/mips
Jun 04 10:49:37 Finished compiler/encoders/mips                                1m26s   1GB
Jun 04 10:49:37 Starting compiler/encoders/riscv
Jun 04 10:51:22 Finished compiler/encoders/riscv                               1m44s 841MB
Jun 04 10:51:22 Starting compiler/encoders/ag32
Jun 04 10:51:40 Finished compiler/encoders/ag32                                  17s 908MB
Jun 04 10:51:40 Starting compiler/backend/x64
Jun 04 10:51:59 Finished compiler/backend/x64                                    19s   1GB
Jun 04 10:51:59 Starting compiler/backend/arm7
Jun 04 10:52:20 Finished compiler/backend/arm7                                   21s   1GB
Jun 04 10:52:21 Starting compiler/backend/arm8
Jun 04 10:52:38 Finished compiler/backend/arm8                                   17s   1GB
Jun 04 10:52:39 Starting compiler/backend/mips
Jun 04 10:52:58 Finished compiler/backend/mips                                   19s   1GB
Jun 04 10:52:58 Starting compiler/backend/riscv
Jun 04 10:53:19 Finished compiler/backend/riscv                                  20s   1GB
Jun 04 10:53:19 Starting compiler/backend/ag32
Jun 04 10:54:29 Finished compiler/backend/ag32                                 1m09s   1GB
Jun 04 10:54:29 Starting compiler/parsing/proofs
Jun 04 11:00:35 Finished compiler/parsing/proofs                               6m05s 893MB
Jun 04 11:00:35 Starting compiler/inference/proofs
Jun 04 11:03:04 Finished compiler/inference/proofs                             2m29s   1GB
Jun 04 11:03:04 Starting compiler/backend/semantics
Jun 04 11:31:14 Finished compiler/backend/semantics                           28m10s   3GB
Jun 04 11:31:15 Starting compiler/backend/reg_alloc/proofs
Jun 04 11:34:41 Finished compiler/backend/reg_alloc/proofs                     3m25s   1GB
Jun 04 11:34:41 Starting compiler/backend/proofs
Jun 04 12:25:36 Finished compiler/backend/proofs                              50m55s  19GB
Jun 04 12:25:36 Starting compiler/encoders/x64/proofs
Jun 04 12:35:12 Finished compiler/encoders/x64/proofs                          9m35s   4GB
Jun 04 12:35:12 Starting compiler/encoders/arm7/proofs
Jun 04 12:48:19 Finished compiler/encoders/arm7/proofs                        13m06s   3GB
Jun 04 12:48:19 Starting compiler/encoders/arm8/proofs
Jun 04 12:55:05 Finished compiler/encoders/arm8/proofs                         6m45s   1GB
Jun 04 12:55:05 Starting compiler/encoders/mips/proofs
Jun 04 13:05:05 Finished compiler/encoders/mips/proofs                         9m59s   2GB
Jun 04 13:05:05 Starting compiler/encoders/riscv/proofs
Jun 04 13:13:57 Finished compiler/encoders/riscv/proofs                        8m51s   1GB
Jun 04 13:13:57 Starting compiler/encoders/ag32/proofs
Jun 04 13:16:31 Finished compiler/encoders/ag32/proofs                         2m33s 667MB
Jun 04 13:16:31 Starting compiler/backend/x64/proofs
Jun 04 13:16:53 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 04 13:16:53 Starting compiler/backend/arm7/proofs
Jun 04 13:17:16 Finished compiler/backend/arm7/proofs                            22s   1GB
Jun 04 13:17:16 Starting compiler/backend/arm8/proofs
Jun 04 13:17:39 Finished compiler/backend/arm8/proofs                            22s   2GB
Jun 04 13:17:39 Starting compiler/backend/mips/proofs
Jun 04 13:18:00 Finished compiler/backend/mips/proofs                            21s   1GB
Jun 04 13:18:01 Starting compiler/backend/riscv/proofs
Jun 04 13:18:24 Finished compiler/backend/riscv/proofs                           22s   1GB
Jun 04 13:18:24 Starting compiler/backend/ag32/proofs
Jun 04 13:30:42 Finished compiler/backend/ag32/proofs                         12m18s   3GB
Jun 04 13:30:42 Starting compiler/proofs
Jun 04 13:32:36 Finished compiler/proofs                                       1m54s   3GB
Jun 04 13:32:36 Starting candle/set-theory
Jun 04 13:33:05 Finished candle/set-theory                                       28s 777MB
Jun 04 13:33:06 Starting candle/syntax-lib
Jun 04 13:33:17 Finished candle/syntax-lib                                       10s 658MB
Jun 04 13:33:17 Starting candle/standard/syntax
Jun 04 13:35:08 Finished candle/standard/syntax                                1m51s 973MB
Jun 04 13:35:08 Starting candle/standard/semantics
Jun 04 13:36:52 Finished candle/standard/semantics                             1m43s   1GB
Jun 04 13:36:52 Starting candle/standard/monadic
Jun 04 13:38:36 Finished candle/standard/monadic                               1m43s   1GB
Jun 04 13:38:38 Starting candle/standard/ml_kernel
Jun 04 13:44:20 Finished candle/standard/ml_kernel                             5m41s   4GB
Jun 04 13:44:20 Starting candle/overloading/syntax
Jun 04 13:47:29 Finished candle/overloading/syntax                             3m09s   1GB
Jun 04 13:47:30 Starting candle/overloading/semantics
Jun 04 13:59:28 Finished candle/overloading/semantics                         11m57s   4GB
Jun 04 13:59:28 Starting characteristic/examples
Jun 04 14:00:46 Finished characteristic/examples                               1m18s   3GB
Jun 04 14:00:46 Starting tutorial/solutions
Jun 04 14:16:15 Finished tutorial/solutions                                   15m28s   8GB
Jun 04 14:16:15 Starting translator/monadic/examples
Jun 04 14:19:31 Finished translator/monadic/examples                           3m15s   3GB
Jun 04 14:19:31 Starting examples
Jun 04 14:28:01 Finished examples                                              8m29s   3GB
Jun 04 14:28:01 Starting examples/compilation/x64
Jun 04 16:52:10 Finished examples/compilation/x64                           2h24m09s  15GB
Jun 04 16:52:10 Starting examples/compilation/x64/proofs
Jun 04 16:53:52 Finished examples/compilation/x64/proofs                       1m41s   3GB
Jun 04 16:53:53 Starting examples/compilation/ag32
Jun 04 17:27:46 Finished examples/compilation/ag32                            33m53s   8GB
Jun 04 17:27:46 Starting examples/compilation/ag32/proofs
Jun 04 17:28:58 Finished examples/compilation/ag32/proofs                      1m11s   2GB
Jun 04 17:28:58 Starting examples/cost
Jun 04 18:22:32 Finished examples/cost                                        53m34s   8GB
Jun 04 18:22:32 Starting examples/lpr_checker
Jun 04 18:26:30 Finished examples/lpr_checker                                  3m57s   2GB
Jun 04 18:26:31 Starting examples/lpr_checker/compilation
Jun 04 18:44:32 Finished examples/lpr_checker/compilation                     18m00s  11GB
Jun 04 18:44:32 Starting examples/lpr_checker/compilation/proofs
Jun 04 18:45:14 Finished examples/lpr_checker/compilation/proofs                 42s   2GB
Jun 04 18:45:14 Starting examples/lpr_checker/array
Jun 04 18:59:33 Finished examples/lpr_checker/array                           14m18s   4GB
Jun 04 18:59:33 Starting examples/lpr_checker/array/compilation
Jun 04 19:19:19 Finished examples/lpr_checker/array/compilation               19m46s  13GB
Jun 04 19:19:19 Starting examples/lpr_checker/array/compilation/proofs
Jun 04 19:20:09 Finished examples/lpr_checker/array/compilation/proofs           49s   4GB
Jun 04 19:20:09 Starting examples/opentheory
Jun 04 19:29:44 Finished examples/opentheory                                   9m34s   6GB
Jun 04 19:29:44 Starting examples/opentheory
Jun 04 19:29:46 Finished examples/opentheory                                      1s  35MB
Jun 04 19:29:46 Starting examples/opentheory/compilation
Jun 04 20:01:14 Finished examples/opentheory/compilation                      31m28s  19GB
Jun 04 20:01:15 Starting examples/opentheory/compilation/proofs
Jun 04 20:01:59 Finished examples/opentheory/compilation/proofs                  44s   2GB
Jun 04 20:01:59 Starting examples/opentheory/compilation/ag32
Jun 04 20:36:13 Finished examples/opentheory/compilation/ag32                 34m13s  18GB
Jun 04 20:36:13 Starting examples/opentheory/compilation/ag32/proofs
Jun 04 20:37:50 Finished examples/opentheory/compilation/ag32/proofs           1m36s   3GB
Jun 04 20:37:50 Starting examples/sat_encodings
Jun 04 20:39:37 Finished examples/sat_encodings                                1m46s 863MB
Jun 04 20:39:37 Starting examples/sat_encodings/case_studies
Jun 04 20:41:09 Finished examples/sat_encodings/case_studies                   1m31s 787MB
Jun 04 20:41:09 Starting examples/sat_encodings/translation
Jun 04 20:46:49 Finished examples/sat_encodings/translation                    5m39s   5GB
Jun 04 20:46:49 Starting examples/sat_encodings/translation/compilation
Jun 04 21:27:47 Finished examples/sat_encodings/translation/compilation       40m57s  12GB
Jun 04 21:27:47 Starting translator/okasaki-examples
Jun 04 21:32:11 Finished translator/okasaki-examples                           4m23s   1GB
Jun 04 21:32:11 Starting translator/other-examples
Jun 04 21:34:16 Finished translator/other-examples                             2m04s   1GB
Jun 04 21:34:16 Starting compiler/parsing/tests
Jun 04 21:34:42 Finished compiler/parsing/tests                                  26s 704MB
Jun 04 21:34:42 Starting compiler/inference/tests
Jun 04 21:42:25 Finished compiler/inference/tests                              7m42s   6GB
Jun 04 21:42:25 Starting compiler/bootstrap/translation
Jun 05 00:11:04 Finished compiler/bootstrap/translation                     2h28m38s  29GB
Jun 05 00:11:04 Starting unverified/sexpr-bootstrap/x64/64
Jun 05 00:23:19 Finished unverified/sexpr-bootstrap/x64/64                    12m14s   8GB
Jun 05 00:23:19 Starting unverified/sexpr-bootstrap/x64/32
Jun 05 00:33:50 Finished unverified/sexpr-bootstrap/x64/32                    10m29s   8GB
Jun 05 00:33:50 Starting compiler/benchmarks
Jun 05 00:33:52 Finished compiler/benchmarks                                      1s  34MB
Jun 05 00:33:52 Starting compiler/bootstrap/compilation/x64/64
Jun 05 12:56:16 Finished compiler/bootstrap/compilation/x64/64             12h22m22s  64GB
Jun 05 12:56:16 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 05 12:59:33 Finished compiler/bootstrap/compilation/x64/64/proofs          3m16s  12GB
Jun 05 12:59:33 Starting compiler/bootstrap/compilation/x64/32
Jun 05 23:57:52 Finished compiler/bootstrap/compilation/x64/32             10h58m18s  64GB
Jun 05 23:57:52 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 06 00:00:43 Finished compiler/bootstrap/compilation/x64/32/proofs          2m51s  11GB
Jun 06 00:00:43 Starting compiler/bootstrap/compilation/ag32/32
Jun 06 11:24:14 Finished compiler/bootstrap/compilation/ag32/32            11h23m30s  64GB
Jun 06 11:24:14 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 06 11:50:55 Finished compiler/bootstrap/compilation/ag32/32/proofs        26m41s  21GB
Jun 06 11:50:56 SUCCESS