Job 2440

CakeML:c03b0f4110b1846ada0d2ba523e9c1e363817906
  fix a broken proof in data_to_word_memoryProof [Jul 03 14:07:01]
HOL:a0047680ef60f5bf44fe05190b5dcf8756ab4a73
  Get help/src-sml to build again after 7c55b699b9714 [Jul 02 04:04:45]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux
Artefacts:cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz
cake-x64-32.tar.gz

Jul 03 23:11:25 Claimed job
Jul 03 23:11:26 Reusing HOL
Jul 03 23:12:10 Starting developers
Jul 03 23:12:16 Finished developers                                               5s 147MB
Jul 03 23:12:16 Starting developers/bin
Jul 03 23:12:22 Finished developers/bin                                           5s   1GB
Jul 03 23:12:22 Starting compiler/proofs
Jul 04 01:14:51 Finished compiler/proofs                                    2h02m28s  26GB
Jul 04 01:14:51 Starting compiler/bootstrap/translation
Jul 04 09:42:04 Finished compiler/bootstrap/translation                     8h27m12s  35GB
Jul 04 09:42:04 Starting semantics/ffi
Jul 04 09:42:09 Finished semantics/ffi                                            5s 375MB
Jul 04 09:42:09 Starting semantics
Jul 04 09:42:11 Finished semantics                                                1s  19MB
Jul 04 09:42:11 Starting semantics/proofs
Jul 04 09:42:45 Finished semantics/proofs                                        33s 938MB
Jul 04 09:42:45 Starting semantics/alt_semantics
Jul 04 09:43:17 Finished semantics/alt_semantics                                 32s 862MB
Jul 04 09:43:17 Starting semantics/alt_semantics/proofs
Jul 04 09:55:17 Finished semantics/alt_semantics/proofs                       11m59s   1GB
Jul 04 09:55:17 Starting basis/pure
Jul 04 09:55:19 Finished basis/pure                                               1s  19MB
Jul 04 09:55:19 Starting translator
Jul 04 09:57:09 Finished translator                                            1m49s   2GB
Jul 04 09:57:09 Starting compiler/parsing
Jul 04 09:57:11 Finished compiler/parsing                                         1s  22MB
Jul 04 09:57:11 Starting characteristic
Jul 04 09:57:13 Finished characteristic                                           1s  27MB
Jul 04 09:57:13 Starting translator/monadic
Jul 04 09:57:15 Finished translator/monadic                                       1s  20MB
Jul 04 09:57:15 Starting basis
Jul 04 10:00:54 Finished basis                                                 3m38s   3GB
Jul 04 10:00:54 Starting compiler/inference
Jul 04 10:00:56 Finished compiler/inference                                       1s  21MB
Jul 04 10:00:56 Starting compiler/backend/reg_alloc
Jul 04 10:00:57 Finished compiler/backend/reg_alloc                               1s  22MB
Jul 04 10:00:57 Starting compiler/backend/gc
Jul 04 10:01:00 Finished compiler/backend/gc                                      2s  31MB
Jul 04 10:01:00 Starting compiler/backend
Jul 04 10:01:14 Finished compiler/backend                                        13s 839MB
Jul 04 10:01:14 Starting compiler/encoders/asm
Jul 04 10:01:16 Finished compiler/encoders/asm                                    1s  24MB
Jul 04 10:01:16 Starting compiler/encoders/x64
Jul 04 10:01:18 Finished compiler/encoders/x64                                    1s  20MB
Jul 04 10:01:18 Starting compiler/encoders/arm7
Jul 04 10:01:20 Finished compiler/encoders/arm7                                   1s  21MB
Jul 04 10:01:20 Starting compiler/encoders/arm8
Jul 04 10:01:22 Finished compiler/encoders/arm8                                   1s  20MB
Jul 04 10:01:22 Starting compiler/encoders/arm8_asl
Jul 04 12:35:03 Finished compiler/encoders/arm8_asl                         2h33m40s  40GB
Jul 04 12:35:03 Starting compiler/encoders/mips
Jul 04 12:35:05 Finished compiler/encoders/mips                                   1s  23MB
Jul 04 12:35:05 Starting compiler/encoders/riscv
Jul 04 12:35:07 Finished compiler/encoders/riscv                                  1s  26MB
Jul 04 12:35:07 Starting compiler/encoders/ag32
Jul 04 12:35:09 Finished compiler/encoders/ag32                                   1s  21MB
Jul 04 12:35:09 Starting compiler/backend/x64
Jul 04 12:35:12 Finished compiler/backend/x64                                     2s  32MB
Jul 04 12:35:12 Starting compiler/backend/arm7
Jul 04 12:35:14 Finished compiler/backend/arm7                                    2s  26MB
Jul 04 12:35:14 Starting compiler/backend/arm8
Jul 04 12:35:17 Finished compiler/backend/arm8                                    2s  23MB
Jul 04 12:35:17 Starting compiler/backend/mips
Jul 04 12:35:19 Finished compiler/backend/mips                                    2s  23MB
Jul 04 12:35:19 Starting compiler/backend/riscv
Jul 04 12:35:22 Finished compiler/backend/riscv                                   2s  23MB
Jul 04 12:35:22 Starting compiler/backend/ag32
Jul 04 12:36:49 Finished compiler/backend/ag32                                 1m26s   1GB
Jul 04 12:36:49 Starting compiler/parsing/proofs
Jul 04 12:36:51 Finished compiler/parsing/proofs                                  1s  23MB
Jul 04 12:36:51 Starting compiler/inference/proofs
Jul 04 12:36:53 Finished compiler/inference/proofs                                1s  23MB
Jul 04 12:36:53 Starting compiler/backend/semantics
Jul 04 12:40:45 Finished compiler/backend/semantics                            3m51s   2GB
Jul 04 12:40:45 Starting compiler/backend/reg_alloc/proofs
Jul 04 12:40:47 Finished compiler/backend/reg_alloc/proofs                        1s  19MB
Jul 04 12:40:47 Starting compiler/backend/proofs
Jul 04 12:41:50 Finished compiler/backend/proofs                               1m02s   3GB
Jul 04 12:41:50 Starting compiler/backend/serialiser
Jul 04 12:41:52 Finished compiler/backend/serialiser                              2s  27MB
Jul 04 12:41:52 Starting compiler/encoders/x64/proofs
Jul 04 12:51:46 Finished compiler/encoders/x64/proofs                          9m53s   4GB
Jul 04 12:51:46 Starting compiler/encoders/arm7/proofs
Jul 04 13:05:29 Finished compiler/encoders/arm7/proofs                        13m43s   4GB
Jul 04 13:05:30 Starting compiler/encoders/arm8/proofs
Jul 04 13:12:27 Finished compiler/encoders/arm8/proofs                         6m57s   1GB
Jul 04 13:12:27 Starting compiler/encoders/arm8_asl/proofs
Jul 04 14:05:47 Finished compiler/encoders/arm8_asl/proofs                    53m19s   7GB
Jul 04 14:05:47 Starting compiler/encoders/mips/proofs
Jul 04 14:16:16 Finished compiler/encoders/mips/proofs                        10m29s   3GB
Jul 04 14:16:16 Starting compiler/encoders/riscv/proofs
Jul 04 14:25:09 Finished compiler/encoders/riscv/proofs                        8m52s   2GB
Jul 04 14:25:09 Starting compiler/encoders/ag32/proofs
Jul 04 14:27:43 Finished compiler/encoders/ag32/proofs                         2m34s   1GB
Jul 04 14:27:43 Starting compiler/backend/x64/proofs
Jul 04 14:28:16 Finished compiler/backend/x64/proofs                             33s   1GB
Jul 04 14:28:17 Starting compiler/backend/arm7/proofs
Jul 04 14:28:53 Finished compiler/backend/arm7/proofs                            36s   2GB
Jul 04 14:28:53 Starting compiler/backend/arm8/proofs
Jul 04 14:29:26 Finished compiler/backend/arm8/proofs                            32s   1GB
Jul 04 14:29:26 Starting compiler/backend/arm8_asl
Jul 04 14:29:51 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 04 14:29:51 Starting compiler/backend/mips/proofs
Jul 04 14:30:27 Finished compiler/backend/mips/proofs                            36s   2GB
Jul 04 14:30:27 Starting compiler/backend/riscv/proofs
Jul 04 14:31:05 Finished compiler/backend/riscv/proofs                           37s   2GB
Jul 04 14:31:05 Starting compiler/backend/ag32/proofs
Jul 04 14:45:49 Finished compiler/backend/ag32/proofs                         14m43s   2GB
Jul 04 14:45:49 Starting compiler/backend/cv_compute
Jul 04 14:47:09 Finished compiler/backend/cv_compute                           1m20s   2GB
Jul 04 14:47:10 Starting cv_translator
Jul 04 15:07:44 Finished cv_translator                                        20m34s   8GB
Jul 04 15:07:44 Starting candle/set-theory
Jul 04 15:08:29 Finished candle/set-theory                                       44s   1GB
Jul 04 15:08:29 Starting candle/syntax-lib
Jul 04 15:08:31 Finished candle/syntax-lib                                        1s  18MB
Jul 04 15:08:31 Starting candle/standard/syntax
Jul 04 15:08:43 Finished candle/standard/syntax                                  12s 793MB
Jul 04 15:08:44 Starting candle/standard/semantics
Jul 04 15:10:53 Finished candle/standard/semantics                             2m09s   1GB
Jul 04 15:10:53 Starting candle/standard/monadic
Jul 04 15:10:55 Finished candle/standard/monadic                                  1s  23MB
Jul 04 15:10:55 Starting candle/standard/ml_kernel
Jul 04 15:12:44 Finished candle/standard/ml_kernel                             1m48s   3GB
Jul 04 15:12:44 Starting candle/overloading/syntax
Jul 04 15:16:19 Finished candle/overloading/syntax                             3m34s   1GB
Jul 04 15:16:19 Starting candle/overloading/semantics
Jul 04 15:28:46 Finished candle/overloading/semantics                         12m27s   2GB
Jul 04 15:28:46 Starting candle/overloading/monadic
Jul 04 15:31:36 Finished candle/overloading/monadic                            2m49s   1GB
Jul 04 15:31:36 Starting candle/overloading/ml_kernel
Jul 04 15:39:43 Finished candle/overloading/ml_kernel                          8m07s   5GB
Jul 04 15:39:43 Starting candle/overloading/ml_checker
Jul 04 15:42:24 Finished candle/overloading/ml_checker                         2m40s   2GB
Jul 04 15:42:24 Starting candle/prover
Jul 04 15:52:40 Finished candle/prover                                        10m16s   3GB
Jul 04 15:52:40 Starting pancake
Jul 04 15:53:30 Finished pancake                                                 49s 920MB
Jul 04 15:53:30 Starting pancake/ffi
Jul 04 15:53:31 Finished pancake/ffi                                              0s  13MB
Jul 04 15:53:31 Starting pancake/semantics
Jul 04 15:56:32 Finished pancake/semantics                                     3m00s   1GB
Jul 04 15:56:32 Starting pancake/parser
Jul 04 15:57:02 Finished pancake/parser                                          30s   1GB
Jul 04 15:57:03 Starting pancake/proofs
Jul 04 16:32:19 Finished pancake/proofs                                       35m16s   4GB
Jul 04 16:32:19 Starting characteristic/examples
Jul 04 16:33:56 Finished characteristic/examples                               1m36s   3GB
Jul 04 16:33:56 Starting tutorial/solutions
Jul 04 16:36:34 Finished tutorial/solutions                                    2m37s   3GB
Jul 04 16:36:34 Starting translator/monadic/examples
Jul 04 16:40:55 Finished translator/monadic/examples                           4m21s   3GB
Jul 04 16:40:55 Starting examples
Jul 04 16:57:19 Finished examples                                             16m23s   5GB
Jul 04 16:57:19 Starting examples/compilation/x64
Jul 04 17:06:02 Finished examples/compilation/x64                              8m43s   5GB
Jul 04 17:06:02 Starting examples/compilation/x64/proofs
Jul 04 17:08:59 Finished examples/compilation/x64/proofs                       2m56s   4GB
Jul 04 17:08:59 Starting examples/compilation/ag32
Jul 04 17:11:06 Finished examples/compilation/ag32                             2m06s   3GB
Jul 04 17:11:06 Starting examples/compilation/ag32/proofs
Jul 04 17:12:20 Finished examples/compilation/ag32/proofs                      1m13s   5GB
Jul 04 17:12:20 Starting examples/compilation/to_word
Jul 04 17:16:00 Finished examples/compilation/to_word                          3m40s   7GB
Jul 04 17:16:01 Starting examples/lpr_checker
Jul 04 17:17:12 Finished examples/lpr_checker                                  1m11s   1GB
Jul 04 17:17:13 Starting examples/lpr_checker/array
Jul 04 17:47:30 Finished examples/lpr_checker/array                           30m17s   7GB
Jul 04 17:47:30 Starting examples/lpr_checker/array/compilation
Jul 04 17:50:13 Finished examples/lpr_checker/array/compilation                2m42s   7GB
Jul 04 17:50:13 Starting examples/lpr_checker/array/compilation/proofs
Jul 04 17:51:38 Finished examples/lpr_checker/array/compilation/proofs         1m24s   6GB
Jul 04 17:51:38 Starting examples/lpr_checker/array/compilation/proofsARM8
Jul 04 17:52:52 Finished examples/lpr_checker/array/compilation/proofsARM8     1m14s   6GB
Jul 04 17:52:53 Starting examples/xlrup_checker
Jul 04 17:53:58 Finished examples/xlrup_checker                                1m05s 982MB
Jul 04 17:53:58 Starting examples/xlrup_checker/array
Jul 04 18:10:08 Finished examples/xlrup_checker/array                         16m09s   3GB
Jul 04 18:10:08 Starting examples/xlrup_checker/array/compilation
Jul 04 18:11:33 Finished examples/xlrup_checker/array/compilation              1m24s   4GB
Jul 04 18:11:33 Starting examples/xlrup_checker/array/compilation/proofs
Jul 04 18:12:41 Finished examples/xlrup_checker/array/compilation/proofs       1m08s   5GB
Jul 04 18:12:41 Starting examples/pseudo_bool
Jul 04 18:14:43 Finished examples/pseudo_bool                                  2m02s   1GB
Jul 04 18:14:43 Starting examples/pseudo_bool/cnf_encoding
Jul 04 18:15:13 Finished examples/pseudo_bool/cnf_encoding                       29s   1GB
Jul 04 18:15:13 Starting examples/pseudo_bool/graph_encoding
Jul 04 18:16:00 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Jul 04 18:16:00 Starting examples/pseudo_bool/array
Jul 04 19:25:55 Finished examples/pseudo_bool/array                         1h09m54s   8GB
Jul 04 19:25:55 Starting examples/pseudo_bool/array/compilation
Jul 04 19:40:34 Finished examples/pseudo_bool/array/compilation               14m38s  26GB
Jul 04 19:40:34 Starting examples/pseudo_bool/array/compilation/proofs
Jul 04 19:43:31 Finished examples/pseudo_bool/array/compilation/proofs         2m56s   7GB
Jul 04 19:43:31 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jul 04 19:44:54 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m23s   6GB
Jul 04 19:44:55 Starting examples/opentheory
Jul 04 19:55:59 Finished examples/opentheory                                  11m04s   4GB
Jul 04 19:56:00 Starting examples/opentheory
Jul 04 19:56:02 Finished examples/opentheory                                      1s  28MB
Jul 04 19:56:02 Starting examples/opentheory/compilation
Jul 04 19:58:05 Finished examples/opentheory/compilation                       2m02s   6GB
Jul 04 19:58:05 Starting examples/opentheory/compilation/proofs
Jul 04 19:59:15 Finished examples/opentheory/compilation/proofs                1m09s   5GB
Jul 04 19:59:15 Starting examples/opentheory/compilation/ag32
Jul 04 20:01:18 Finished examples/opentheory/compilation/ag32                  2m02s   6GB
Jul 04 20:01:18 Starting examples/opentheory/compilation/ag32/proofs
Jul 04 20:03:02 Finished examples/opentheory/compilation/ag32/proofs           1m43s   5GB
Jul 04 20:03:02 Starting examples/sat_encodings
Jul 04 20:05:20 Finished examples/sat_encodings                                2m18s   1GB
Jul 04 20:05:20 Starting examples/sat_encodings/case_studies
Jul 04 20:07:19 Finished examples/sat_encodings/case_studies                   1m59s   1GB
Jul 04 20:07:19 Starting examples/sat_encodings/translation
Jul 04 20:13:57 Finished examples/sat_encodings/translation                    6m37s   4GB
Jul 04 20:13:57 Starting examples/sat_encodings/translation/compilation
Jul 04 20:16:21 Finished examples/sat_encodings/translation/compilation        2m23s   5GB
Jul 04 20:16:21 Starting examples/deflate
Jul 04 20:17:31 Finished examples/deflate                                      1m09s   1GB
Jul 04 20:17:31 Starting examples/deflate/translation
Jul 04 20:19:20 Finished examples/deflate/translation                          1m48s   3GB
Jul 04 20:19:20 Starting examples/deflate/translation/compilation
Jul 04 20:20:27 Finished examples/deflate/translation/compilation              1m07s   4GB
Jul 04 20:20:27 Starting examples/vipr
Jul 04 20:24:42 Finished examples/vipr                                         4m14s   3GB
Jul 04 20:24:42 Starting examples/vipr/compilation
Jul 04 20:25:58 Finished examples/vipr/compilation                             1m15s   4GB
Jul 04 20:25:58 Starting translator/okasaki-examples
Jul 04 20:31:24 Finished translator/okasaki-examples                           5m26s   2GB
Jul 04 20:31:24 Starting translator/other-examples
Jul 04 20:35:07 Finished translator/other-examples                             3m43s   2GB
Jul 04 20:35:08 Starting compiler/parsing/tests
Jul 04 20:35:42 Finished compiler/parsing/tests                                  34s 820MB
Jul 04 20:35:42 Starting compiler/inference/tests
Jul 04 20:36:13 Finished compiler/inference/tests                                30s   1GB
Jul 04 20:36:13 Starting compiler/printing/test
Jul 04 20:37:42 Finished compiler/printing/test                                1m29s   2GB
Jul 04 20:37:42 Starting icing/flover
Jul 04 21:24:06 Finished icing/flover                                         46m23s   2GB
Jul 04 21:24:06 Starting icing/
Jul 04 21:53:31 Finished icing/                                               29m24s   4GB
Jul 04 21:53:31 Starting icing/examples
Jul 04 21:55:09 Finished icing/examples                                        1m37s   5GB
Jul 04 21:55:09 Starting compiler/repl
Jul 04 22:04:01 Finished compiler/repl                                         8m51s   6GB
Jul 04 22:04:01 Starting unverified/sexpr-bootstrap/x64/64
Jul 04 22:18:48 Finished unverified/sexpr-bootstrap/x64/64                    14m46s  17GB
Jul 04 22:18:48 Starting unverified/sexpr-bootstrap/x64/32
Jul 04 22:30:27 Finished unverified/sexpr-bootstrap/x64/32                    11m37s  15GB
Jul 04 22:30:27 Starting compiler/benchmarks
Jul 04 22:46:10 Finished compiler/benchmarks                                  15m43s   2GB
Jul 04 22:46:10 Starting compiler/bootstrap/compilation/x64/64
Jul 04 23:43:14 Finished compiler/bootstrap/compilation/x64/64                57m03s  63GB
Jul 04 23:43:15 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 05 00:05:13 Finished compiler/bootstrap/compilation/x64/64/proofs         21m58s  45GB
Jul 05 00:05:13 Starting compiler/bootstrap/compilation/x64/32
Jul 05 00:40:23 Finished compiler/bootstrap/compilation/x64/32                35m09s  64GB
Jul 05 00:40:23 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 05 00:46:01 Finished compiler/bootstrap/compilation/x64/32/proofs          5m37s  18GB
Jul 05 00:46:01 Starting compiler/bootstrap/compilation/ag32/32
Jul 05 01:23:17 Finished compiler/bootstrap/compilation/ag32/32               37m15s  63GB
Jul 05 01:23:17 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jul 05 01:30:29 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m11s  20GB
Jul 05 01:30:29 SUCCESS