Job 2160

CakeML:adc733eac3cce0b29c0005fde1f7111638ee6cd7
  Fix a proof broken by changes in HOL master [Jul 04 03:47:29]
HOL:39d587ce28156b9b533d088a721d072e3271ddfb
  Fix another proof broken by automatic {DIV,MOD}_0 [Jul 03 07:06:39]
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

Jul 05 02:13:42 Claimed job
Jul 05 02:13:48 Building HOL
Jul 05 02:26:13 Starting developers
Jul 05 02:26:18 Finished developers                                               5s 105MB
Jul 05 02:26:19 Starting developers/bin
Jul 05 02:26:24 Finished developers/bin                                           5s   1GB
Jul 05 02:26:25 Starting compiler/proofs
Jul 05 04:19:41 Finished compiler/proofs                                    1h53m15s  16GB
Jul 05 04:19:42 Starting compiler/bootstrap/translation
Jul 05 12:24:46 Finished compiler/bootstrap/translation                     8h05m03s  43GB
Jul 05 12:24:46 Starting semantics/ffi
Jul 05 12:24:52 Finished semantics/ffi                                            5s 219MB
Jul 05 12:24:52 Starting semantics
Jul 05 12:24:54 Finished semantics                                                1s  19MB
Jul 05 12:24:54 Starting semantics/proofs
Jul 05 12:25:26 Finished semantics/proofs                                        32s 735MB
Jul 05 12:25:27 Starting semantics/alt_semantics
Jul 05 12:25:58 Finished semantics/alt_semantics                                 31s 707MB
Jul 05 12:25:58 Starting semantics/alt_semantics/proofs
Jul 05 12:37:55 Finished semantics/alt_semantics/proofs                       11m56s   1GB
Jul 05 12:37:55 Starting basis/pure
Jul 05 12:37:57 Finished basis/pure                                               1s  20MB
Jul 05 12:37:57 Starting translator
Jul 05 12:39:46 Finished translator                                            1m49s   1GB
Jul 05 12:39:46 Starting compiler/parsing
Jul 05 12:39:48 Finished compiler/parsing                                         1s  18MB
Jul 05 12:39:48 Starting characteristic
Jul 05 12:39:50 Finished characteristic                                           1s  23MB
Jul 05 12:39:50 Starting translator/monadic
Jul 05 12:39:52 Finished translator/monadic                                       1s  23MB
Jul 05 12:39:52 Starting basis
Jul 05 12:43:55 Finished basis                                                 4m03s   2GB
Jul 05 12:43:56 Starting compiler/inference
Jul 05 12:43:57 Finished compiler/inference                                       1s  24MB
Jul 05 12:43:57 Starting compiler/backend/reg_alloc
Jul 05 12:43:59 Finished compiler/backend/reg_alloc                               1s  27MB
Jul 05 12:43:59 Starting compiler/backend/gc
Jul 05 12:44:01 Finished compiler/backend/gc                                      2s  24MB
Jul 05 12:44:02 Starting compiler/backend
Jul 05 12:44:14 Finished compiler/backend                                        12s 842MB
Jul 05 12:44:14 Starting compiler/encoders/asm
Jul 05 12:44:16 Finished compiler/encoders/asm                                    1s  23MB
Jul 05 12:44:16 Starting compiler/encoders/x64
Jul 05 12:44:18 Finished compiler/encoders/x64                                    1s  22MB
Jul 05 12:44:18 Starting compiler/encoders/arm7
Jul 05 12:44:20 Finished compiler/encoders/arm7                                   1s  22MB
Jul 05 12:44:20 Starting compiler/encoders/arm8
Jul 05 12:44:22 Finished compiler/encoders/arm8                                   1s  21MB
Jul 05 12:44:22 Starting compiler/encoders/arm8_asl
Jul 05 15:18:57 Finished compiler/encoders/arm8_asl                         2h34m31s  45GB
Jul 05 15:18:57 Starting compiler/encoders/mips
Jul 05 15:18:59 Finished compiler/encoders/mips                                   1s  26MB
Jul 05 15:18:59 Starting compiler/encoders/riscv
Jul 05 15:19:01 Finished compiler/encoders/riscv                                  1s  23MB
Jul 05 15:19:01 Starting compiler/encoders/ag32
Jul 05 15:19:03 Finished compiler/encoders/ag32                                   1s  23MB
Jul 05 15:19:03 Starting compiler/backend/x64
Jul 05 15:19:05 Finished compiler/backend/x64                                     2s  37MB
Jul 05 15:19:05 Starting compiler/backend/arm7
Jul 05 15:19:08 Finished compiler/backend/arm7                                    2s  25MB
Jul 05 15:19:08 Starting compiler/backend/arm8
Jul 05 15:19:10 Finished compiler/backend/arm8                                    2s  37MB
Jul 05 15:19:10 Starting compiler/backend/mips
Jul 05 15:19:12 Finished compiler/backend/mips                                    2s  35MB
Jul 05 15:19:12 Starting compiler/backend/riscv
Jul 05 15:19:15 Finished compiler/backend/riscv                                   2s  28MB
Jul 05 15:19:15 Starting compiler/backend/ag32
Jul 05 15:21:01 Finished compiler/backend/ag32                                 1m45s   1GB
Jul 05 15:21:01 Starting compiler/parsing/proofs
Jul 05 15:21:02 Finished compiler/parsing/proofs                                  1s  19MB
Jul 05 15:21:03 Starting compiler/inference/proofs
Jul 05 15:21:04 Finished compiler/inference/proofs                                1s  24MB
Jul 05 15:21:05 Starting compiler/backend/semantics
Jul 05 15:22:34 Finished compiler/backend/semantics                            1m29s   1GB
Jul 05 15:22:34 Starting compiler/backend/reg_alloc/proofs
Jul 05 15:22:36 Finished compiler/backend/reg_alloc/proofs                        1s  24MB
Jul 05 15:22:36 Starting compiler/backend/proofs
Jul 05 15:23:46 Finished compiler/backend/proofs                               1m09s   2GB
Jul 05 15:23:46 Starting compiler/backend/serialiser
Jul 05 15:23:50 Finished compiler/backend/serialiser                              3s  47MB
Jul 05 15:23:50 Starting compiler/encoders/x64/proofs
Jul 05 15:35:45 Finished compiler/encoders/x64/proofs                         11m54s   6GB
Jul 05 15:35:45 Starting compiler/encoders/arm7/proofs
Jul 05 15:52:28 Finished compiler/encoders/arm7/proofs                        16m43s   3GB
Jul 05 15:52:28 Starting compiler/encoders/arm8/proofs
Jul 05 15:59:48 Finished compiler/encoders/arm8/proofs                         7m19s   1GB
Jul 05 15:59:48 Starting compiler/encoders/arm8_asl/proofs
Jul 05 16:54:40 Finished compiler/encoders/arm8_asl/proofs                    54m51s   6GB
Jul 05 16:54:40 Starting compiler/encoders/mips/proofs
Jul 05 17:05:38 Finished compiler/encoders/mips/proofs                        10m57s   2GB
Jul 05 17:05:38 Starting compiler/encoders/riscv/proofs
Jul 05 17:14:56 Finished compiler/encoders/riscv/proofs                        9m17s   1GB
Jul 05 17:14:56 Starting compiler/encoders/ag32/proofs
Jul 05 17:17:47 Finished compiler/encoders/ag32/proofs                         2m51s 572MB
Jul 05 17:17:47 Starting compiler/backend/x64/proofs
Jul 05 17:18:18 Finished compiler/backend/x64/proofs                             31s   2GB
Jul 05 17:18:18 Starting compiler/backend/arm7/proofs
Jul 05 17:18:56 Finished compiler/backend/arm7/proofs                            37s   1GB
Jul 05 17:18:56 Starting compiler/backend/arm8/proofs
Jul 05 17:19:30 Finished compiler/backend/arm8/proofs                            33s   1GB
Jul 05 17:19:30 Starting compiler/backend/arm8_asl
Jul 05 17:19:54 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 05 17:19:55 Starting compiler/backend/mips/proofs
Jul 05 17:20:30 Finished compiler/backend/mips/proofs                            35s   2GB
Jul 05 17:20:30 Starting compiler/backend/riscv/proofs
Jul 05 17:21:05 Finished compiler/backend/riscv/proofs                           35s   2GB
Jul 05 17:21:05 Starting compiler/backend/ag32/proofs
Jul 05 17:35:00 Finished compiler/backend/ag32/proofs                         13m54s   2GB
Jul 05 17:35:00 Starting candle/set-theory
Jul 05 17:35:41 Finished candle/set-theory                                       40s   1GB
Jul 05 17:35:41 Starting candle/syntax-lib
Jul 05 17:35:43 Finished candle/syntax-lib                                        1s  18MB
Jul 05 17:35:43 Starting candle/standard/syntax
Jul 05 17:35:54 Finished candle/standard/syntax                                  10s 812MB
Jul 05 17:35:54 Starting candle/standard/semantics
Jul 05 17:37:56 Finished candle/standard/semantics                             2m01s   1GB
Jul 05 17:37:56 Starting candle/standard/monadic
Jul 05 17:37:58 Finished candle/standard/monadic                                  1s  27MB
Jul 05 17:37:58 Starting candle/standard/ml_kernel
Jul 05 17:39:37 Finished candle/standard/ml_kernel                             1m38s   3GB
Jul 05 17:39:37 Starting candle/overloading/syntax
Jul 05 17:43:02 Finished candle/overloading/syntax                             3m24s   1GB
Jul 05 17:43:02 Starting candle/overloading/semantics
Jul 05 17:55:21 Finished candle/overloading/semantics                         12m17s   2GB
Jul 05 17:55:21 Starting candle/overloading/monadic
Jul 05 17:58:02 Finished candle/overloading/monadic                            2m40s   2GB
Jul 05 17:58:02 Starting candle/overloading/ml_kernel
Jul 05 18:05:59 Finished candle/overloading/ml_kernel                          7m56s   3GB
Jul 05 18:05:59 Starting candle/overloading/ml_checker
Jul 05 18:08:34 Finished candle/overloading/ml_checker                         2m33s   2GB
Jul 05 18:08:34 Starting candle/prover
Jul 05 18:18:40 Finished candle/prover                                        10m06s   3GB
Jul 05 18:18:40 Starting pancake
Jul 05 18:19:25 Finished pancake                                                 44s   1GB
Jul 05 18:19:25 Starting pancake/ffi
Jul 05 18:19:26 Finished pancake/ffi                                              0s  13MB
Jul 05 18:19:26 Starting pancake/semantics
Jul 05 18:21:56 Finished pancake/semantics                                     2m30s   1GB
Jul 05 18:21:57 Starting pancake/proofs
Jul 05 18:41:04 Finished pancake/proofs                                       19m07s   4GB
Jul 05 18:41:05 Starting characteristic/examples
Jul 05 18:42:50 Finished characteristic/examples                               1m45s   3GB
Jul 05 18:42:50 Starting tutorial/solutions
Jul 05 18:58:16 Finished tutorial/solutions                                   15m24s   8GB
Jul 05 18:58:16 Starting translator/monadic/examples
Jul 05 19:02:20 Finished translator/monadic/examples                           4m04s   3GB
Jul 05 19:02:20 Starting examples
Jul 05 19:19:13 Finished examples                                             16m52s   4GB
Jul 05 19:19:13 Starting examples/compilation/x64
Jul 05 21:20:30 Finished examples/compilation/x64                           2h01m13s  14GB
Jul 05 21:20:30 Starting examples/compilation/x64/proofs
Jul 05 21:23:55 Finished examples/compilation/x64/proofs                       3m24s   4GB
Jul 05 21:23:55 Starting examples/compilation/ag32
Jul 05 21:58:31 Finished examples/compilation/ag32                            34m36s   7GB
Jul 05 21:58:31 Starting examples/compilation/ag32/proofs
Jul 05 21:59:41 Finished examples/compilation/ag32/proofs                      1m09s   3GB
Jul 05 21:59:41 Starting examples/compilation/to_word
Jul 05 22:03:15 Finished examples/compilation/to_word                          3m34s   7GB
Jul 05 22:03:15 Starting examples/lpr_checker
Jul 05 22:04:27 Finished examples/lpr_checker                                  1m11s   1GB
Jul 05 22:04:27 Starting examples/lpr_checker/array
Jul 05 23:00:29 Finished examples/lpr_checker/array                           56m00s   5GB
Jul 05 23:00:29 Starting examples/lpr_checker/array/compilation
Jul 06 00:14:26 Finished examples/lpr_checker/array/compilation             1h13m55s  12GB
Jul 06 00:14:26 Starting examples/lpr_checker/array/compilation/proofs
Jul 06 00:16:50 Finished examples/lpr_checker/array/compilation/proofs         2m23s   3GB
Jul 06 00:16:50 Starting examples/opentheory
Jul 06 00:29:30 Finished examples/opentheory                                  12m40s   4GB
Jul 06 00:29:30 Starting examples/opentheory
Jul 06 00:29:33 Finished examples/opentheory                                      2s  26MB
Jul 06 00:29:33 Starting examples/opentheory/compilation
Jul 06 01:14:45 Finished examples/opentheory/compilation                      45m09s  27GB
Jul 06 01:14:46 Starting examples/opentheory/compilation/proofs
Jul 06 01:15:54 Finished examples/opentheory/compilation/proofs                1m08s   4GB
Jul 06 01:15:55 Starting examples/opentheory/compilation/ag32
Jul 06 01:50:35 Finished examples/opentheory/compilation/ag32                 34m39s  23GB
Jul 06 01:50:35 Starting examples/opentheory/compilation/ag32/proofs
Jul 06 01:52:43 Finished examples/opentheory/compilation/ag32/proofs           2m07s   8GB
Jul 06 01:52:43 Starting examples/sat_encodings
Jul 06 01:54:50 Finished examples/sat_encodings                                2m07s 813MB
Jul 06 01:54:50 Starting examples/sat_encodings/case_studies
Jul 06 01:56:39 Finished examples/sat_encodings/case_studies                   1m48s   1GB
Jul 06 01:56:39 Starting examples/sat_encodings/translation
Jul 06 02:03:09 Finished examples/sat_encodings/translation                    6m30s   4GB
Jul 06 02:03:10 Starting examples/sat_encodings/translation/compilation
Jul 06 02:54:24 Finished examples/sat_encodings/translation/compilation       51m12s  24GB
Jul 06 02:54:24 Starting examples/deflate
Jul 06 02:55:30 Finished examples/deflate                                      1m05s 836MB
Jul 06 02:55:30 Starting examples/deflate/translation
Jul 06 02:57:45 Finished examples/deflate/translation                          2m15s   2GB
Jul 06 02:57:46 Starting examples/deflate/translation/compilation
Jul 06 03:31:01 Finished examples/deflate/translation/compilation             33m15s   4GB
Jul 06 03:31:01 Starting examples/vipr
Jul 06 03:36:45 Finished examples/vipr                                         5m43s   4GB
Jul 06 03:36:45 Starting examples/vipr/compilation
Jul 06 04:01:05 Finished examples/vipr/compilation                            24m17s  15GB
Jul 06 04:01:06 Starting translator/okasaki-examples
Jul 06 04:07:30 Finished translator/okasaki-examples                           6m24s   2GB
Jul 06 04:07:30 Starting translator/other-examples
Jul 06 04:10:27 Finished translator/other-examples                             2m56s   1GB
Jul 06 04:10:27 Starting compiler/parsing/tests
Jul 06 04:11:01 Finished compiler/parsing/tests                                  33s 752MB
Jul 06 04:11:01 Starting compiler/inference/tests
Jul 06 04:19:53 Finished compiler/inference/tests                              8m52s   3GB
Jul 06 04:19:53 Starting compiler/printing/test
Jul 06 04:23:51 Finished compiler/printing/test                                3m58s   3GB
Jul 06 04:23:51 Starting icing/flover
Jul 06 05:07:42 Finished icing/flover                                         43m49s   2GB
Jul 06 05:07:42 Starting icing/
Jul 06 06:02:54 Finished icing/                                               55m12s   8GB
Jul 06 06:02:54 Starting icing/examples
Jul 06 06:04:32 Finished icing/examples                                        1m37s   6GB
Jul 06 06:04:32 Starting compiler/repl
Jul 06 06:13:19 Finished compiler/repl                                         8m45s   6GB
Jul 06 06:13:21 Starting unverified/sexpr-bootstrap/x64/64
Jul 06 06:26:40 Finished unverified/sexpr-bootstrap/x64/64                    13m14s  17GB
Jul 06 06:26:40 Starting unverified/sexpr-bootstrap/x64/32
Jul 06 06:37:21 Finished unverified/sexpr-bootstrap/x64/32                    10m39s  12GB
Jul 06 06:37:21 Starting compiler/benchmarks
Jul 06 06:52:45 Finished compiler/benchmarks                                  15m24s   2GB
Jul 06 06:52:45 Starting compiler/bootstrap/compilation/x64/64
Jul 06 21:02:50 Finished compiler/bootstrap/compilation/x64/64             14h10m00s  64GB
Jul 06 21:02:50 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 06 21:34:02 Finished compiler/bootstrap/compilation/x64/64/proofs         31m11s  14GB
Jul 06 21:34:02 Starting compiler/bootstrap/compilation/x64/32
Jul 07 04:36:56 Finished compiler/bootstrap/compilation/x64/32              7h02m51s  64GB
Jul 07 04:36:56 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 07 04:39:54 Finished compiler/bootstrap/compilation/x64/32/proofs          2m57s  18GB
Jul 07 04:39:54 Starting compiler/bootstrap/compilation/ag32/32
Jul 07 11:48:30 Finished compiler/bootstrap/compilation/ag32/32             7h08m33s  64GB
Jul 07 11:48:30 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 07 11:55:28 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m57s  44GB
Jul 07 11:55:28 SUCCESS