Job 1732

CakeML:fe46ca072678de42c6fdfc32f40eafeb917dab02
  Fix proof broken by HOL changes making more rewrites automatic [Jan 20 00:31:55]
HOL:74f42248dbc44958d90a69acf52b5902e11e6683
  Provide more automatic rewrites about positivity of u.l.p constants [Jan 20 23:50:06]
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

Jan 22 11:42:57 Claimed job
Jan 22 11:42:58 Reusing HOL
Jan 22 11:43:10 Starting developers
Jan 22 11:43:15 Finished developers                                               4s 142MB
Jan 22 11:43:15 Starting developers/bin
Jan 22 11:43:19 Finished developers/bin                                           4s 675MB
Jan 22 11:43:19 Starting semantics/ffi
Jan 22 11:43:28 Finished semantics/ffi                                            8s 256MB
Jan 22 11:43:28 Starting semantics
Jan 22 11:45:02 Finished semantics                                             1m33s   1GB
Jan 22 11:45:02 Starting semantics/proofs
Jan 22 11:48:38 Finished semantics/proofs                                      3m35s   1GB
Jan 22 11:48:38 Starting semantics/alt_semantics
Jan 22 11:48:50 Finished semantics/alt_semantics                                 11s 406MB
Jan 22 11:48:50 Starting semantics/alt_semantics/proofs
Jan 22 11:51:16 Finished semantics/alt_semantics/proofs                        2m25s   1GB
Jan 22 11:51:16 Starting basis/pure
Jan 22 11:54:03 Finished basis/pure                                            2m46s 878MB
Jan 22 11:54:04 Starting translator
Jan 22 11:56:54 Finished translator                                            2m49s   1GB
Jan 22 11:56:54 Starting compiler/parsing
Jan 22 11:58:08 Finished compiler/parsing                                      1m14s   2GB
Jan 22 11:58:08 Starting characteristic
Jan 22 12:04:01 Finished characteristic                                        5m51s   1GB
Jan 22 12:04:01 Starting translator/monadic
Jan 22 12:05:47 Finished translator/monadic                                    1m46s   1GB
Jan 22 12:05:47 Starting basis
Jan 22 12:51:54 Finished basis                                                46m07s  14GB
Jan 22 12:51:54 Starting compiler/inference
Jan 22 12:53:11 Finished compiler/inference                                    1m16s   1GB
Jan 22 12:53:11 Starting compiler/backend/reg_alloc
Jan 22 12:54:18 Finished compiler/backend/reg_alloc                            1m07s   1GB
Jan 22 12:54:18 Starting compiler/backend/gc
Jan 22 12:57:55 Finished compiler/backend/gc                                   3m36s   2GB
Jan 22 12:57:55 Starting compiler/backend
Jan 22 13:02:59 Finished compiler/backend                                      5m03s   2GB
Jan 22 13:02:59 Starting compiler/encoders/asm
Jan 22 13:03:23 Finished compiler/encoders/asm                                   23s 742MB
Jan 22 13:03:23 Starting compiler/encoders/x64
Jan 22 13:04:29 Finished compiler/encoders/x64                                 1m01s   1GB
Jan 22 13:04:29 Starting compiler/encoders/arm7
Jan 22 13:06:34 Finished compiler/encoders/arm7                                2m05s   1GB
Jan 22 13:06:34 Starting compiler/encoders/arm8
Jan 22 13:07:14 Finished compiler/encoders/arm8                                  39s 843MB
Jan 22 13:07:14 Starting compiler/encoders/mips
Jan 22 13:08:41 Finished compiler/encoders/mips                                1m27s   1GB
Jan 22 13:08:42 Starting compiler/encoders/riscv
Jan 22 13:10:26 Finished compiler/encoders/riscv                               1m44s   1GB
Jan 22 13:10:26 Starting compiler/encoders/ag32
Jan 22 13:10:45 Finished compiler/encoders/ag32                                  19s 722MB
Jan 22 13:10:45 Starting compiler/backend/x64
Jan 22 13:11:06 Finished compiler/backend/x64                                    20s   1GB
Jan 22 13:11:06 Starting compiler/backend/arm7
Jan 22 13:11:27 Finished compiler/backend/arm7                                   20s   1GB
Jan 22 13:11:27 Starting compiler/backend/arm8
Jan 22 13:11:48 Finished compiler/backend/arm8                                   21s   1GB
Jan 22 13:11:48 Starting compiler/backend/mips
Jan 22 13:12:10 Finished compiler/backend/mips                                   20s   1GB
Jan 22 13:12:10 Starting compiler/backend/riscv
Jan 22 13:12:31 Finished compiler/backend/riscv                                  21s   1GB
Jan 22 13:12:31 Starting compiler/backend/ag32
Jan 22 13:13:41 Finished compiler/backend/ag32                                 1m10s   1GB
Jan 22 13:13:42 Starting compiler/parsing/proofs
Jan 22 13:17:25 Finished compiler/parsing/proofs                               3m43s   1GB
Jan 22 13:17:25 Starting compiler/inference/proofs
Jan 22 13:19:52 Finished compiler/inference/proofs                             2m27s 846MB
Jan 22 13:19:53 Starting compiler/backend/semantics
Jan 22 13:48:22 Finished compiler/backend/semantics                           28m29s   2GB
Jan 22 13:48:22 Starting compiler/backend/reg_alloc/proofs
Jan 22 13:51:48 Finished compiler/backend/reg_alloc/proofs                     3m26s 849MB
Jan 22 13:51:48 Starting compiler/backend/proofs
Jan 22 14:43:28 Finished compiler/backend/proofs                              51m38s  21GB
Jan 22 14:43:28 Starting compiler/backend/serialiser
Jan 22 14:44:54 Finished compiler/backend/serialiser                           1m25s   1GB
Jan 22 14:44:54 Starting compiler/encoders/x64/proofs
Jan 22 14:54:27 Finished compiler/encoders/x64/proofs                          9m33s   4GB
Jan 22 14:54:27 Starting compiler/encoders/arm7/proofs
Jan 22 15:07:35 Finished compiler/encoders/arm7/proofs                        13m07s   8GB
Jan 22 15:07:35 Starting compiler/encoders/arm8/proofs
Jan 22 15:14:22 Finished compiler/encoders/arm8/proofs                         6m46s   1GB
Jan 22 15:14:22 Starting compiler/encoders/mips/proofs
Jan 22 15:24:18 Finished compiler/encoders/mips/proofs                         9m55s   2GB
Jan 22 15:24:18 Starting compiler/encoders/riscv/proofs
Jan 22 15:33:14 Finished compiler/encoders/riscv/proofs                        8m56s   1GB
Jan 22 15:33:14 Starting compiler/encoders/ag32/proofs
Jan 22 15:35:49 Finished compiler/encoders/ag32/proofs                         2m35s 651MB
Jan 22 15:35:50 Starting compiler/backend/x64/proofs
Jan 22 15:36:15 Finished compiler/backend/x64/proofs                             25s   1GB
Jan 22 15:36:15 Starting compiler/backend/arm7/proofs
Jan 22 15:36:43 Finished compiler/backend/arm7/proofs                            27s   1GB
Jan 22 15:36:43 Starting compiler/backend/arm8/proofs
Jan 22 15:37:09 Finished compiler/backend/arm8/proofs                            26s   2GB
Jan 22 15:37:09 Starting compiler/backend/mips/proofs
Jan 22 15:37:37 Finished compiler/backend/mips/proofs                            27s   1GB
Jan 22 15:37:37 Starting compiler/backend/riscv/proofs
Jan 22 15:38:03 Finished compiler/backend/riscv/proofs                           26s   1GB
Jan 22 15:38:03 Starting compiler/backend/ag32/proofs
Jan 22 15:50:44 Finished compiler/backend/ag32/proofs                         12m39s   2GB
Jan 22 15:50:44 Starting compiler/proofs
Jan 22 15:52:52 Finished compiler/proofs                                       2m07s   3GB
Jan 22 15:52:52 Starting candle/set-theory
Jan 22 15:53:20 Finished candle/set-theory                                       28s 711MB
Jan 22 15:53:20 Starting candle/syntax-lib
Jan 22 15:53:31 Finished candle/syntax-lib                                       10s 638MB
Jan 22 15:53:32 Starting candle/standard/syntax
Jan 22 15:55:19 Finished candle/standard/syntax                                1m47s   1GB
Jan 22 15:55:19 Starting candle/standard/semantics
Jan 22 15:57:05 Finished candle/standard/semantics                             1m45s   1GB
Jan 22 15:57:05 Starting candle/standard/monadic
Jan 22 15:58:41 Finished candle/standard/monadic                               1m35s   1GB
Jan 22 15:58:41 Starting candle/standard/ml_kernel
Jan 22 16:05:19 Finished candle/standard/ml_kernel                             6m38s   3GB
Jan 22 16:05:19 Starting candle/overloading/syntax
Jan 22 16:08:25 Finished candle/overloading/syntax                             3m05s   1GB
Jan 22 16:08:25 Starting candle/overloading/semantics
Jan 22 16:20:08 Finished candle/overloading/semantics                         11m42s   2GB
Jan 22 16:20:08 Starting candle/prover
Jan 22 16:27:36 Finished candle/prover                                         7m28s   2GB
Jan 22 16:27:37 Starting pancake
Jan 22 16:30:15 Finished pancake                                               2m38s   2GB
Jan 22 16:30:15 Starting pancake/ffi
Jan 22 16:30:15 Finished pancake/ffi                                              0s  35MB
Jan 22 16:30:15 Starting pancake/semantics
Jan 22 16:32:44 Finished pancake/semantics                                     2m28s   1GB
Jan 22 16:32:44 Starting pancake/proofs
Jan 22 16:44:36 Finished pancake/proofs                                       11m52s   7GB
Jan 22 16:44:36 Starting characteristic/examples
Jan 22 16:45:58 Finished characteristic/examples                               1m21s   3GB
Jan 22 16:45:58 Starting tutorial/solutions
Jan 22 17:02:04 Finished tutorial/solutions                                   16m05s  13GB
Jan 22 17:02:04 Starting translator/monadic/examples
Jan 22 17:05:29 Finished translator/monadic/examples                           3m24s   3GB
Jan 22 17:05:29 Starting examples
Jan 22 17:14:45 Finished examples                                              9m16s   4GB
Jan 22 17:14:45 Starting examples/compilation/x64
Jan 22 19:42:41 Finished examples/compilation/x64                           2h27m54s  16GB
Jan 22 19:42:41 Starting examples/compilation/x64/proofs
Jan 22 19:45:23 Finished examples/compilation/x64/proofs                       2m41s   2GB
Jan 22 19:45:23 Starting examples/compilation/ag32
Jan 22 20:19:50 Finished examples/compilation/ag32                            34m26s   9GB
Jan 22 20:19:50 Starting examples/compilation/ag32/proofs
Jan 22 20:20:42 Finished examples/compilation/ag32/proofs                        52s   3GB
Jan 22 20:20:43 Starting examples/cost
Jan 22 21:16:11 Finished examples/cost                                        55m27s   9GB
Jan 22 21:16:11 Starting examples/lpr_checker
Jan 22 21:17:03 Finished examples/lpr_checker                                    52s 662MB
Jan 22 21:17:03 Starting examples/lpr_checker/array
Jan 22 21:45:30 Finished examples/lpr_checker/array                           28m26s   6GB
Jan 22 21:45:30 Starting examples/lpr_checker/array/compilation
Jan 22 23:10:40 Finished examples/lpr_checker/array/compilation             1h25m08s  33GB
Jan 22 23:10:40 Starting examples/lpr_checker/array/compilation/proofs
Jan 22 23:12:02 Finished examples/lpr_checker/array/compilation/proofs         1m21s   6GB
Jan 22 23:12:02 Starting examples/opentheory
Jan 22 23:21:50 Finished examples/opentheory                                   9m48s   4GB
Jan 22 23:21:51 Starting examples/opentheory
Jan 22 23:21:52 Finished examples/opentheory                                      1s 133MB
Jan 22 23:21:52 Starting examples/opentheory/compilation
Jan 23 00:01:07 Finished examples/opentheory/compilation                      39m15s  32GB
Jan 23 00:01:07 Starting examples/opentheory/compilation/proofs
Jan 23 00:02:01 Finished examples/opentheory/compilation/proofs                  53s   4GB
Jan 23 00:02:01 Starting examples/opentheory/compilation/ag32
Jan 23 00:40:55 Finished examples/opentheory/compilation/ag32                 38m53s  45GB
Jan 23 00:40:55 Starting examples/opentheory/compilation/ag32/proofs
Jan 23 00:42:38 Finished examples/opentheory/compilation/ag32/proofs           1m41s   3GB
Jan 23 00:42:38 Starting examples/sat_encodings
Jan 23 00:44:36 Finished examples/sat_encodings                                1m58s 707MB
Jan 23 00:44:36 Starting examples/sat_encodings/case_studies
Jan 23 00:46:18 Finished examples/sat_encodings/case_studies                   1m41s 684MB
Jan 23 00:46:18 Starting examples/sat_encodings/translation
Jan 23 00:51:55 Finished examples/sat_encodings/translation                    5m37s   3GB
Jan 23 00:51:56 Starting examples/sat_encodings/translation/compilation
Jan 23 01:40:30 Finished examples/sat_encodings/translation/compilation       48m33s  21GB
Jan 23 01:40:30 Starting translator/okasaki-examples
Jan 23 01:45:04 Finished translator/okasaki-examples                           4m33s   1GB
Jan 23 01:45:04 Starting translator/other-examples
Jan 23 01:46:58 Finished translator/other-examples                             1m53s   1GB
Jan 23 01:46:58 Starting compiler/parsing/tests
Jan 23 01:47:27 Finished compiler/parsing/tests                                  28s 664MB
Jan 23 01:47:27 Starting compiler/inference/tests
Jan 23 01:55:26 Finished compiler/inference/tests                              7m58s   5GB
Jan 23 01:55:26 Starting compiler/bootstrap/translation
Jan 23 04:30:02 Finished compiler/bootstrap/translation                     2h34m33s  34GB
Jan 23 04:30:04 Starting unverified/sexpr-bootstrap/x64/64
Jan 23 04:40:13 Finished unverified/sexpr-bootstrap/x64/64                    10m08s   8GB
Jan 23 04:40:13 Starting unverified/sexpr-bootstrap/x64/32
Jan 23 04:49:01 Finished unverified/sexpr-bootstrap/x64/32                     8m47s   8GB
Jan 23 04:49:01 Starting compiler/benchmarks
Jan 23 04:49:57 Finished compiler/benchmarks                                     55s 673MB
Jan 23 04:49:57 Starting compiler/bootstrap/compilation/x64/64
Jan 23 17:22:52 Finished compiler/bootstrap/compilation/x64/64             12h32m53s  64GB
Jan 23 17:22:52 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 23 17:25:18 Finished compiler/bootstrap/compilation/x64/64/proofs          2m25s  15GB
Jan 23 17:25:18 Starting compiler/bootstrap/compilation/x64/32
Jan 24 04:25:18 Finished compiler/bootstrap/compilation/x64/32             10h59m57s  64GB
Jan 24 04:25:18 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 24 04:28:41 Finished compiler/bootstrap/compilation/x64/32/proofs          3m22s  12GB
Jan 24 04:28:41 Starting compiler/bootstrap/compilation/ag32/32
Jan 24 15:38:43 Finished compiler/bootstrap/compilation/ag32/32            11h10m01s  64GB
Jan 24 15:38:43 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 24 16:12:53 Finished compiler/bootstrap/compilation/ag32/32/proofs        34m09s  23GB
Jan 24 16:12:53 SUCCESS