Job 2648

CakeML:b9843ac59b40ad1a8adc0dfdfcd5e0656f44ab6e
  Merge pull request #1064 from CakeML/remove-define [Oct 10 11:32:18]
HOL:277f6ad618617d462cd4ad2955206cb261828f87
  Add proofs about clock for fun-op-sem/imp (#1310) [Oct 03 07:36:31]
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-arm8-64.tar.gz
cake-x64-32.tar.gz

Oct 10 11:34:45 Claimed job
Oct 10 11:34:50 Reusing HOL
Oct 10 11:35:35 Starting developers
Oct 10 11:35:41 Finished developers                                               6s  82MB
Oct 10 11:35:41 Starting developers/bin
Oct 10 11:35:48 Finished developers/bin                                           6s   1GB
Oct 10 11:35:48 Starting compiler/proofs
Oct 10 13:30:52 Finished compiler/proofs                                    1h55m03s  21GB
Oct 10 13:30:52 Starting compiler/bootstrap/translation
Oct 10 22:22:47 Finished compiler/bootstrap/translation                     8h51m54s  38GB
Oct 10 22:22:47 Starting semantics/ffi
Oct 10 22:22:53 Finished semantics/ffi                                            5s 410MB
Oct 10 22:22:53 Starting semantics
Oct 10 22:22:54 Finished semantics                                                1s  21MB
Oct 10 22:22:55 Starting semantics/proofs
Oct 10 22:23:20 Finished semantics/proofs                                        25s 413MB
Oct 10 22:23:20 Starting semantics/alt_semantics
Oct 10 22:23:44 Finished semantics/alt_semantics                                 23s 524MB
Oct 10 22:23:44 Starting semantics/alt_semantics/proofs
Oct 10 22:35:21 Finished semantics/alt_semantics/proofs                       11m37s   2GB
Oct 10 22:35:21 Starting basis/pure
Oct 10 22:35:23 Finished basis/pure                                               1s  18MB
Oct 10 22:35:23 Starting translator
Oct 10 22:37:05 Finished translator                                            1m41s   1GB
Oct 10 22:37:05 Starting compiler/parsing
Oct 10 22:37:06 Finished compiler/parsing                                         1s  18MB
Oct 10 22:37:06 Starting characteristic
Oct 10 22:37:09 Finished characteristic                                           1s  21MB
Oct 10 22:37:09 Starting translator/monadic
Oct 10 22:37:11 Finished translator/monadic                                       1s  22MB
Oct 10 22:37:11 Starting basis
Oct 10 22:39:41 Finished basis                                                 2m30s   2GB
Oct 10 22:39:41 Starting compiler/inference
Oct 10 22:39:43 Finished compiler/inference                                       1s  21MB
Oct 10 22:39:43 Starting compiler/backend/reg_alloc
Oct 10 22:39:44 Finished compiler/backend/reg_alloc                               1s  21MB
Oct 10 22:39:45 Starting compiler/backend/gc
Oct 10 22:39:47 Finished compiler/backend/gc                                      2s  26MB
Oct 10 22:39:47 Starting compiler/backend
Oct 10 22:39:53 Finished compiler/backend                                         5s 268MB
Oct 10 22:39:53 Starting compiler/encoders/asm
Oct 10 22:39:55 Finished compiler/encoders/asm                                    1s  26MB
Oct 10 22:39:55 Starting compiler/encoders/x64
Oct 10 22:39:57 Finished compiler/encoders/x64                                    1s  26MB
Oct 10 22:39:57 Starting compiler/encoders/arm7
Oct 10 22:39:59 Finished compiler/encoders/arm7                                   1s  21MB
Oct 10 22:39:59 Starting compiler/encoders/arm8
Oct 10 22:40:01 Finished compiler/encoders/arm8                                   1s  25MB
Oct 10 22:40:01 Starting compiler/encoders/arm8_asl
Oct 10 22:43:08 Finished compiler/encoders/arm8_asl                            3m06s   1GB
Oct 10 22:43:08 Starting compiler/encoders/mips
Oct 10 22:43:10 Finished compiler/encoders/mips                                   1s  21MB
Oct 10 22:43:10 Starting compiler/encoders/riscv
Oct 10 22:43:11 Finished compiler/encoders/riscv                                  1s  22MB
Oct 10 22:43:12 Starting compiler/encoders/ag32
Oct 10 22:43:13 Finished compiler/encoders/ag32                                   1s  21MB
Oct 10 22:43:13 Starting compiler/backend/x64
Oct 10 22:43:16 Finished compiler/backend/x64                                     2s  30MB
Oct 10 22:43:16 Starting compiler/backend/arm7
Oct 10 22:43:18 Finished compiler/backend/arm7                                    2s  23MB
Oct 10 22:43:18 Starting compiler/backend/arm8
Oct 10 22:43:21 Finished compiler/backend/arm8                                    2s  27MB
Oct 10 22:43:21 Starting compiler/backend/mips
Oct 10 22:43:23 Finished compiler/backend/mips                                    2s  29MB
Oct 10 22:43:23 Starting compiler/backend/riscv
Oct 10 22:43:26 Finished compiler/backend/riscv                                   2s  25MB
Oct 10 22:43:26 Starting compiler/backend/ag32
Oct 10 22:44:38 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 10 22:44:38 Starting compiler/parsing/proofs
Oct 10 22:44:39 Finished compiler/parsing/proofs                                  1s  20MB
Oct 10 22:44:40 Starting compiler/inference/proofs
Oct 10 22:44:41 Finished compiler/inference/proofs                                1s  24MB
Oct 10 22:44:42 Starting compiler/backend/semantics
Oct 10 22:48:13 Finished compiler/backend/semantics                            3m31s   1GB
Oct 10 22:48:13 Starting compiler/backend/reg_alloc/proofs
Oct 10 22:48:15 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Oct 10 22:48:15 Starting compiler/backend/proofs
Oct 10 22:49:10 Finished compiler/backend/proofs                                 54s   2GB
Oct 10 22:49:10 Starting compiler/backend/serialiser
Oct 10 22:49:12 Finished compiler/backend/serialiser                              2s  28MB
Oct 10 22:49:12 Starting compiler/encoders/x64/proofs
Oct 10 22:59:52 Finished compiler/encoders/x64/proofs                         10m39s   5GB
Oct 10 22:59:52 Starting compiler/encoders/arm7/proofs
Oct 10 23:13:54 Finished compiler/encoders/arm7/proofs                        14m01s   4GB
Oct 10 23:13:54 Starting compiler/encoders/arm8/proofs
Oct 10 23:21:30 Finished compiler/encoders/arm8/proofs                         7m35s   1GB
Oct 10 23:21:30 Starting compiler/encoders/arm8_asl/proofs
Oct 10 23:39:18 Finished compiler/encoders/arm8_asl/proofs                    17m47s   1GB
Oct 10 23:39:18 Starting compiler/encoders/mips/proofs
Oct 10 23:50:01 Finished compiler/encoders/mips/proofs                        10m42s   3GB
Oct 10 23:50:01 Starting compiler/encoders/riscv/proofs
Oct 10 23:59:02 Finished compiler/encoders/riscv/proofs                        9m01s   2GB
Oct 10 23:59:02 Starting compiler/encoders/ag32/proofs
Oct 11 00:02:20 Finished compiler/encoders/ag32/proofs                         3m18s   1GB
Oct 11 00:02:20 Starting compiler/backend/x64/proofs
Oct 11 00:02:53 Finished compiler/backend/x64/proofs                             32s   2GB
Oct 11 00:02:53 Starting compiler/backend/arm7/proofs
Oct 11 00:03:27 Finished compiler/backend/arm7/proofs                            33s   1GB
Oct 11 00:03:27 Starting compiler/backend/arm8/proofs
Oct 11 00:04:02 Finished compiler/backend/arm8/proofs                            34s   2GB
Oct 11 00:04:02 Starting compiler/backend/arm8_asl
Oct 11 00:04:26 Finished compiler/backend/arm8_asl                               24s   2GB
Oct 11 00:04:26 Starting compiler/backend/mips/proofs
Oct 11 00:05:00 Finished compiler/backend/mips/proofs                            33s   2GB
Oct 11 00:05:00 Starting compiler/backend/riscv/proofs
Oct 11 00:05:38 Finished compiler/backend/riscv/proofs                           37s   2GB
Oct 11 00:05:38 Starting compiler/backend/ag32/proofs
Oct 11 00:20:32 Finished compiler/backend/ag32/proofs                         14m53s   3GB
Oct 11 00:20:32 Starting compiler/backend/cv_compute
Oct 11 00:21:50 Finished compiler/backend/cv_compute                           1m17s   2GB
Oct 11 00:21:50 Starting cv_translator
Oct 11 00:42:44 Finished cv_translator                                        20m53s   7GB
Oct 11 00:42:44 Starting candle/set-theory
Oct 11 00:43:21 Finished candle/set-theory                                       37s 967MB
Oct 11 00:43:21 Starting candle/syntax-lib
Oct 11 00:43:23 Finished candle/syntax-lib                                        1s  21MB
Oct 11 00:43:23 Starting candle/standard/syntax
Oct 11 00:43:36 Finished candle/standard/syntax                                  12s 818MB
Oct 11 00:43:36 Starting candle/standard/semantics
Oct 11 00:45:50 Finished candle/standard/semantics                             2m13s   1GB
Oct 11 00:45:50 Starting candle/standard/monadic
Oct 11 00:45:52 Finished candle/standard/monadic                                  1s  24MB
Oct 11 00:45:52 Starting candle/standard/ml_kernel
Oct 11 00:47:44 Finished candle/standard/ml_kernel                             1m52s   3GB
Oct 11 00:47:44 Starting candle/overloading/syntax
Oct 11 00:51:15 Finished candle/overloading/syntax                             3m30s   1GB
Oct 11 00:51:15 Starting candle/overloading/semantics
Oct 11 01:03:58 Finished candle/overloading/semantics                         12m43s   3GB
Oct 11 01:03:58 Starting candle/overloading/monadic
Oct 11 01:06:28 Finished candle/overloading/monadic                            2m30s   1GB
Oct 11 01:06:29 Starting candle/overloading/ml_kernel
Oct 11 01:14:56 Finished candle/overloading/ml_kernel                          8m27s   3GB
Oct 11 01:14:56 Starting candle/overloading/ml_checker
Oct 11 01:17:43 Finished candle/overloading/ml_checker                         2m46s   2GB
Oct 11 01:17:43 Starting candle/prover
Oct 11 01:28:10 Finished candle/prover                                        10m26s   3GB
Oct 11 01:28:10 Starting pancake
Oct 11 01:28:36 Finished pancake                                                 25s 828MB
Oct 11 01:28:36 Starting pancake/ffi
Oct 11 01:28:36 Finished pancake/ffi                                              0s  13MB
Oct 11 01:28:36 Starting pancake/semantics
Oct 11 01:31:06 Finished pancake/semantics                                     2m29s   1GB
Oct 11 01:31:06 Starting pancake/parser
Oct 11 01:31:34 Finished pancake/parser                                          27s 486MB
Oct 11 01:31:34 Starting pancake/proofs
Oct 11 01:51:37 Finished pancake/proofs                                       20m02s   3GB
Oct 11 01:51:37 Starting compiler/dafny
Oct 11 01:54:20 Finished compiler/dafny                                        2m43s   9GB
Oct 11 01:54:20 Starting compiler/dafny/translation
Oct 11 02:25:35 Finished compiler/dafny/translation                           31m14s  19GB
Oct 11 02:25:35 Starting compiler/dafny/compilation
Oct 11 02:29:12 Finished compiler/dafny/compilation                            3m37s  10GB
Oct 11 02:29:13 Starting compiler/dafny/semantics
Oct 11 02:29:51 Finished compiler/dafny/semantics                                37s 827MB
Oct 11 02:29:51 Starting characteristic/examples
Oct 11 02:31:25 Finished characteristic/examples                               1m34s   3GB
Oct 11 02:31:25 Starting tutorial/solutions
Oct 11 02:34:13 Finished tutorial/solutions                                    2m47s   4GB
Oct 11 02:34:13 Starting translator/monadic/examples
Oct 11 02:38:11 Finished translator/monadic/examples                           3m58s   2GB
Oct 11 02:38:11 Starting examples
Oct 11 02:58:42 Finished examples                                             20m30s   4GB
Oct 11 02:58:42 Starting examples/compilation/x64
Oct 11 03:08:08 Finished examples/compilation/x64                              9m25s   6GB
Oct 11 03:08:08 Starting examples/compilation/x64/proofs
Oct 11 03:12:16 Finished examples/compilation/x64/proofs                       4m08s   4GB
Oct 11 03:12:16 Starting examples/compilation/ag32
Oct 11 03:14:54 Finished examples/compilation/ag32                             2m37s   3GB
Oct 11 03:14:54 Starting examples/compilation/ag32/proofs
Oct 11 03:16:33 Finished examples/compilation/ag32/proofs                      1m38s   5GB
Oct 11 03:16:33 Starting examples/compilation/to_word
Oct 11 03:20:43 Finished examples/compilation/to_word                          4m10s   7GB
Oct 11 03:20:43 Starting examples/lpr_checker
Oct 11 03:21:23 Finished examples/lpr_checker                                    39s 990MB
Oct 11 03:21:23 Starting examples/lpr_checker/array
Oct 11 03:55:49 Finished examples/lpr_checker/array                           34m26s   4GB
Oct 11 03:55:50 Starting examples/lpr_checker/array/compilation
Oct 11 03:59:40 Finished examples/lpr_checker/array/compilation                3m50s   8GB
Oct 11 03:59:40 Starting examples/lpr_checker/array/compilation/proofs
Oct 11 04:01:16 Finished examples/lpr_checker/array/compilation/proofs         1m35s   6GB
Oct 11 04:01:16 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 11 04:02:42 Finished examples/lpr_checker/array/compilation/proofsARM8     1m25s   6GB
Oct 11 04:02:42 Starting examples/xlrup_checker
Oct 11 04:03:22 Finished examples/xlrup_checker                                  39s 891MB
Oct 11 04:03:22 Starting examples/xlrup_checker/array
Oct 11 04:18:32 Finished examples/xlrup_checker/array                         15m09s   2GB
Oct 11 04:18:32 Starting examples/xlrup_checker/array/compilation
Oct 11 04:19:59 Finished examples/xlrup_checker/array/compilation              1m27s   4GB
Oct 11 04:19:59 Starting examples/xlrup_checker/array/compilation/proofs
Oct 11 04:21:08 Finished examples/xlrup_checker/array/compilation/proofs       1m08s   5GB
Oct 11 04:21:08 Starting examples/pseudo_bool
Oct 11 04:22:45 Finished examples/pseudo_bool                                  1m37s   1GB
Oct 11 04:22:45 Starting examples/pseudo_bool/cnf_encoding
Oct 11 04:23:17 Finished examples/pseudo_bool/cnf_encoding                       31s 993MB
Oct 11 04:23:17 Starting examples/pseudo_bool/graph_encoding
Oct 11 04:24:08 Finished examples/pseudo_bool/graph_encoding                     50s   1GB
Oct 11 04:24:08 Starting examples/pseudo_bool/array
Oct 11 05:34:37 Finished examples/pseudo_bool/array                         1h10m28s   8GB
Oct 11 05:34:37 Starting examples/pseudo_bool/array/compilation
Oct 11 05:50:06 Finished examples/pseudo_bool/array/compilation               15m29s  26GB
Oct 11 05:50:06 Starting examples/pseudo_bool/array/compilation/proofs
Oct 11 05:53:43 Finished examples/pseudo_bool/array/compilation/proofs         3m37s   7GB
Oct 11 05:53:43 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 11 05:55:02 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m18s   6GB
Oct 11 05:55:02 Starting examples/opentheory
Oct 11 06:04:23 Finished examples/opentheory                                   9m21s   2GB
Oct 11 06:04:23 Starting examples/opentheory
Oct 11 06:04:25 Finished examples/opentheory                                      1s  32MB
Oct 11 06:04:25 Starting examples/opentheory/compilation
Oct 11 06:06:29 Finished examples/opentheory/compilation                       2m03s   7GB
Oct 11 06:06:29 Starting examples/opentheory/compilation/proofs
Oct 11 06:07:40 Finished examples/opentheory/compilation/proofs                1m10s   5GB
Oct 11 06:07:40 Starting examples/opentheory/compilation/ag32
Oct 11 06:09:45 Finished examples/opentheory/compilation/ag32                  2m05s   5GB
Oct 11 06:09:45 Starting examples/opentheory/compilation/ag32/proofs
Oct 11 06:11:33 Finished examples/opentheory/compilation/ag32/proofs           1m47s   8GB
Oct 11 06:11:33 Starting examples/sat_encodings
Oct 11 06:12:42 Finished examples/sat_encodings                                1m09s 602MB
Oct 11 06:12:42 Starting examples/sat_encodings/case_studies
Oct 11 06:14:39 Finished examples/sat_encodings/case_studies                   1m56s   1GB
Oct 11 06:14:39 Starting examples/sat_encodings/translation
Oct 11 06:18:53 Finished examples/sat_encodings/translation                    4m14s   1GB
Oct 11 06:18:53 Starting examples/sat_encodings/translation/compilation
Oct 11 06:21:29 Finished examples/sat_encodings/translation/compilation        2m35s   5GB
Oct 11 06:21:30 Starting examples/deflate
Oct 11 06:22:03 Finished examples/deflate                                        33s 492MB
Oct 11 06:22:03 Starting examples/deflate/translation
Oct 11 06:23:16 Finished examples/deflate/translation                          1m13s   1GB
Oct 11 06:23:16 Starting examples/deflate/translation/compilation
Oct 11 06:24:30 Finished examples/deflate/translation/compilation              1m13s   4GB
Oct 11 06:24:31 Starting examples/vipr
Oct 11 06:28:34 Finished examples/vipr                                         4m02s   4GB
Oct 11 06:28:34 Starting examples/vipr/compilation
Oct 11 06:29:52 Finished examples/vipr/compilation                             1m18s   4GB
Oct 11 06:29:52 Starting translator/okasaki-examples
Oct 11 06:34:32 Finished translator/okasaki-examples                           4m40s   2GB
Oct 11 06:34:32 Starting translator/other-examples
Oct 11 06:35:34 Finished translator/other-examples                             1m01s   1GB
Oct 11 06:35:34 Starting compiler/parsing/tests
Oct 11 06:36:11 Finished compiler/parsing/tests                                  37s   1GB
Oct 11 06:36:12 Starting compiler/inference/tests
Oct 11 06:36:48 Finished compiler/inference/tests                                36s   1GB
Oct 11 06:36:48 Starting compiler/printing/test
Oct 11 06:38:21 Finished compiler/printing/test                                1m32s   2GB
Oct 11 06:38:21 Starting icing/flover
Oct 11 07:24:45 Finished icing/flover                                         46m23s   2GB
Oct 11 07:24:45 Starting icing/
Oct 11 07:54:12 Finished icing/                                               29m27s   3GB
Oct 11 07:54:13 Starting icing/examples
Oct 11 07:55:56 Finished icing/examples                                        1m43s   4GB
Oct 11 07:55:56 Starting compiler/repl
Oct 11 08:04:53 Finished compiler/repl                                         8m56s   6GB
Oct 11 08:04:53 Starting unverified/sexpr-bootstrap/x64/64
Oct 11 08:21:08 Finished unverified/sexpr-bootstrap/x64/64                    16m14s  18GB
Oct 11 08:21:08 Starting unverified/sexpr-bootstrap/x64/32
Oct 11 08:33:59 Finished unverified/sexpr-bootstrap/x64/32                    12m50s  15GB
Oct 11 08:33:59 Starting compiler/benchmarks
Oct 11 08:49:42 Finished compiler/benchmarks                                  15m42s   2GB
Oct 11 08:49:42 Starting compiler/bootstrap/compilation/x64/64
Oct 11 09:31:53 Finished compiler/bootstrap/compilation/x64/64                42m10s  63GB
Oct 11 09:31:53 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 11 09:57:18 Finished compiler/bootstrap/compilation/x64/64/proofs         25m25s  62GB
Oct 11 09:57:18 Starting compiler/bootstrap/compilation/x64/32
Oct 11 10:40:23 Finished compiler/bootstrap/compilation/x64/32                43m05s  30GB
Oct 11 10:40:24 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 11 10:44:30 Finished compiler/bootstrap/compilation/x64/32/proofs          4m06s  26GB
Oct 11 10:44:30 Starting compiler/bootstrap/compilation/arm8/64
Oct 11 11:36:55 Finished compiler/bootstrap/compilation/arm8/64               52m24s  64GB
Oct 11 11:36:55 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 11 11:44:06 Finished compiler/bootstrap/compilation/arm8/64/proofs         7m10s  24GB
Oct 11 11:44:06 Starting compiler/bootstrap/compilation/ag32/32
Oct 11 12:20:59 Finished compiler/bootstrap/compilation/ag32/32               36m53s  64GB
Oct 11 12:20:59 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 11 12:27:42 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m42s  21GB
Oct 11 12:27:42 SUCCESS