Job 2640

CakeML:dfbdb671e1bb100903b2fc50179b1241bba4b006
  Fix errors [Sep 30 21:15:46]
#1061 (remove-tDefine-paren-matching)
Merging into:95fcf67a782508c8452388d720098fe2bd4a4a3a
  Merge pull request #1063 from CakeML/remove-xdefine [Oct 05 18:51:32]
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

Oct 06 08:08:35 Claimed job
Oct 06 08:08:37 Reusing HOL
Oct 06 08:09:22 Starting developers
Oct 06 08:09:28 Finished developers                                               5s 126MB
Oct 06 08:09:28 Starting developers/bin
Oct 06 08:09:34 Finished developers/bin                                           5s   1GB
Oct 06 08:09:34 Starting compiler/proofs
Oct 06 10:04:45 Finished compiler/proofs                                    1h55m11s  17GB
Oct 06 10:04:46 Starting compiler/bootstrap/translation
Oct 06 18:58:06 Finished compiler/bootstrap/translation                     8h53m20s  37GB
Oct 06 18:58:06 Starting semantics/ffi
Oct 06 18:58:11 Finished semantics/ffi                                            5s 410MB
Oct 06 18:58:12 Starting semantics
Oct 06 18:58:13 Finished semantics                                                1s  18MB
Oct 06 18:58:13 Starting semantics/proofs
Oct 06 18:58:39 Finished semantics/proofs                                        25s 442MB
Oct 06 18:58:39 Starting semantics/alt_semantics
Oct 06 18:59:02 Finished semantics/alt_semantics                                 22s 524MB
Oct 06 18:59:02 Starting semantics/alt_semantics/proofs
Oct 06 19:10:36 Finished semantics/alt_semantics/proofs                       11m34s   1GB
Oct 06 19:10:36 Starting basis/pure
Oct 06 19:10:38 Finished basis/pure                                               1s  22MB
Oct 06 19:10:38 Starting translator
Oct 06 19:12:16 Finished translator                                            1m38s   2GB
Oct 06 19:12:16 Starting compiler/parsing
Oct 06 19:12:18 Finished compiler/parsing                                         1s  18MB
Oct 06 19:12:18 Starting characteristic
Oct 06 19:12:20 Finished characteristic                                           1s  23MB
Oct 06 19:12:20 Starting translator/monadic
Oct 06 19:12:22 Finished translator/monadic                                       1s  23MB
Oct 06 19:12:22 Starting basis
Oct 06 19:14:54 Finished basis                                                 2m31s   3GB
Oct 06 19:14:54 Starting compiler/inference
Oct 06 19:14:56 Finished compiler/inference                                       1s  24MB
Oct 06 19:14:56 Starting compiler/backend/reg_alloc
Oct 06 19:14:57 Finished compiler/backend/reg_alloc                               1s  21MB
Oct 06 19:14:57 Starting compiler/backend/gc
Oct 06 19:15:00 Finished compiler/backend/gc                                      2s  32MB
Oct 06 19:15:00 Starting compiler/backend
Oct 06 19:15:06 Finished compiler/backend                                         5s 268MB
Oct 06 19:15:06 Starting compiler/encoders/asm
Oct 06 19:15:08 Finished compiler/encoders/asm                                    1s  20MB
Oct 06 19:15:08 Starting compiler/encoders/x64
Oct 06 19:15:10 Finished compiler/encoders/x64                                    1s  28MB
Oct 06 19:15:10 Starting compiler/encoders/arm7
Oct 06 19:15:12 Finished compiler/encoders/arm7                                   1s  28MB
Oct 06 19:15:12 Starting compiler/encoders/arm8
Oct 06 19:15:14 Finished compiler/encoders/arm8                                   1s  26MB
Oct 06 19:15:14 Starting compiler/encoders/arm8_asl
Oct 06 19:18:19 Finished compiler/encoders/arm8_asl                            3m04s   1GB
Oct 06 19:18:19 Starting compiler/encoders/mips
Oct 06 19:18:21 Finished compiler/encoders/mips                                   1s  28MB
Oct 06 19:18:21 Starting compiler/encoders/riscv
Oct 06 19:18:23 Finished compiler/encoders/riscv                                  1s  29MB
Oct 06 19:18:23 Starting compiler/encoders/ag32
Oct 06 19:18:25 Finished compiler/encoders/ag32                                   1s  23MB
Oct 06 19:18:25 Starting compiler/backend/x64
Oct 06 19:18:27 Finished compiler/backend/x64                                     2s  29MB
Oct 06 19:18:27 Starting compiler/backend/arm7
Oct 06 19:18:30 Finished compiler/backend/arm7                                    2s  32MB
Oct 06 19:18:30 Starting compiler/backend/arm8
Oct 06 19:18:32 Finished compiler/backend/arm8                                    2s  25MB
Oct 06 19:18:32 Starting compiler/backend/mips
Oct 06 19:18:34 Finished compiler/backend/mips                                    2s  25MB
Oct 06 19:18:34 Starting compiler/backend/riscv
Oct 06 19:18:37 Finished compiler/backend/riscv                                   2s  25MB
Oct 06 19:18:37 Starting compiler/backend/ag32
Oct 06 19:19:49 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 06 19:19:49 Starting compiler/parsing/proofs
Oct 06 19:19:51 Finished compiler/parsing/proofs                                  1s  21MB
Oct 06 19:19:51 Starting compiler/inference/proofs
Oct 06 19:19:53 Finished compiler/inference/proofs                                1s  25MB
Oct 06 19:19:53 Starting compiler/backend/semantics
Oct 06 19:23:21 Finished compiler/backend/semantics                            3m27s   1GB
Oct 06 19:23:21 Starting compiler/backend/reg_alloc/proofs
Oct 06 19:23:23 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Oct 06 19:23:23 Starting compiler/backend/proofs
Oct 06 19:24:16 Finished compiler/backend/proofs                                 53s   2GB
Oct 06 19:24:16 Starting compiler/backend/serialiser
Oct 06 19:24:19 Finished compiler/backend/serialiser                              2s  28MB
Oct 06 19:24:19 Starting compiler/encoders/x64/proofs
Oct 06 19:34:57 Finished compiler/encoders/x64/proofs                         10m38s   5GB
Oct 06 19:34:57 Starting compiler/encoders/arm7/proofs
Oct 06 19:49:05 Finished compiler/encoders/arm7/proofs                        14m07s   3GB
Oct 06 19:49:05 Starting compiler/encoders/arm8/proofs
Oct 06 19:56:34 Finished compiler/encoders/arm8/proofs                         7m28s   1GB
Oct 06 19:56:34 Starting compiler/encoders/arm8_asl/proofs
Oct 06 20:13:41 Finished compiler/encoders/arm8_asl/proofs                    17m06s   2GB
Oct 06 20:13:41 Starting compiler/encoders/mips/proofs
Oct 06 20:24:14 Finished compiler/encoders/mips/proofs                        10m33s   4GB
Oct 06 20:24:14 Starting compiler/encoders/riscv/proofs
Oct 06 20:33:24 Finished compiler/encoders/riscv/proofs                        9m09s   1GB
Oct 06 20:33:24 Starting compiler/encoders/ag32/proofs
Oct 06 20:36:43 Finished compiler/encoders/ag32/proofs                         3m19s   1GB
Oct 06 20:36:43 Starting compiler/backend/x64/proofs
Oct 06 20:37:17 Finished compiler/backend/x64/proofs                             33s   2GB
Oct 06 20:37:17 Starting compiler/backend/arm7/proofs
Oct 06 20:37:50 Finished compiler/backend/arm7/proofs                            33s   1GB
Oct 06 20:37:50 Starting compiler/backend/arm8/proofs
Oct 06 20:38:23 Finished compiler/backend/arm8/proofs                            32s   1GB
Oct 06 20:38:23 Starting compiler/backend/arm8_asl
Oct 06 20:38:48 Finished compiler/backend/arm8_asl                               24s   1GB
Oct 06 20:38:48 Starting compiler/backend/mips/proofs
Oct 06 20:39:21 Finished compiler/backend/mips/proofs                            33s   1GB
Oct 06 20:39:21 Starting compiler/backend/riscv/proofs
Oct 06 20:39:58 Finished compiler/backend/riscv/proofs                           36s   2GB
Oct 06 20:39:58 Starting compiler/backend/ag32/proofs
Oct 06 20:55:00 Finished compiler/backend/ag32/proofs                         15m01s   2GB
Oct 06 20:55:00 Starting compiler/backend/cv_compute
Oct 06 20:56:22 Finished compiler/backend/cv_compute                           1m21s   1GB
Oct 06 20:56:22 Starting cv_translator
Oct 06 21:17:32 Finished cv_translator                                        21m10s   6GB
Oct 06 21:17:32 Starting candle/set-theory
Oct 06 21:18:10 Finished candle/set-theory                                       37s 901MB
Oct 06 21:18:10 Starting candle/syntax-lib
Oct 06 21:18:11 Finished candle/syntax-lib                                        1s  24MB
Oct 07 14:08:01 Resuming candle/standard/syntax
Oct 07 14:08:14 Finished candle/standard/syntax                                  12s 837MB
Oct 07 14:08:14 Starting candle/standard/semantics
Oct 07 14:10:27 Finished candle/standard/semantics                             2m12s   1GB
Oct 07 14:10:27 Starting candle/standard/monadic
Oct 07 14:10:29 Finished candle/standard/monadic                                  1s  34MB
Oct 07 14:10:29 Starting candle/standard/ml_kernel
Oct 07 14:12:21 Finished candle/standard/ml_kernel                             1m51s   3GB
Oct 07 14:12:21 Starting candle/overloading/syntax
Oct 07 14:15:50 Finished candle/overloading/syntax                             3m29s   1GB
Oct 07 14:15:51 Starting candle/overloading/semantics
Oct 07 14:28:43 Finished candle/overloading/semantics                         12m52s   3GB
Oct 07 14:28:43 Starting candle/overloading/monadic
Oct 07 14:31:14 Finished candle/overloading/monadic                            2m30s   1GB
Oct 07 14:31:14 Starting candle/overloading/ml_kernel
Oct 07 14:39:32 Finished candle/overloading/ml_kernel                          8m17s   4GB
Oct 07 14:39:32 Starting candle/overloading/ml_checker
Oct 07 14:42:20 Finished candle/overloading/ml_checker                         2m47s   2GB
Oct 07 14:42:20 Starting candle/prover
Oct 07 18:46:23 Resuming candle/prover
Oct 07 18:46:24 Finished candle/prover                                            1s  26MB
Oct 07 18:46:25 Starting pancake
Oct 07 18:46:50 Finished pancake                                                 25s 850MB
Oct 07 18:46:50 Starting pancake/ffi
Oct 07 18:46:51 Finished pancake/ffi                                              0s  13MB
Oct 07 18:46:51 Starting pancake/semantics
Oct 07 18:49:15 Finished pancake/semantics                                     2m24s   1GB
Oct 07 18:49:16 Starting pancake/parser
Oct 07 18:49:41 Finished pancake/parser                                          25s 419MB
Oct 07 18:49:41 Starting pancake/proofs
Oct 07 19:08:10 Finished pancake/proofs                                       18m28s   3GB
Oct 07 19:08:10 Starting compiler/dafny
Oct 07 19:10:37 Finished compiler/dafny                                        2m27s   9GB
Oct 07 19:10:37 Starting compiler/dafny/translation
Oct 07 19:40:59 Finished compiler/dafny/translation                           30m21s  12GB
Oct 07 19:40:59 Starting compiler/dafny/compilation
Oct 07 19:44:23 Finished compiler/dafny/compilation                            3m23s  11GB
Oct 07 19:44:23 Starting compiler/dafny/semantics
Oct 07 19:45:00 Finished compiler/dafny/semantics                                36s 824MB
Oct 07 19:45:00 Starting characteristic/examples
Oct 07 19:46:29 Finished characteristic/examples                               1m29s   3GB
Oct 07 19:46:29 Starting tutorial/solutions
Oct 07 19:49:18 Finished tutorial/solutions                                    2m49s   4GB
Oct 07 19:49:18 Starting translator/monadic/examples
Oct 07 19:52:59 Finished translator/monadic/examples                           3m40s   3GB
Oct 07 19:52:59 Starting examples
Oct 07 20:07:34 Finished examples                                             14m35s   3GB
Oct 07 20:07:34 Starting examples/compilation/x64
Oct 07 20:16:43 Finished examples/compilation/x64                              9m08s   5GB
Oct 07 20:16:43 Starting examples/compilation/x64/proofs
Oct 07 20:19:41 Finished examples/compilation/x64/proofs                       2m58s   4GB
Oct 07 20:19:41 Starting examples/compilation/ag32
Oct 07 20:21:59 Finished examples/compilation/ag32                             2m17s   3GB
Oct 07 20:21:59 Starting examples/compilation/ag32/proofs
Oct 07 20:23:10 Finished examples/compilation/ag32/proofs                      1m10s   5GB
Oct 07 20:23:10 Starting examples/compilation/to_word
Oct 07 20:26:41 Finished examples/compilation/to_word                          3m31s   5GB
Oct 07 20:26:41 Starting examples/lpr_checker
Oct 07 20:27:12 Finished examples/lpr_checker                                    30s 548MB
Oct 07 20:27:12 Starting examples/lpr_checker/array
Oct 07 20:55:20 Finished examples/lpr_checker/array                           28m07s   5GB
Oct 07 20:55:20 Starting examples/lpr_checker/array/compilation
Oct 07 20:58:06 Finished examples/lpr_checker/array/compilation                2m45s   7GB
Oct 07 20:58:06 Starting examples/lpr_checker/array/compilation/proofs
Oct 07 20:59:22 Finished examples/lpr_checker/array/compilation/proofs         1m15s   6GB
Oct 07 20:59:22 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 07 21:00:36 Finished examples/lpr_checker/array/compilation/proofsARM8     1m14s   6GB
Oct 07 21:00:36 Starting examples/xlrup_checker
Oct 07 21:01:14 Finished examples/xlrup_checker                                  37s 848MB
Oct 07 21:01:14 Starting examples/xlrup_checker/array
Oct 07 21:15:45 Finished examples/xlrup_checker/array                         14m31s   2GB
Oct 07 21:15:45 Starting examples/xlrup_checker/array/compilation
Oct 07 21:17:13 Finished examples/xlrup_checker/array/compilation              1m28s   4GB
Oct 07 21:17:14 Starting examples/xlrup_checker/array/compilation/proofs
Oct 07 21:18:18 Finished examples/xlrup_checker/array/compilation/proofs       1m04s   4GB
Oct 07 21:18:18 Starting examples/pseudo_bool
Oct 07 21:19:48 Finished examples/pseudo_bool                                  1m30s   1GB
Oct 07 21:19:49 Starting examples/pseudo_bool/cnf_encoding
Oct 07 21:20:20 Finished examples/pseudo_bool/cnf_encoding                       31s 920MB
Oct 07 21:20:20 Starting examples/pseudo_bool/graph_encoding
Oct 07 21:21:09 Finished examples/pseudo_bool/graph_encoding                     48s   1GB
Oct 07 21:21:09 Starting examples/pseudo_bool/array
Oct 07 22:27:10 Finished examples/pseudo_bool/array                         1h06m00s   8GB
Oct 07 22:27:10 Starting examples/pseudo_bool/array/compilation
Oct 07 22:42:12 Finished examples/pseudo_bool/array/compilation               15m02s  25GB
Oct 07 22:42:12 Starting examples/pseudo_bool/array/compilation/proofs
Oct 07 22:45:10 Finished examples/pseudo_bool/array/compilation/proofs         2m57s   7GB
Oct 07 22:45:10 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 07 22:46:33 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m22s   6GB
Oct 07 22:46:33 Starting examples/opentheory
Oct 07 22:55:45 Finished examples/opentheory                                   9m11s   2GB
Oct 07 22:55:45 Starting examples/opentheory
Oct 07 22:55:47 Finished examples/opentheory                                      1s  29MB
Oct 07 22:55:47 Starting examples/opentheory/compilation
Oct 07 22:57:48 Finished examples/opentheory/compilation                       2m01s   6GB
Oct 07 22:57:48 Starting examples/opentheory/compilation/proofs
Oct 07 22:58:56 Finished examples/opentheory/compilation/proofs                1m07s   4GB
Oct 07 22:58:56 Starting examples/opentheory/compilation/ag32
Oct 07 23:00:59 Finished examples/opentheory/compilation/ag32                  2m02s   5GB
Oct 07 23:00:59 Starting examples/opentheory/compilation/ag32/proofs
Oct 07 23:02:42 Finished examples/opentheory/compilation/ag32/proofs           1m42s   6GB
Oct 07 23:02:42 Starting examples/sat_encodings
Oct 07 23:03:49 Finished examples/sat_encodings                                1m07s 603MB
Oct 07 23:03:50 Starting examples/sat_encodings/case_studies
Oct 07 23:05:44 Finished examples/sat_encodings/case_studies                   1m53s   1GB
Oct 07 23:05:44 Starting examples/sat_encodings/translation
Oct 07 23:09:45 Finished examples/sat_encodings/translation                    4m01s   1GB
Oct 07 23:09:46 Starting examples/sat_encodings/translation/compilation
Oct 07 23:12:12 Finished examples/sat_encodings/translation/compilation        2m26s   5GB
Oct 07 23:12:12 Starting examples/deflate
Oct 07 23:12:44 Finished examples/deflate                                        31s 482MB
Oct 07 23:12:44 Starting examples/deflate/translation
Oct 07 23:13:54 Finished examples/deflate/translation                          1m10s   1GB
Oct 07 23:13:54 Starting examples/deflate/translation/compilation
Oct 07 23:15:03 Finished examples/deflate/translation/compilation              1m09s   4GB
Oct 07 23:15:04 Starting examples/vipr
Oct 07 23:18:57 Finished examples/vipr                                         3m53s   3GB
Oct 07 23:18:57 Starting examples/vipr/compilation
Oct 07 23:20:13 Finished examples/vipr/compilation                             1m15s   4GB
Oct 07 23:20:13 Starting translator/okasaki-examples
Oct 07 23:24:48 Finished translator/okasaki-examples                           4m34s   2GB
Oct 07 23:24:48 Starting translator/other-examples
Oct 07 23:25:46 Finished translator/other-examples                               57s   1GB
Oct 07 23:25:46 Starting compiler/parsing/tests
Oct 07 23:26:23 Finished compiler/parsing/tests                                  36s   1GB
Oct 07 23:26:23 Starting compiler/inference/tests
Oct 07 23:26:56 Finished compiler/inference/tests                                32s   2GB
Oct 07 23:26:56 Starting compiler/printing/test
Oct 07 23:28:29 Finished compiler/printing/test                                1m32s   3GB
Oct 07 23:28:29 Starting icing/flover
Oct 08 00:13:36 Finished icing/flover                                         45m07s   2GB
Oct 08 00:13:36 Starting icing/
Oct 08 00:43:42 Finished icing/                                               30m06s   4GB
Oct 08 00:43:42 Starting icing/examples
Oct 08 00:45:25 Finished icing/examples                                        1m42s   5GB
Oct 08 00:45:25 Starting compiler/repl
Oct 08 00:54:22 Finished compiler/repl                                         8m56s   8GB
Oct 08 00:54:22 Starting unverified/sexpr-bootstrap/x64/64
Oct 08 01:10:34 Finished unverified/sexpr-bootstrap/x64/64                    16m12s  16GB
Oct 08 01:10:35 Starting unverified/sexpr-bootstrap/x64/32
Oct 08 01:23:43 Finished unverified/sexpr-bootstrap/x64/32                    13m08s  14GB
Oct 08 01:23:43 Starting compiler/benchmarks
Oct 08 01:39:28 Finished compiler/benchmarks                                  15m44s   2GB
Oct 08 01:39:28 Starting compiler/bootstrap/compilation/x64/64
Oct 08 02:19:59 Finished compiler/bootstrap/compilation/x64/64                40m30s  63GB
Oct 08 02:19:59 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 08 02:43:11 Finished compiler/bootstrap/compilation/x64/64/proofs         23m11s  25GB
Oct 08 02:43:11 Starting compiler/bootstrap/compilation/x64/32
Oct 08 03:25:21 Finished compiler/bootstrap/compilation/x64/32                42m10s  64GB
Oct 08 03:25:21 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 08 03:31:30 Finished compiler/bootstrap/compilation/x64/32/proofs          6m08s  18GB
Oct 08 03:31:30 Starting compiler/bootstrap/compilation/arm8/64
Oct 08 04:23:21 Finished compiler/bootstrap/compilation/arm8/64               51m50s  64GB
Oct 08 04:23:21 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 08 04:28:36 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m14s  33GB
Oct 08 04:28:36 Starting compiler/bootstrap/compilation/ag32/32
Oct 08 05:08:55 Finished compiler/bootstrap/compilation/ag32/32               40m18s  64GB
Oct 08 05:08:55 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 08 05:15:57 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m01s  21GB
Oct 08 05:15:57 SUCCESS