Job 1729

CakeML:fe46ca072678de42c6fdfc32f40eafeb917dab02
  Fix proof broken by HOL changes making more rewrites automatic [Jan 20 00:31:55]
HOL:27accc7f32d82c0cdc10754fd834b339ec17021f
  Tidy up some floating point proofs and extend bounds thms for sqrt [Jan 18 06:17:24]
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 20 01:11:54 Claimed job
Jan 20 01:11:58 Reusing HOL
Jan 20 01:12:10 Starting developers
Jan 20 01:12:15 Finished developers                                               4s 130MB
Jan 20 01:12:15 Starting developers/bin
Jan 20 01:12:19 Finished developers/bin                                           4s 674MB
Jan 20 01:12:19 Starting semantics/ffi
Jan 20 01:12:28 Finished semantics/ffi                                            8s 219MB
Jan 20 01:12:28 Starting semantics
Jan 20 01:13:54 Finished semantics                                             1m25s   1GB
Jan 20 01:13:54 Starting semantics/proofs
Jan 20 01:17:28 Finished semantics/proofs                                      3m33s   1GB
Jan 20 01:17:28 Starting semantics/alt_semantics
Jan 20 01:17:39 Finished semantics/alt_semantics                                 11s 355MB
Jan 20 01:17:39 Starting semantics/alt_semantics/proofs
Jan 20 01:20:06 Finished semantics/alt_semantics/proofs                        2m26s 903MB
Jan 20 01:20:07 Starting basis/pure
Jan 20 01:20:58 Finished basis/pure                                              51s 696MB
Jan 20 01:20:58 Starting translator
Jan 20 01:23:52 Finished translator                                            2m53s   1GB
Jan 20 01:23:53 Starting compiler/parsing
Jan 20 01:25:10 Finished compiler/parsing                                      1m16s   2GB
Jan 20 01:25:10 Starting characteristic
Jan 20 01:31:02 Finished characteristic                                        5m51s   1GB
Jan 20 01:31:02 Starting translator/monadic
Jan 20 01:32:45 Finished translator/monadic                                    1m43s   1GB
Jan 20 01:32:45 Starting basis
Jan 20 02:17:21 Finished basis                                                44m33s  20GB
Jan 20 02:17:21 Starting compiler/inference
Jan 20 02:18:27 Finished compiler/inference                                    1m06s   1GB
Jan 20 02:18:28 Starting compiler/backend/reg_alloc
Jan 20 02:19:33 Finished compiler/backend/reg_alloc                            1m05s   1GB
Jan 20 02:19:33 Starting compiler/backend/gc
Jan 20 02:22:49 Finished compiler/backend/gc                                   3m15s   2GB
Jan 20 02:22:49 Starting compiler/backend
Jan 20 02:27:24 Finished compiler/backend                                      4m34s   2GB
Jan 20 02:27:24 Starting compiler/encoders/asm
Jan 20 02:27:46 Finished compiler/encoders/asm                                   22s 685MB
Jan 20 02:27:46 Starting compiler/encoders/x64
Jan 20 02:28:12 Finished compiler/encoders/x64                                   25s   1GB
Jan 20 02:28:12 Starting compiler/encoders/arm7
Jan 20 02:29:01 Finished compiler/encoders/arm7                                  48s 769MB
Jan 20 02:29:01 Starting compiler/encoders/arm8
Jan 20 02:29:14 Finished compiler/encoders/arm8                                  13s 960MB
Jan 20 02:29:15 Starting compiler/encoders/mips
Jan 20 02:29:32 Finished compiler/encoders/mips                                  17s   1GB
Jan 20 02:29:32 Starting compiler/encoders/riscv
Jan 20 02:29:47 Finished compiler/encoders/riscv                                 14s 719MB
Jan 20 02:29:47 Starting compiler/encoders/ag32
Jan 20 02:30:05 Finished compiler/encoders/ag32                                  18s 863MB
Jan 20 02:30:05 Starting compiler/backend/x64
Jan 20 02:30:25 Finished compiler/backend/x64                                    19s   1GB
Jan 20 02:30:25 Starting compiler/backend/arm7
Jan 20 02:30:46 Finished compiler/backend/arm7                                   21s   1GB
Jan 20 02:30:46 Starting compiler/backend/arm8
Jan 20 02:31:06 Finished compiler/backend/arm8                                   19s   1GB
Jan 20 02:31:07 Starting compiler/backend/mips
Jan 20 02:31:26 Finished compiler/backend/mips                                   19s   1GB
Jan 20 02:31:26 Starting compiler/backend/riscv
Jan 20 02:31:46 Finished compiler/backend/riscv                                  19s   1GB
Jan 20 02:31:46 Starting compiler/backend/ag32
Jan 20 02:32:53 Finished compiler/backend/ag32                                 1m06s   1GB
Jan 20 02:32:53 Starting compiler/parsing/proofs
Jan 20 02:36:32 Finished compiler/parsing/proofs                               3m39s   1GB
Jan 20 02:36:32 Starting compiler/inference/proofs
Jan 20 02:38:55 Finished compiler/inference/proofs                             2m22s   1GB
Jan 20 02:38:55 Starting compiler/backend/semantics
Jan 20 03:06:18 Finished compiler/backend/semantics                           27m23s   1GB
Jan 20 03:06:18 Starting compiler/backend/reg_alloc/proofs
Jan 20 03:09:39 Finished compiler/backend/reg_alloc/proofs                     3m21s   1GB
Jan 20 03:09:40 Starting compiler/backend/proofs
Jan 20 04:00:28 Finished compiler/backend/proofs                              50m47s  17GB
Jan 20 04:00:28 Starting compiler/backend/serialiser
Jan 20 04:01:42 Finished compiler/backend/serialiser                           1m13s   1GB
Jan 20 04:01:42 Starting compiler/encoders/x64/proofs
Jan 20 04:11:16 Finished compiler/encoders/x64/proofs                          9m33s   4GB
Jan 20 04:11:16 Starting compiler/encoders/arm7/proofs
Jan 20 04:24:24 Finished compiler/encoders/arm7/proofs                        13m08s   6GB
Jan 20 04:24:25 Starting compiler/encoders/arm8/proofs
Jan 20 04:31:12 Finished compiler/encoders/arm8/proofs                         6m47s   1GB
Jan 20 04:31:12 Starting compiler/encoders/mips/proofs
Jan 20 04:41:13 Finished compiler/encoders/mips/proofs                        10m01s   1GB
Jan 20 04:41:14 Starting compiler/encoders/riscv/proofs
Jan 20 04:49:56 Finished compiler/encoders/riscv/proofs                        8m42s   1GB
Jan 20 04:49:56 Starting compiler/encoders/ag32/proofs
Jan 20 04:52:26 Finished compiler/encoders/ag32/proofs                         2m29s   1GB
Jan 20 04:52:26 Starting compiler/backend/x64/proofs
Jan 20 04:52:49 Finished compiler/backend/x64/proofs                             22s   1GB
Jan 20 04:52:49 Starting compiler/backend/arm7/proofs
Jan 20 04:53:13 Finished compiler/backend/arm7/proofs                            23s   1GB
Jan 20 04:53:13 Starting compiler/backend/arm8/proofs
Jan 20 04:53:37 Finished compiler/backend/arm8/proofs                            23s   1GB
Jan 20 04:53:37 Starting compiler/backend/mips/proofs
Jan 20 04:54:00 Finished compiler/backend/mips/proofs                            23s   1GB
Jan 20 04:54:00 Starting compiler/backend/riscv/proofs
Jan 20 04:54:24 Finished compiler/backend/riscv/proofs                           23s   1GB
Jan 20 04:54:24 Starting compiler/backend/ag32/proofs
Jan 20 05:06:55 Finished compiler/backend/ag32/proofs                         12m29s   2GB
Jan 20 05:06:55 Starting compiler/proofs
Jan 20 05:08:53 Finished compiler/proofs                                       1m58s   3GB
Jan 20 05:08:53 Starting candle/set-theory
Jan 20 05:09:21 Finished candle/set-theory                                       27s 791MB
Jan 20 05:09:22 Starting candle/syntax-lib
Jan 20 05:09:32 Finished candle/syntax-lib                                       10s 622MB
Jan 20 05:09:32 Starting candle/standard/syntax
Jan 20 05:11:19 Finished candle/standard/syntax                                1m46s   1GB
Jan 20 05:11:19 Starting candle/standard/semantics
Jan 20 05:13:01 Finished candle/standard/semantics                             1m41s   1GB
Jan 20 05:13:01 Starting candle/standard/monadic
Jan 20 05:14:34 Finished candle/standard/monadic                               1m33s   1GB
Jan 20 05:14:35 Starting candle/standard/ml_kernel
Jan 20 05:21:12 Finished candle/standard/ml_kernel                             6m37s   4GB
Jan 20 05:21:12 Starting candle/overloading/syntax
Jan 20 05:24:11 Finished candle/overloading/syntax                             2m58s   1GB
Jan 20 05:24:11 Starting candle/overloading/semantics
Jan 20 05:35:44 Finished candle/overloading/semantics                         11m32s   2GB
Jan 20 05:35:44 Starting candle/prover
Jan 20 05:42:55 Finished candle/prover                                         7m10s   3GB
Jan 20 05:42:55 Starting pancake
Jan 20 05:44:50 Finished pancake                                               1m55s   2GB
Jan 20 05:44:50 Starting pancake/ffi
Jan 20 05:44:50 Finished pancake/ffi                                              0s   7MB
Jan 20 05:44:51 Starting pancake/semantics
Jan 20 05:47:05 Finished pancake/semantics                                     2m14s   1GB
Jan 20 05:47:05 Starting pancake/proofs
Jan 20 05:58:44 Finished pancake/proofs                                       11m39s   6GB
Jan 20 05:58:44 Starting characteristic/examples
Jan 20 06:00:05 Finished characteristic/examples                               1m20s   3GB
Jan 20 06:00:05 Starting tutorial/solutions
Jan 20 06:16:36 Finished tutorial/solutions                                   16m30s  10GB
Jan 20 06:16:37 Starting translator/monadic/examples
Jan 20 06:19:51 Finished translator/monadic/examples                           3m14s   2GB
Jan 20 06:19:51 Starting examples
Jan 20 06:29:00 Finished examples                                              9m08s   4GB
Jan 20 06:29:00 Starting examples/compilation/x64
Jan 20 08:58:54 Finished examples/compilation/x64                           2h29m51s  16GB
Jan 20 08:58:55 Starting examples/compilation/x64/proofs
Jan 20 09:00:56 Finished examples/compilation/x64/proofs                       2m00s   3GB
Jan 20 09:00:56 Starting examples/compilation/ag32
Jan 20 09:35:14 Finished examples/compilation/ag32                            34m17s   7GB
Jan 20 09:35:14 Starting examples/compilation/ag32/proofs
Jan 20 09:36:00 Finished examples/compilation/ag32/proofs                        46s   3GB
Jan 20 09:36:00 Starting examples/cost
Jan 20 10:30:47 Finished examples/cost                                        54m45s   9GB
Jan 20 10:30:47 Starting examples/lpr_checker
Jan 20 10:31:34 Finished examples/lpr_checker                                    47s 983MB
Jan 20 10:31:34 Starting examples/lpr_checker/array
Jan 20 10:59:51 Finished examples/lpr_checker/array                           28m17s   6GB
Jan 20 10:59:51 Starting examples/lpr_checker/array/compilation
Jan 20 12:23:57 Finished examples/lpr_checker/array/compilation             1h24m05s  25GB
Jan 20 12:23:58 Starting examples/lpr_checker/array/compilation/proofs
Jan 20 12:25:13 Finished examples/lpr_checker/array/compilation/proofs         1m15s   6GB
Jan 20 12:25:13 Starting examples/opentheory
Jan 20 12:34:57 Finished examples/opentheory                                   9m44s   5GB
Jan 20 12:34:57 Starting examples/opentheory
Jan 20 12:34:59 Finished examples/opentheory                                      1s 139MB
Jan 20 12:34:59 Starting examples/opentheory/compilation
Jan 20 13:14:00 Finished examples/opentheory/compilation                      39m01s  27GB
Jan 20 13:14:00 Starting examples/opentheory/compilation/proofs
Jan 20 13:14:47 Finished examples/opentheory/compilation/proofs                  46s   3GB
Jan 20 13:14:47 Starting examples/opentheory/compilation/ag32
Jan 20 13:52:32 Finished examples/opentheory/compilation/ag32                 37m43s  30GB
Jan 20 13:52:32 Starting examples/opentheory/compilation/ag32/proofs
Jan 20 13:54:29 Finished examples/opentheory/compilation/ag32/proofs           1m57s   6GB
Jan 20 13:54:29 Starting examples/sat_encodings
Jan 20 13:56:16 Finished examples/sat_encodings                                1m47s 828MB
Jan 20 13:56:17 Starting examples/sat_encodings/case_studies
Jan 20 13:57:50 Finished examples/sat_encodings/case_studies                   1m33s 717MB
Jan 20 13:57:50 Starting examples/sat_encodings/translation
Jan 20 14:03:25 Finished examples/sat_encodings/translation                    5m35s   3GB
Jan 20 14:03:25 Starting examples/sat_encodings/translation/compilation
Jan 20 15:05:05 Finished examples/sat_encodings/translation/compilation     1h01m38s  22GB
Jan 20 15:05:05 Starting translator/okasaki-examples
Jan 20 15:11:13 Finished translator/okasaki-examples                           6m08s   1GB
Jan 20 15:11:13 Starting translator/other-examples
Jan 20 15:13:46 Finished translator/other-examples                             2m32s   1GB
Jan 20 15:13:46 Starting compiler/parsing/tests
Jan 20 15:14:22 Finished compiler/parsing/tests                                  35s 587MB
Jan 20 15:14:22 Starting compiler/inference/tests
Jan 20 15:23:44 Finished compiler/inference/tests                              9m21s   6GB
Jan 20 15:23:44 Starting compiler/bootstrap/translation
Jan 20 18:05:09 Finished compiler/bootstrap/translation                     2h41m24s  16GB
Jan 20 18:05:09 Starting unverified/sexpr-bootstrap/x64/64
Jan 20 18:15:29 Finished unverified/sexpr-bootstrap/x64/64                    10m19s   8GB
Jan 20 18:15:29 Starting unverified/sexpr-bootstrap/x64/32
Jan 20 18:24:49 Finished unverified/sexpr-bootstrap/x64/32                     9m19s   8GB
Jan 20 18:24:49 Starting compiler/benchmarks
Jan 20 18:25:46 Finished compiler/benchmarks                                     56s 674MB
Jan 20 18:25:47 Starting compiler/bootstrap/compilation/x64/64
Jan 21 07:28:23 Finished compiler/bootstrap/compilation/x64/64             13h02m31s  64GB
Jan 21 07:28:23 Starting compiler/bootstrap/compilation/x64/64/proofs
Jan 21 07:31:04 Finished compiler/bootstrap/compilation/x64/64/proofs          2m40s  19GB
Jan 21 07:31:04 Starting compiler/bootstrap/compilation/x64/32
Jan 21 18:45:01 Finished compiler/bootstrap/compilation/x64/32             11h13m55s  64GB
Jan 21 18:45:01 Starting compiler/bootstrap/compilation/x64/32/proofs
Jan 21 18:47:58 Finished compiler/bootstrap/compilation/x64/32/proofs          2m57s  11GB
Jan 21 18:47:58 Starting compiler/bootstrap/compilation/ag32/32
Jan 22 05:54:55 Finished compiler/bootstrap/compilation/ag32/32            11h06m53s  64GB
Jan 22 05:54:56 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jan 22 06:13:21 Finished compiler/bootstrap/compilation/ag32/32/proofs        18m25s  19GB
Jan 22 06:13:22 SUCCESS