Job 2644

CakeML:b3a5924c2b064ee3451fe64f0882f4ffea24a3af
  Ban old Datatype syntax [Oct 06 09:12:27]
#1066 (remove-old-datatype)
Merging into:3605d6febc005ce95658bab8f1ba03960dbea51f
  Merge pull request #1065 from CakeML/remove-zdefine [Oct 06 19:37:34]
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 08 05:15:58 Claimed job
Oct 08 05:16:00 Reusing HOL
Oct 08 05:16:45 Starting developers
Oct 08 05:16:51 Finished developers                                               6s 117MB
Oct 08 05:16:51 Starting developers/bin
Oct 08 05:16:57 Finished developers/bin                                           6s   1GB
Oct 08 05:16:57 Starting compiler/proofs
Oct 08 13:03:36 Resuming compiler/proofs
Oct 08 13:05:43 Finished compiler/proofs                                       2m07s   5GB
Oct 08 13:05:43 Starting compiler/bootstrap/translation
Oct 08 22:05:20 Finished compiler/bootstrap/translation                     8h59m36s  49GB
Oct 08 22:05:20 Starting semantics/ffi
Oct 08 22:05:25 Finished semantics/ffi                                            5s 410MB
Oct 08 22:05:25 Starting semantics
Oct 08 22:05:27 Finished semantics                                                1s  18MB
Oct 08 22:05:27 Starting semantics/proofs
Oct 08 22:05:53 Finished semantics/proofs                                        25s 445MB
Oct 08 22:05:53 Starting semantics/alt_semantics
Oct 08 22:06:16 Finished semantics/alt_semantics                                 23s 563MB
Oct 08 22:06:16 Starting semantics/alt_semantics/proofs
Oct 08 22:17:56 Finished semantics/alt_semantics/proofs                       11m39s   1GB
Oct 08 22:17:56 Starting basis/pure
Oct 08 22:17:58 Finished basis/pure                                               1s  19MB
Oct 08 22:17:58 Starting translator
Oct 08 22:19:39 Finished translator                                            1m41s   1GB
Oct 08 22:19:39 Starting compiler/parsing
Oct 08 22:19:41 Finished compiler/parsing                                         1s  18MB
Oct 08 22:19:41 Starting characteristic
Oct 08 22:19:43 Finished characteristic                                           1s  22MB
Oct 08 22:19:43 Starting translator/monadic
Oct 08 22:19:45 Finished translator/monadic                                       1s  21MB
Oct 08 22:19:45 Starting basis
Oct 08 22:22:19 Finished basis                                                 2m33s   3GB
Oct 08 22:22:19 Starting compiler/inference
Oct 08 22:22:21 Finished compiler/inference                                       1s  29MB
Oct 08 22:22:21 Starting compiler/backend/reg_alloc
Oct 08 22:22:22 Finished compiler/backend/reg_alloc                               1s  21MB
Oct 08 22:22:23 Starting compiler/backend/gc
Oct 08 22:22:25 Finished compiler/backend/gc                                      2s  32MB
Oct 08 22:22:25 Starting compiler/backend
Oct 08 22:22:31 Finished compiler/backend                                         5s 268MB
Oct 08 22:22:31 Starting compiler/encoders/asm
Oct 08 22:22:33 Finished compiler/encoders/asm                                    1s  24MB
Oct 08 22:22:33 Starting compiler/encoders/x64
Oct 08 22:22:35 Finished compiler/encoders/x64                                    1s  22MB
Oct 08 22:22:35 Starting compiler/encoders/arm7
Oct 08 22:22:37 Finished compiler/encoders/arm7                                   1s  24MB
Oct 08 22:22:37 Starting compiler/encoders/arm8
Oct 08 22:22:39 Finished compiler/encoders/arm8                                   1s  27MB
Oct 08 22:22:39 Starting compiler/encoders/arm8_asl
Oct 08 22:25:44 Finished compiler/encoders/arm8_asl                            3m05s   1GB
Oct 08 22:25:44 Starting compiler/encoders/mips
Oct 08 22:25:46 Finished compiler/encoders/mips                                   1s  26MB
Oct 08 22:25:46 Starting compiler/encoders/riscv
Oct 08 22:25:48 Finished compiler/encoders/riscv                                  1s  22MB
Oct 08 22:25:48 Starting compiler/encoders/ag32
Oct 08 22:25:50 Finished compiler/encoders/ag32                                   1s  22MB
Oct 08 22:25:50 Starting compiler/backend/x64
Oct 08 22:25:53 Finished compiler/backend/x64                                     2s  28MB
Oct 08 22:25:53 Starting compiler/backend/arm7
Oct 08 22:25:55 Finished compiler/backend/arm7                                    2s  26MB
Oct 08 22:25:55 Starting compiler/backend/arm8
Oct 08 22:25:58 Finished compiler/backend/arm8                                    2s  27MB
Oct 08 22:25:58 Starting compiler/backend/mips
Oct 08 22:26:00 Finished compiler/backend/mips                                    2s  26MB
Oct 08 22:26:00 Starting compiler/backend/riscv
Oct 08 22:26:02 Finished compiler/backend/riscv                                   2s  27MB
Oct 08 22:26:03 Starting compiler/backend/ag32
Oct 08 22:27:15 Finished compiler/backend/ag32                                 1m12s   1GB
Oct 08 22:27:15 Starting compiler/parsing/proofs
Oct 08 22:27:17 Finished compiler/parsing/proofs                                  1s  17MB
Oct 08 22:27:17 Starting compiler/inference/proofs
Oct 08 22:27:19 Finished compiler/inference/proofs                                1s  22MB
Oct 08 22:27:19 Starting compiler/backend/semantics
Oct 08 22:30:45 Finished compiler/backend/semantics                            3m26s   1GB
Oct 08 22:30:46 Starting compiler/backend/reg_alloc/proofs
Oct 08 22:30:48 Finished compiler/backend/reg_alloc/proofs                        1s  23MB
Oct 08 22:30:48 Starting compiler/backend/proofs
Oct 08 22:31:40 Finished compiler/backend/proofs                                 52s   2GB
Oct 08 22:31:40 Starting compiler/backend/serialiser
Oct 08 22:31:42 Finished compiler/backend/serialiser                              2s  27MB
Oct 08 22:31:42 Starting compiler/encoders/x64/proofs
Oct 08 22:42:26 Finished compiler/encoders/x64/proofs                         10m43s   4GB
Oct 08 22:42:26 Starting compiler/encoders/arm7/proofs
Oct 08 22:56:33 Finished compiler/encoders/arm7/proofs                        14m06s   3GB
Oct 08 22:56:33 Starting compiler/encoders/arm8/proofs
Oct 08 23:04:06 Finished compiler/encoders/arm8/proofs                         7m32s   1GB
Oct 08 23:04:06 Starting compiler/encoders/arm8_asl/proofs
Oct 08 23:21:47 Finished compiler/encoders/arm8_asl/proofs                    17m40s   2GB
Oct 08 23:21:47 Starting compiler/encoders/mips/proofs
Oct 08 23:32:31 Finished compiler/encoders/mips/proofs                        10m44s   3GB
Oct 08 23:32:32 Starting compiler/encoders/riscv/proofs
Oct 08 23:41:44 Finished compiler/encoders/riscv/proofs                        9m11s   1GB
Oct 08 23:41:44 Starting compiler/encoders/ag32/proofs
Oct 08 23:45:02 Finished compiler/encoders/ag32/proofs                         3m18s   1GB
Oct 08 23:45:02 Starting compiler/backend/x64/proofs
Oct 08 23:45:35 Finished compiler/backend/x64/proofs                             32s   2GB
Oct 08 23:45:35 Starting compiler/backend/arm7/proofs
Oct 08 23:46:09 Finished compiler/backend/arm7/proofs                            33s   1GB
Oct 08 23:46:09 Starting compiler/backend/arm8/proofs
Oct 08 23:46:41 Finished compiler/backend/arm8/proofs                            32s   1GB
Oct 08 23:46:41 Starting compiler/backend/arm8_asl
Oct 08 23:47:07 Finished compiler/backend/arm8_asl                               25s   2GB
Oct 08 23:47:07 Starting compiler/backend/mips/proofs
Oct 08 23:47:40 Finished compiler/backend/mips/proofs                            33s   2GB
Oct 08 23:47:40 Starting compiler/backend/riscv/proofs
Oct 08 23:48:17 Finished compiler/backend/riscv/proofs                           36s   2GB
Oct 08 23:48:17 Starting compiler/backend/ag32/proofs
Oct 09 00:03:16 Finished compiler/backend/ag32/proofs                         14m58s   2GB
Oct 09 00:03:16 Starting compiler/backend/cv_compute
Oct 09 00:04:37 Finished compiler/backend/cv_compute                           1m20s   2GB
Oct 09 00:04:37 Starting cv_translator
Oct 09 00:25:20 Finished cv_translator                                        20m42s   8GB
Oct 09 00:25:20 Starting candle/set-theory
Oct 09 00:25:58 Finished candle/set-theory                                       38s 947MB
Oct 09 00:25:58 Starting candle/syntax-lib
Oct 09 00:26:00 Finished candle/syntax-lib                                        1s  18MB
Oct 09 00:26:00 Starting candle/standard/syntax
Oct 09 00:26:13 Finished candle/standard/syntax                                  13s 837MB
Oct 09 00:26:13 Starting candle/standard/semantics
Oct 09 00:28:26 Finished candle/standard/semantics                             2m12s   1GB
Oct 09 00:28:26 Starting candle/standard/monadic
Oct 09 00:28:28 Finished candle/standard/monadic                                  1s  20MB
Oct 09 00:28:28 Starting candle/standard/ml_kernel
Oct 09 00:30:26 Finished candle/standard/ml_kernel                             1m57s   3GB
Oct 09 00:30:26 Starting candle/overloading/syntax
Oct 09 00:33:57 Finished candle/overloading/syntax                             3m31s   1GB
Oct 09 00:33:57 Starting candle/overloading/semantics
Oct 09 00:46:35 Finished candle/overloading/semantics                         12m37s   3GB
Oct 09 00:46:35 Starting candle/overloading/monadic
Oct 09 00:49:06 Finished candle/overloading/monadic                            2m30s   1GB
Oct 09 00:49:06 Starting candle/overloading/ml_kernel
Oct 09 00:57:19 Finished candle/overloading/ml_kernel                          8m13s   4GB
Oct 09 00:57:20 Starting candle/overloading/ml_checker
Oct 09 01:00:38 Finished candle/overloading/ml_checker                         3m17s   5GB
Oct 09 01:00:38 Starting candle/prover
Oct 09 01:11:10 Finished candle/prover                                        10m32s   4GB
Oct 09 01:11:10 Starting pancake
Oct 09 01:11:36 Finished pancake                                                 25s 833MB
Oct 09 01:11:36 Starting pancake/ffi
Oct 09 01:11:36 Finished pancake/ffi                                              0s  13MB
Oct 09 01:11:36 Starting pancake/semantics
Oct 09 01:14:01 Finished pancake/semantics                                     2m24s   1GB
Oct 09 01:14:01 Starting pancake/parser
Oct 09 01:14:27 Finished pancake/parser                                          26s 419MB
Oct 09 01:14:27 Starting pancake/proofs
Oct 09 01:32:59 Finished pancake/proofs                                       18m31s   3GB
Oct 09 01:32:59 Starting compiler/dafny
Oct 09 01:35:25 Finished compiler/dafny                                        2m25s   8GB
Oct 09 01:35:25 Starting compiler/dafny/translation
Oct 09 02:05:39 Finished compiler/dafny/translation                           30m13s  14GB
Oct 09 02:05:39 Starting compiler/dafny/compilation
Oct 09 02:09:04 Finished compiler/dafny/compilation                            3m25s  10GB
Oct 09 02:09:04 Starting compiler/dafny/semantics
Oct 09 02:09:42 Finished compiler/dafny/semantics                                37s 824MB
Oct 09 02:09:42 Starting characteristic/examples
Oct 09 02:11:11 Finished characteristic/examples                               1m29s   2GB
Oct 09 02:11:12 Starting tutorial/solutions
Oct 09 02:13:58 Finished tutorial/solutions                                    2m46s   3GB
Oct 09 02:13:59 Starting translator/monadic/examples
Oct 09 02:17:41 Finished translator/monadic/examples                           3m42s   3GB
Oct 09 02:17:41 Starting examples
Oct 09 02:32:02 Finished examples                                             14m20s   3GB
Oct 09 02:32:02 Starting examples/compilation/x64
Oct 09 02:41:04 Finished examples/compilation/x64                              9m01s   5GB
Oct 09 02:41:04 Starting examples/compilation/x64/proofs
Oct 09 02:44:01 Finished examples/compilation/x64/proofs                       2m56s   4GB
Oct 09 02:44:01 Starting examples/compilation/ag32
Oct 09 02:46:18 Finished examples/compilation/ag32                             2m17s   3GB
Oct 09 02:46:19 Starting examples/compilation/ag32/proofs
Oct 09 02:47:29 Finished examples/compilation/ag32/proofs                      1m09s   5GB
Oct 09 02:47:29 Starting examples/compilation/to_word
Oct 09 02:50:59 Finished examples/compilation/to_word                          3m29s   5GB
Oct 09 02:50:59 Starting examples/lpr_checker
Oct 09 02:51:30 Finished examples/lpr_checker                                    31s 845MB
Oct 09 02:51:30 Starting examples/lpr_checker/array
Oct 09 03:19:31 Finished examples/lpr_checker/array                           28m00s   5GB
Oct 09 03:19:31 Starting examples/lpr_checker/array/compilation
Oct 09 03:22:14 Finished examples/lpr_checker/array/compilation                2m43s   7GB
Oct 09 03:22:14 Starting examples/lpr_checker/array/compilation/proofs
Oct 09 03:23:40 Finished examples/lpr_checker/array/compilation/proofs         1m25s   5GB
Oct 09 03:23:40 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 09 03:24:51 Finished examples/lpr_checker/array/compilation/proofsARM8     1m11s   5GB
Oct 09 03:24:51 Starting examples/xlrup_checker
Oct 09 03:25:29 Finished examples/xlrup_checker                                  37s 848MB
Oct 09 03:25:29 Starting examples/xlrup_checker/array
Oct 09 03:39:57 Finished examples/xlrup_checker/array                         14m27s   3GB
Oct 09 03:39:57 Starting examples/xlrup_checker/array/compilation
Oct 09 03:41:22 Finished examples/xlrup_checker/array/compilation              1m24s   5GB
Oct 09 03:41:22 Starting examples/xlrup_checker/array/compilation/proofs
Oct 09 03:42:25 Finished examples/xlrup_checker/array/compilation/proofs       1m02s   4GB
Oct 09 03:42:25 Starting examples/pseudo_bool
Oct 09 03:43:57 Finished examples/pseudo_bool                                  1m31s   1GB
Oct 09 03:43:57 Starting examples/pseudo_bool/cnf_encoding
Oct 09 03:44:28 Finished examples/pseudo_bool/cnf_encoding                       30s 945MB
Oct 09 03:44:28 Starting examples/pseudo_bool/graph_encoding
Oct 09 03:45:15 Finished examples/pseudo_bool/graph_encoding                     47s 969MB
Oct 09 03:45:15 Starting examples/pseudo_bool/array
Oct 09 04:51:31 Finished examples/pseudo_bool/array                         1h06m15s  10GB
Oct 09 04:51:31 Starting examples/pseudo_bool/array/compilation
Oct 09 05:06:21 Finished examples/pseudo_bool/array/compilation               14m50s  25GB
Oct 09 05:06:21 Starting examples/pseudo_bool/array/compilation/proofs
Oct 09 05:09:15 Finished examples/pseudo_bool/array/compilation/proofs         2m54s   6GB
Oct 09 05:09:15 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 09 05:10:35 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m19s   7GB
Oct 09 05:10:35 Starting examples/opentheory
Oct 09 05:19:40 Finished examples/opentheory                                   9m04s   3GB
Oct 09 05:19:40 Starting examples/opentheory
Oct 09 05:19:42 Finished examples/opentheory                                      1s  26MB
Oct 09 05:19:42 Starting examples/opentheory/compilation
Oct 09 05:21:45 Finished examples/opentheory/compilation                       2m03s   7GB
Oct 09 05:21:45 Starting examples/opentheory/compilation/proofs
Oct 09 05:22:52 Finished examples/opentheory/compilation/proofs                1m06s   5GB
Oct 09 05:22:52 Starting examples/opentheory/compilation/ag32
Oct 09 05:24:56 Finished examples/opentheory/compilation/ag32                  2m04s   5GB
Oct 09 05:24:57 Starting examples/opentheory/compilation/ag32/proofs
Oct 09 05:26:39 Finished examples/opentheory/compilation/ag32/proofs           1m42s   6GB
Oct 09 05:26:39 Starting examples/sat_encodings
Oct 09 05:27:47 Finished examples/sat_encodings                                1m07s 612MB
Oct 09 05:27:47 Starting examples/sat_encodings/case_studies
Oct 09 05:29:42 Finished examples/sat_encodings/case_studies                   1m54s   1GB
Oct 09 05:29:42 Starting examples/sat_encodings/translation
Oct 09 05:33:46 Finished examples/sat_encodings/translation                    4m04s   1GB
Oct 09 05:33:46 Starting examples/sat_encodings/translation/compilation
Oct 09 05:36:21 Finished examples/sat_encodings/translation/compilation        2m34s   5GB
Oct 09 05:36:21 Starting examples/deflate
Oct 09 05:36:53 Finished examples/deflate                                        31s 478MB
Oct 09 05:36:53 Starting examples/deflate/translation
Oct 09 05:38:01 Finished examples/deflate/translation                          1m07s   1GB
Oct 09 05:38:01 Starting examples/deflate/translation/compilation
Oct 09 05:39:10 Finished examples/deflate/translation/compilation              1m09s   5GB
Oct 09 05:39:11 Starting examples/vipr
Oct 09 05:43:07 Finished examples/vipr                                         3m56s   5GB
Oct 09 05:43:07 Starting examples/vipr/compilation
Oct 09 05:44:22 Finished examples/vipr/compilation                             1m15s   4GB
Oct 09 05:44:23 Starting translator/okasaki-examples
Oct 09 05:48:57 Finished translator/okasaki-examples                           4m34s   1GB
Oct 09 05:48:57 Starting translator/other-examples
Oct 09 05:49:55 Finished translator/other-examples                               58s   2GB
Oct 09 05:49:55 Starting compiler/parsing/tests
Oct 09 05:50:32 Finished compiler/parsing/tests                                  37s   1GB
Oct 09 05:50:33 Starting compiler/inference/tests
Oct 09 05:51:06 Finished compiler/inference/tests                                33s   2GB
Oct 09 05:51:06 Starting compiler/printing/test
Oct 09 05:52:38 Finished compiler/printing/test                                1m31s   2GB
Oct 09 05:52:38 Starting icing/flover
Oct 09 06:38:54 Finished icing/flover                                         46m15s   2GB
Oct 09 06:38:54 Starting icing/
Oct 09 07:08:45 Finished icing/                                               29m51s   3GB
Oct 09 07:08:45 Starting icing/examples
Oct 09 07:10:28 Finished icing/examples                                        1m42s   4GB
Oct 09 07:10:28 Starting compiler/repl
Oct 09 07:19:36 Finished compiler/repl                                         9m07s   8GB
Oct 09 07:19:36 Starting unverified/sexpr-bootstrap/x64/64
Oct 09 07:35:55 Finished unverified/sexpr-bootstrap/x64/64                    16m19s  18GB
Oct 09 07:35:55 Starting unverified/sexpr-bootstrap/x64/32
Oct 09 07:49:03 Finished unverified/sexpr-bootstrap/x64/32                    13m07s  18GB
Oct 09 07:49:03 Starting compiler/benchmarks
Oct 09 08:04:37 Finished compiler/benchmarks                                  15m34s   2GB
Oct 09 08:04:37 Starting compiler/bootstrap/compilation/x64/64
Oct 09 08:42:12 Finished compiler/bootstrap/compilation/x64/64                37m34s  63GB
Oct 09 08:42:12 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 09 09:07:15 Finished compiler/bootstrap/compilation/x64/64/proofs         25m02s  49GB
Oct 09 09:07:15 Starting compiler/bootstrap/compilation/x64/32
Oct 09 09:47:12 Finished compiler/bootstrap/compilation/x64/32                39m56s  64GB
Oct 09 09:47:12 Starting compiler/bootstrap/compilation/x64/32/proofs
Oct 09 09:51:01 Finished compiler/bootstrap/compilation/x64/32/proofs          3m49s  23GB
Oct 09 09:51:01 Starting compiler/bootstrap/compilation/arm8/64
Oct 09 10:42:59 Finished compiler/bootstrap/compilation/arm8/64               51m57s  64GB
Oct 09 10:42:59 Starting compiler/bootstrap/compilation/arm8/64/proofs
Oct 09 10:50:22 Finished compiler/bootstrap/compilation/arm8/64/proofs         7m22s  22GB
Oct 09 10:50:22 Starting compiler/bootstrap/compilation/ag32/32
Oct 09 11:27:42 Finished compiler/bootstrap/compilation/ag32/32               37m20s  64GB
Oct 09 11:27:43 Starting compiler/bootstrap/compilation/ag32/32/proofs
Oct 09 11:34:36 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m53s  21GB
Oct 09 11:34:36 SUCCESS