Job 2634

CakeML:f75fcbe801e04eaa9ba012a65a23b09ddb54203a
  Fix proof broken by recent HOL change [Oct 03 03:30:59]
HOL:277f6ad618617d462cd4ad2955206cb261828f87
  Add proofs about clock for fun-op-sem/imp (#1310) [Oct 03 07:36:31]
Machine:pavlova
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 04 15:54:42 Claimed job
Oct 04 15:54:50 Building HOL
Oct 04 16:10:01 Starting developers
Oct 04 16:10:05 Finished developers                                               2s 222MB
Oct 04 16:10:06 Starting developers/bin
Oct 04 16:10:26 Finished developers/bin                                          19s   1GB
Oct 04 16:10:27 Starting compiler/proofs
Oct 04 17:57:15 Finished compiler/proofs                                    1h46m47s  33GB
Oct 04 17:57:16 Starting compiler/bootstrap/translation
Oct 05 03:01:32 Finished compiler/bootstrap/translation                     9h04m15s  61GB
Oct 05 03:01:33 Starting semantics/ffi
Oct 05 03:01:43 Finished semantics/ffi                                            9s 670MB
Oct 05 03:01:44 Starting semantics
Oct 05 03:01:46 Finished semantics                                                0s  69MB
Oct 05 03:01:47 Starting semantics/proofs
Oct 05 03:02:10 Finished semantics/proofs                                        22s 842MB
Oct 05 03:02:11 Starting semantics/alt_semantics
Oct 05 03:02:35 Finished semantics/alt_semantics                                 22s 863MB
Oct 05 03:02:36 Starting semantics/alt_semantics/proofs
Oct 05 03:12:50 Finished semantics/alt_semantics/proofs                       10m13s   4GB
Oct 05 03:12:51 Starting basis/pure
Oct 05 03:12:53 Finished basis/pure                                               0s  71MB
Oct 05 03:12:54 Starting translator
Oct 05 03:14:30 Finished translator                                            1m35s   4GB
Oct 05 03:14:31 Starting compiler/parsing
Oct 05 03:14:32 Finished compiler/parsing                                         0s  72MB
Oct 05 03:14:33 Starting characteristic
Oct 05 03:14:35 Finished characteristic                                           0s  95MB
Oct 05 03:14:36 Starting translator/monadic
Oct 05 03:14:38 Finished translator/monadic                                       0s 101MB
Oct 05 03:14:39 Starting basis
Oct 05 03:17:01 Finished basis                                                 2m21s   4GB
Oct 05 03:17:01 Starting compiler/inference
Oct 05 03:17:03 Finished compiler/inference                                       0s  94MB
Oct 05 03:17:04 Starting compiler/backend/reg_alloc
Oct 05 03:17:05 Finished compiler/backend/reg_alloc                               0s  64MB
Oct 05 03:17:06 Starting compiler/backend/gc
Oct 05 03:17:08 Finished compiler/backend/gc                                      1s 149MB
Oct 05 03:17:09 Starting compiler/backend
Oct 05 03:17:15 Finished compiler/backend                                         4s 310MB
Oct 05 03:17:16 Starting compiler/encoders/asm
Oct 05 03:17:17 Finished compiler/encoders/asm                                    0s  90MB
Oct 05 03:17:18 Starting compiler/encoders/x64
Oct 05 03:17:20 Finished compiler/encoders/x64                                    0s  95MB
Oct 05 03:17:21 Starting compiler/encoders/arm7
Oct 05 03:17:22 Finished compiler/encoders/arm7                                   0s  99MB
Oct 05 03:17:23 Starting compiler/encoders/arm8
Oct 05 03:17:25 Finished compiler/encoders/arm8                                   0s  99MB
Oct 05 03:17:26 Starting compiler/encoders/arm8_asl
Oct 05 05:46:37 Finished compiler/encoders/arm8_asl                         2h29m10s  44GB
Oct 05 05:46:38 Starting compiler/encoders/mips
Oct 05 05:46:39 Finished compiler/encoders/mips                                   0s  92MB
Oct 05 05:46:40 Starting compiler/encoders/riscv
Oct 05 05:46:42 Finished compiler/encoders/riscv                                  0s  94MB
Oct 05 05:46:43 Starting compiler/encoders/ag32
Oct 05 05:46:45 Finished compiler/encoders/ag32                                   0s  89MB
Oct 05 05:46:45 Starting compiler/backend/x64
Oct 05 05:46:47 Finished compiler/backend/x64                                     1s 140MB
Oct 05 05:46:48 Starting compiler/backend/arm7
Oct 05 05:46:50 Finished compiler/backend/arm7                                    1s 139MB
Oct 05 05:46:51 Starting compiler/backend/arm8
Oct 05 05:46:53 Finished compiler/backend/arm8                                    1s 139MB
Oct 05 05:46:54 Starting compiler/backend/mips
Oct 05 05:46:56 Finished compiler/backend/mips                                    1s 139MB
Oct 05 05:46:57 Starting compiler/backend/riscv
Oct 05 05:46:59 Finished compiler/backend/riscv                                   1s 139MB
Oct 05 05:47:00 Starting compiler/backend/ag32
Oct 05 05:48:12 Finished compiler/backend/ag32                                 1m10s   2GB
Oct 05 05:48:12 Starting compiler/parsing/proofs
Oct 05 05:48:14 Finished compiler/parsing/proofs                                  0s  75MB
Oct 05 05:48:15 Starting compiler/inference/proofs
Oct 05 05:48:17 Finished compiler/inference/proofs                                0s  99MB
Oct 05 05:48:17 Starting compiler/backend/semantics
Oct 05 05:51:36 Finished compiler/backend/semantics                            3m17s   3GB
Oct 05 05:51:37 Starting compiler/backend/reg_alloc/proofs
Oct 05 05:51:39 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
Oct 05 05:51:39 Starting compiler/backend/proofs
Oct 05 05:52:34 Finished compiler/backend/proofs                                 53s   2GB
Oct 05 05:52:35 Starting compiler/backend/serialiser
Oct 05 05:52:37 Finished compiler/backend/serialiser                              1s 151MB
Oct 05 05:52:38 Starting compiler/encoders/x64/proofs
Oct 05 06:02:50 Finished compiler/encoders/x64/proofs                         10m10s   5GB
Oct 05 06:02:51 Starting compiler/encoders/arm7/proofs
Oct 05 06:15:46 Finished compiler/encoders/arm7/proofs                        12m54s   8GB
Oct 05 06:15:47 Starting compiler/encoders/arm8/proofs
Oct 05 06:22:38 Finished compiler/encoders/arm8/proofs                         6m50s   7GB
Oct 05 06:22:39 Starting compiler/encoders/arm8_asl/proofs
Oct 05 07:13:07 Finished compiler/encoders/arm8_asl/proofs                    50m26s   5GB
Oct 05 07:13:08 Starting compiler/encoders/mips/proofs
Oct 05 07:23:16 Finished compiler/encoders/mips/proofs                        10m06s   6GB
Oct 05 07:23:16 Starting compiler/encoders/riscv/proofs
Oct 05 07:31:56 Finished compiler/encoders/riscv/proofs                        8m38s   4GB
Oct 05 07:31:57 Starting compiler/encoders/ag32/proofs
Oct 05 07:34:55 Finished compiler/encoders/ag32/proofs                         2m57s   2GB
Oct 05 07:34:56 Starting compiler/backend/x64/proofs
Oct 05 07:35:42 Finished compiler/backend/x64/proofs                             45s   3GB
Oct 05 07:35:43 Starting compiler/backend/arm7/proofs
Oct 05 07:36:30 Finished compiler/backend/arm7/proofs                            46s   2GB
Oct 05 07:36:31 Starting compiler/backend/arm8/proofs
Oct 05 07:37:15 Finished compiler/backend/arm8/proofs                            42s   3GB
Oct 05 07:37:16 Starting compiler/backend/arm8_asl
Oct 05 07:37:46 Finished compiler/backend/arm8_asl                               29s   2GB
Oct 05 07:37:47 Starting compiler/backend/mips/proofs
Oct 05 07:38:38 Finished compiler/backend/mips/proofs                            49s   3GB
Oct 05 07:38:39 Starting compiler/backend/riscv/proofs
Oct 05 07:39:36 Finished compiler/backend/riscv/proofs                           55s   3GB
Oct 05 07:39:37 Starting compiler/backend/ag32/proofs
Oct 05 07:54:43 Finished compiler/backend/ag32/proofs                         15m05s   6GB
Oct 05 07:54:44 Starting compiler/backend/cv_compute
Oct 05 07:56:36 Finished compiler/backend/cv_compute                           1m51s   3GB
Oct 05 07:56:37 Starting cv_translator
Oct 05 08:16:58 Finished cv_translator                                        20m19s  13GB
Oct 05 08:16:58 Starting candle/set-theory
Oct 05 08:17:48 Finished candle/set-theory                                       48s   1GB
Oct 05 08:17:48 Starting candle/syntax-lib
Oct 05 08:17:50 Finished candle/syntax-lib                                        0s  69MB
Oct 05 08:17:51 Starting candle/standard/syntax
Oct 05 08:18:11 Finished candle/standard/syntax                                  19s   1GB
Oct 05 08:18:12 Starting candle/standard/semantics
Oct 05 08:21:07 Finished candle/standard/semantics                             2m54s   4GB
Oct 05 08:21:08 Starting candle/standard/monadic
Oct 05 08:21:10 Finished candle/standard/monadic                                  0s 106MB
Oct 05 08:21:10 Starting candle/standard/ml_kernel
Oct 05 08:23:16 Finished candle/standard/ml_kernel                             2m04s   5GB
Oct 05 08:23:17 Starting candle/overloading/syntax
Oct 05 08:27:01 Finished candle/overloading/syntax                             3m43s   2GB
Oct 05 08:27:02 Starting candle/overloading/semantics
Oct 05 08:38:41 Finished candle/overloading/semantics                         11m37s   5GB
Oct 05 08:38:42 Starting candle/overloading/monadic
Oct 05 08:41:10 Finished candle/overloading/monadic                            2m26s   2GB
Oct 05 08:41:10 Starting candle/overloading/ml_kernel
Oct 05 08:49:21 Finished candle/overloading/ml_kernel                          8m09s   7GB
Oct 05 08:49:22 Starting candle/overloading/ml_checker
Oct 05 08:52:05 Finished candle/overloading/ml_checker                         2m42s   7GB
Oct 05 08:52:06 Starting candle/prover
Oct 05 09:02:44 Finished candle/prover                                        10m36s   5GB
Oct 05 09:02:45 Starting pancake
Oct 05 09:03:13 Finished pancake                                                 27s 953MB
Oct 05 09:03:14 Starting pancake/ffi
Oct 05 09:03:14 Finished pancake/ffi                                              0s  22MB
Oct 05 09:03:15 Starting pancake/semantics
Oct 05 09:05:29 Finished pancake/semantics                                     2m13s   2GB
Oct 05 09:05:30 Starting pancake/parser
Oct 05 09:05:54 Finished pancake/parser                                          22s 598MB
Oct 05 09:05:55 Starting pancake/proofs
Oct 05 09:22:12 Finished pancake/proofs                                       16m16s   6GB
Oct 05 09:22:13 Starting compiler/dafny
Oct 05 09:24:48 Finished compiler/dafny                                        2m33s  10GB
Oct 05 09:24:48 Starting compiler/dafny/translation
Oct 05 09:53:18 Finished compiler/dafny/translation                           28m29s  14GB
Oct 05 09:53:19 Starting compiler/dafny/compilation
Oct 05 09:56:51 Finished compiler/dafny/compilation                            3m30s  14GB
Oct 05 09:56:52 Starting compiler/dafny/semantics
Oct 05 09:57:30 Finished compiler/dafny/semantics                                36s   1GB
Oct 05 09:57:31 Starting characteristic/examples
Oct 05 09:59:02 Finished characteristic/examples                               1m29s   5GB
Oct 05 09:59:02 Starting tutorial/solutions
Oct 05 10:01:56 Finished tutorial/solutions                                    2m52s   6GB
Oct 05 10:01:57 Starting translator/monadic/examples
Oct 05 10:05:16 Finished translator/monadic/examples                           3m17s   4GB
Oct 05 10:05:17 Starting examples
Oct 05 10:17:32 Finished examples                                             12m14s   7GB
Oct 05 10:17:33 Starting examples/compilation/x64
Oct 05 10:27:37 Finished examples/compilation/x64                             10m03s   7GB
Oct 05 10:27:38 Starting examples/compilation/x64/proofs
Oct 05 10:32:33 Finished examples/compilation/x64/proofs                       4m54s   7GB
Oct 05 10:32:34 Starting examples/compilation/ag32
Oct 05 10:35:18 Finished examples/compilation/ag32                             2m43s   5GB
Oct 05 10:35:19 Starting examples/compilation/ag32/proofs
Oct 05 10:37:20 Finished examples/compilation/ag32/proofs                      1m59s   8GB
Oct 05 10:37:21 Starting examples/compilation/to_word
Oct 05 10:41:40 Finished examples/compilation/to_word                          4m18s  14GB
Oct 05 10:41:41 Starting examples/lpr_checker
Oct 05 10:42:12 Finished examples/lpr_checker                                    30s   1GB
Oct 05 10:42:13 Starting examples/lpr_checker/array
Oct 05 11:08:50 Finished examples/lpr_checker/array                           26m36s  28GB
Oct 05 11:08:51 Starting examples/lpr_checker/array/compilation
Oct 05 11:11:31 Finished examples/lpr_checker/array/compilation                2m38s  10GB
Oct 05 11:11:31 Starting examples/lpr_checker/array/compilation/proofs
Oct 05 11:13:37 Finished examples/lpr_checker/array/compilation/proofs         2m04s   8GB
Oct 05 11:13:37 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 05 11:15:39 Finished examples/lpr_checker/array/compilation/proofsARM8     2m00s   8GB
Oct 05 11:15:40 Starting examples/xlrup_checker
Oct 05 11:16:16 Finished examples/xlrup_checker                                  35s   1GB
Oct 05 11:16:16 Starting examples/xlrup_checker/array
Oct 05 11:29:37 Finished examples/xlrup_checker/array                         13m18s  10GB
Oct 05 11:29:38 Starting examples/xlrup_checker/array/compilation
Oct 05 11:31:08 Finished examples/xlrup_checker/array/compilation              1m28s   7GB
Oct 05 11:31:08 Starting examples/xlrup_checker/array/compilation/proofs
Oct 05 11:32:56 Finished examples/xlrup_checker/array/compilation/proofs       1m46s   8GB
Oct 05 11:32:57 Starting examples/pseudo_bool
Oct 05 11:34:23 Finished examples/pseudo_bool                                  1m25s   1GB
Oct 05 11:34:24 Starting examples/pseudo_bool/cnf_encoding
Oct 05 11:35:06 Finished examples/pseudo_bool/cnf_encoding                       41s   1GB
Oct 05 11:35:07 Starting examples/pseudo_bool/graph_encoding
Oct 05 11:36:02 Finished examples/pseudo_bool/graph_encoding                     54s   1GB
Oct 05 11:36:03 Starting examples/pseudo_bool/array
Oct 05 12:39:09 Finished examples/pseudo_bool/array                         1h03m05s  28GB
Oct 05 12:39:10 Starting examples/pseudo_bool/array/compilation
Oct 05 12:53:13 Finished examples/pseudo_bool/array/compilation               14m01s  31GB
Oct 05 12:53:14 Starting examples/pseudo_bool/array/compilation/proofs
Oct 05 12:57:28 Finished examples/pseudo_bool/array/compilation/proofs         4m13s  10GB
Oct 05 12:57:29 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 05 12:59:27 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m57s   8GB
Oct 05 12:59:28 Starting examples/opentheory
Oct 05 13:08:18 Finished examples/opentheory                                   8m49s   5GB
Oct 05 13:08:19 Starting examples/opentheory
Oct 05 13:08:21 Finished examples/opentheory                                      1s 126MB
Oct 05 13:08:22 Starting examples/opentheory/compilation
Oct 05 13:10:30 Finished examples/opentheory/compilation                       2m07s   9GB
Oct 05 13:10:31 Starting examples/opentheory/compilation/proofs
Oct 05 13:12:24 Finished examples/opentheory/compilation/proofs                1m52s   6GB
Oct 05 13:12:25 Starting examples/opentheory/compilation/ag32
Oct 05 13:14:43 Finished examples/opentheory/compilation/ag32                  2m16s   8GB
Oct 05 13:14:44 Starting examples/opentheory/compilation/ag32/proofs
Oct 05 13:17:20 Finished examples/opentheory/compilation/ag32/proofs           2m35s  13GB
Oct 05 13:17:21 Starting examples/sat_encodings
Oct 05 13:18:24 Finished examples/sat_encodings                                1m02s 935MB
Oct 05 13:18:25 Starting examples/sat_encodings/case_studies
Oct 05 13:20:38 Finished examples/sat_encodings/case_studies                   2m11s   2GB
Oct 05 13:20:39 Starting examples/sat_encodings/translation
Oct 05 13:24:24 Finished examples/sat_encodings/translation                    3m44s   3GB
Oct 05 13:24:25 Starting examples/sat_encodings/translation/compilation
Oct 05 13:26:56 Finished examples/sat_encodings/translation/compilation        2m30s   7GB
Oct 05 13:26:57 Starting examples/deflate
Oct 05 13:27:26 Finished examples/deflate                                        28s 775MB
Oct 05 13:27:27 Starting examples/deflate/translation
Oct 05 13:28:27 Finished examples/deflate/translation                            59s   2GB
Oct 05 13:28:28 Starting examples/deflate/translation/compilation
Oct 05 13:29:37 Finished examples/deflate/translation/compilation              1m08s   6GB
Oct 05 13:29:38 Starting examples/vipr
Oct 05 13:33:20 Finished examples/vipr                                         3m41s   4GB
Oct 05 13:33:21 Starting examples/vipr/compilation
Oct 05 13:34:44 Finished examples/vipr/compilation                             1m22s   6GB
Oct 05 13:34:45 Starting translator/okasaki-examples
Oct 05 13:39:01 Finished translator/okasaki-examples                           4m14s   4GB
Oct 05 13:39:02 Starting translator/other-examples
Oct 05 13:44:15 Finished translator/other-examples                             5m12s   3GB
Oct 05 13:44:16 Starting compiler/parsing/tests
Oct 05 13:44:56 Finished compiler/parsing/tests                                  38s   1GB
Oct 05 13:44:57 Starting compiler/inference/tests
Oct 05 13:45:44 Finished compiler/inference/tests                                46s   3GB
Oct 05 13:45:45 Starting compiler/printing/test
Oct 05 13:47:28 Finished compiler/printing/test                                1m41s   6GB
Oct 05 13:47:29 Starting icing/flover
Oct 05 14:24:48 Finished icing/flover                                         37m18s   4GB
Oct 05 14:24:49 Starting icing/
Oct 05 14:52:41 Finished icing/                                               27m51s   9GB
Oct 05 14:52:42 Starting icing/examples
Oct 05 14:54:41 Finished icing/examples                                        1m57s   9GB
Oct 05 14:54:42 Starting compiler/repl
Oct 05 15:03:58 Finished compiler/repl                                         9m15s  10GB
Oct 05 15:03:59 Starting unverified/sexpr-bootstrap/x64/64
Oct 05 15:18:25 Finished unverified/sexpr-bootstrap/x64/64                    13m59s  19GB
Oct 05 15:18:26 Starting unverified/sexpr-bootstrap/x64/32
Oct 05 15:30:00 Finished unverified/sexpr-bootstrap/x64/32                    11m14s  14GB
Oct 05 15:30:01 Starting compiler/benchmarks
Oct 05 15:30:47 Finished compiler/benchmarks                                     44s 711MB
Oct 05 15:30:47 Starting compiler/bootstrap/compilation/x64/64
Oct 05 16:16:17 Finished compiler/bootstrap/compilation/x64/64                45m16s 130GB
Oct 05 16:16:18 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 05 16:41:26 Finished compiler/bootstrap/compilation/x64/64/proofs         25m07s  61GB
Oct 05 16:41:27 Starting compiler/bootstrap/compilation/x64/32
Oct 05 17:23:16 Finished compiler/bootstrap/compilation/x64/32                41m40s 110GB
Oct 05 17:23:17 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 05 17:28:40 Finished compiler/bootstrap/compilation/x64/32/proofs          5m22s  26GB
Oct 05 17:28:41 Starting compiler/bootstrap/compilation/arm8/64
Oct 05 18:29:18 Finished compiler/bootstrap/compilation/arm8/64             1h00m28s 135GB
Oct 05 18:29:19 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 05 18:35:57 Finished compiler/bootstrap/compilation/arm8/64/proofs         6m36s  34GB
Oct 05 18:35:58 Starting compiler/bootstrap/compilation/ag32/32
Oct 05 19:19:37 Finished compiler/bootstrap/compilation/ag32/32               43m37s 109GB
Oct 05 19:19:38 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 05 19:26:01 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m22s  33GB
Oct 05 19:26:02 SUCCESS