Job 2600

CakeML:5fd08a4642e821e24b09245447b99f5b21e74664
  Modernise diffScript [Sep 12 11:49:16]
#1052 (diff)
Merging into:7b614da7b56c9d04e55ecc20f0c22bdd8d7866e7
  Fix a broken proof [Sep 11 11:01:55]
HOL:7bf55e0eb37d0d68268a5b6c2d55dc2895fd6361
  Fix bug in reduceLib.NOT_CONV [Sep 09 04:53:02]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Sep 12 17:21:37 Claimed job
Sep 12 17:21:38 Reusing HOL
Sep 12 17:22:24 Starting developers
Sep 12 17:22:29 Finished developers                                               5s 152MB
Sep 12 17:22:30 Starting developers/bin
Sep 12 17:22:36 Finished developers/bin                                           5s   1GB
Sep 12 17:22:36 Starting compiler/proofs
Sep 12 19:20:31 Finished compiler/proofs                                    1h57m55s  10GB
Sep 12 19:20:31 Starting compiler/bootstrap/translation
Sep 13 04:45:36 Finished compiler/bootstrap/translation                     9h25m04s  48GB
Sep 13 04:45:36 Starting semantics/ffi
Sep 13 04:45:43 Finished semantics/ffi                                            6s 240MB
Sep 13 04:45:43 Starting semantics
Sep 13 04:45:45 Finished semantics                                                1s  19MB
Sep 13 04:45:45 Starting semantics/proofs
Sep 13 04:46:11 Finished semantics/proofs                                        26s 414MB
Sep 13 04:46:11 Starting semantics/alt_semantics
Sep 13 04:46:38 Finished semantics/alt_semantics                                 26s 579MB
Sep 13 04:46:38 Starting semantics/alt_semantics/proofs
Sep 13 04:59:20 Finished semantics/alt_semantics/proofs                       12m41s   1GB
Sep 13 04:59:20 Starting basis/pure
Sep 13 04:59:22 Finished basis/pure                                               1s  18MB
Sep 13 04:59:22 Starting translator
Sep 13 05:01:29 Finished translator                                            2m07s   2GB
Sep 13 05:01:29 Starting compiler/parsing
Sep 13 05:01:31 Finished compiler/parsing                                         1s  24MB
Sep 13 05:01:31 Starting characteristic
Sep 13 05:01:33 Finished characteristic                                           2s  21MB
Sep 13 05:01:33 Starting translator/monadic
Sep 13 05:01:35 Finished translator/monadic                                       1s  23MB
Sep 13 05:01:35 Starting basis
Sep 13 05:04:26 Finished basis                                                 2m50s   3GB
Sep 13 05:04:26 Starting compiler/inference
Sep 13 05:04:28 Finished compiler/inference                                       1s  23MB
Sep 13 05:04:28 Starting compiler/backend/reg_alloc
Sep 13 05:04:29 Finished compiler/backend/reg_alloc                               1s  24MB
Sep 13 05:04:29 Starting compiler/backend/gc
Sep 13 05:04:32 Finished compiler/backend/gc                                      2s  24MB
Sep 13 05:04:32 Starting compiler/backend
Sep 13 05:04:38 Finished compiler/backend                                         5s 296MB
Sep 13 05:04:38 Starting compiler/encoders/asm
Sep 13 05:04:40 Finished compiler/encoders/asm                                    1s  25MB
Sep 13 05:04:40 Starting compiler/encoders/x64
Sep 13 05:04:42 Finished compiler/encoders/x64                                    1s  28MB
Sep 13 05:04:42 Starting compiler/encoders/arm7
Sep 13 05:04:44 Finished compiler/encoders/arm7                                   1s  22MB
Sep 13 05:04:44 Starting compiler/encoders/arm8
Sep 13 05:04:46 Finished compiler/encoders/arm8                                   1s  22MB
Sep 13 05:04:46 Starting compiler/encoders/arm8_asl
Sep 13 05:08:01 Finished compiler/encoders/arm8_asl                            3m14s   1GB
Sep 13 05:08:01 Starting compiler/encoders/mips
Sep 13 05:08:03 Finished compiler/encoders/mips                                   1s  25MB
Sep 13 05:08:03 Starting compiler/encoders/riscv
Sep 13 05:08:05 Finished compiler/encoders/riscv                                  1s  26MB
Sep 13 05:08:05 Starting compiler/encoders/ag32
Sep 13 05:08:07 Finished compiler/encoders/ag32                                   1s  22MB
Sep 13 05:08:07 Starting compiler/backend/x64
Sep 13 05:08:09 Finished compiler/backend/x64                                     2s  25MB
Sep 13 05:08:09 Starting compiler/backend/arm7
Sep 13 05:08:12 Finished compiler/backend/arm7                                    2s  25MB
Sep 13 05:08:12 Starting compiler/backend/arm8
Sep 13 05:08:14 Finished compiler/backend/arm8                                    2s  24MB
Sep 13 05:08:14 Starting compiler/backend/mips
Sep 13 05:08:16 Finished compiler/backend/mips                                    2s  27MB
Sep 13 05:08:16 Starting compiler/backend/riscv
Sep 13 05:08:19 Finished compiler/backend/riscv                                   2s  29MB
Sep 13 05:08:19 Starting compiler/backend/ag32
Sep 13 05:09:52 Finished compiler/backend/ag32                                 1m33s   1GB
Sep 13 05:09:52 Starting compiler/parsing/proofs
Sep 13 05:09:54 Finished compiler/parsing/proofs                                  1s  18MB
Sep 13 05:09:54 Starting compiler/inference/proofs
Sep 13 05:09:56 Finished compiler/inference/proofs                                1s  22MB
Sep 13 05:09:56 Starting compiler/backend/semantics
Sep 13 05:13:38 Finished compiler/backend/semantics                            3m41s   1GB
Sep 13 05:13:38 Starting compiler/backend/reg_alloc/proofs
Sep 13 05:13:40 Finished compiler/backend/reg_alloc/proofs                        1s  35MB
Sep 13 05:13:40 Starting compiler/backend/proofs
Sep 13 05:14:39 Finished compiler/backend/proofs                                 59s   2GB
Sep 13 05:14:39 Starting compiler/backend/serialiser
Sep 13 05:14:42 Finished compiler/backend/serialiser                              2s  26MB
Sep 13 05:14:42 Starting compiler/encoders/x64/proofs
Sep 13 05:26:05 Finished compiler/encoders/x64/proofs                         11m23s   5GB
Sep 13 05:26:05 Starting compiler/encoders/arm7/proofs
Sep 13 05:40:15 Finished compiler/encoders/arm7/proofs                        14m10s   4GB
Sep 13 05:40:15 Starting compiler/encoders/arm8/proofs
Sep 13 05:47:57 Finished compiler/encoders/arm8/proofs                         7m41s   1GB
Sep 13 05:47:57 Starting compiler/encoders/arm8_asl/proofs
Sep 13 06:06:08 Finished compiler/encoders/arm8_asl/proofs                    18m10s   2GB
Sep 13 06:06:08 Starting compiler/encoders/mips/proofs
Sep 13 06:17:06 Finished compiler/encoders/mips/proofs                        10m58s   2GB
Sep 13 06:17:06 Starting compiler/encoders/riscv/proofs
Sep 13 06:26:23 Finished compiler/encoders/riscv/proofs                        9m17s   2GB
Sep 13 06:26:23 Starting compiler/encoders/ag32/proofs
Sep 13 06:29:41 Finished compiler/encoders/ag32/proofs                         3m18s   1GB
Sep 13 06:29:42 Starting compiler/backend/x64/proofs
Sep 13 06:30:14 Finished compiler/backend/x64/proofs                             32s   1GB
Sep 13 06:30:15 Starting compiler/backend/arm7/proofs
Sep 13 06:30:49 Finished compiler/backend/arm7/proofs                            34s   1GB
Sep 13 06:30:49 Starting compiler/backend/arm8/proofs
Sep 13 06:31:23 Finished compiler/backend/arm8/proofs                            33s   1GB
Sep 13 06:31:23 Starting compiler/backend/arm8_asl
Sep 13 06:31:47 Finished compiler/backend/arm8_asl                               24s   2GB
Sep 13 06:31:48 Starting compiler/backend/mips/proofs
Sep 13 06:32:23 Finished compiler/backend/mips/proofs                            35s   2GB
Sep 13 06:32:23 Starting compiler/backend/riscv/proofs
Sep 13 06:33:01 Finished compiler/backend/riscv/proofs                           37s   2GB
Sep 13 06:33:01 Starting compiler/backend/ag32/proofs
Sep 13 06:48:08 Finished compiler/backend/ag32/proofs                         15m06s   3GB
Sep 13 06:48:08 Starting compiler/backend/cv_compute
Sep 13 06:49:32 Finished compiler/backend/cv_compute                           1m23s   2GB
Sep 13 06:49:32 Starting cv_translator
Sep 13 07:10:05 Finished cv_translator                                        20m32s   7GB
Sep 13 07:10:05 Starting candle/set-theory
Sep 13 07:10:48 Finished candle/set-theory                                       43s   1GB
Sep 13 07:10:48 Starting candle/syntax-lib
Sep 13 07:10:50 Finished candle/syntax-lib                                        1s  21MB
Sep 13 07:10:50 Starting candle/standard/syntax
Sep 13 07:11:04 Finished candle/standard/syntax                                  13s 868MB
Sep 13 07:11:04 Starting candle/standard/semantics
Sep 13 07:13:18 Finished candle/standard/semantics                             2m13s   1GB
Sep 13 07:13:18 Starting candle/standard/monadic
Sep 13 07:13:20 Finished candle/standard/monadic                                  1s  22MB
Sep 13 07:13:20 Starting candle/standard/ml_kernel
Sep 13 07:15:03 Finished candle/standard/ml_kernel                             1m43s   2GB
Sep 13 07:15:03 Starting candle/overloading/syntax
Sep 13 07:18:37 Finished candle/overloading/syntax                             3m33s   1GB
Sep 13 07:18:37 Starting candle/overloading/semantics
Sep 13 07:31:00 Finished candle/overloading/semantics                         12m22s   4GB
Sep 13 07:31:00 Starting candle/overloading/monadic
Sep 13 07:33:45 Finished candle/overloading/monadic                            2m45s   1GB
Sep 13 07:33:46 Starting candle/overloading/ml_kernel
Sep 13 07:42:06 Finished candle/overloading/ml_kernel                          8m20s   4GB
Sep 13 07:42:06 Starting candle/overloading/ml_checker
Sep 13 07:44:47 Finished candle/overloading/ml_checker                         2m41s   3GB
Sep 13 07:44:47 Starting candle/prover
Sep 13 07:55:24 Finished candle/prover                                        10m36s   4GB
Sep 13 07:55:24 Starting pancake
Sep 13 07:55:48 Finished pancake                                                 23s 703MB
Sep 13 07:55:48 Starting pancake/ffi
Sep 13 07:55:49 Finished pancake/ffi                                              0s  13MB
Sep 13 07:55:49 Starting pancake/semantics
Sep 13 07:58:14 Finished pancake/semantics                                     2m25s   1GB
Sep 13 07:58:14 Starting pancake/parser
Sep 13 07:58:39 Finished pancake/parser                                          24s 502MB
Sep 13 07:58:39 Starting pancake/proofs
Sep 13 08:16:57 Finished pancake/proofs                                       18m17s   6GB
Sep 13 08:16:57 Starting characteristic/examples
Sep 13 08:18:28 Finished characteristic/examples                               1m31s   2GB
Sep 13 08:18:29 Starting tutorial/solutions
Sep 13 08:21:22 Finished tutorial/solutions                                    2m52s   4GB
Sep 13 08:21:22 Starting translator/monadic/examples
Sep 13 08:25:09 Finished translator/monadic/examples                           3m47s   3GB
Sep 13 08:25:09 Starting examples
Sep 13 08:40:00 Finished examples                                             14m50s   4GB
Sep 13 08:40:00 Starting examples/compilation/x64
Sep 13 08:49:03 Finished examples/compilation/x64                              9m03s   6GB
Sep 13 08:49:03 Starting examples/compilation/x64/proofs
Sep 13 08:52:01 Finished examples/compilation/x64/proofs                       2m57s   4GB
Sep 13 08:52:01 Starting examples/compilation/ag32
Sep 13 08:54:18 Finished examples/compilation/ag32                             2m16s   2GB
Sep 13 08:54:18 Starting examples/compilation/ag32/proofs
Sep 13 08:55:29 Finished examples/compilation/ag32/proofs                      1m10s   5GB
Sep 13 08:55:29 Starting examples/compilation/to_word
Sep 13 08:58:58 Finished examples/compilation/to_word                          3m28s   7GB
Sep 13 08:58:58 Starting examples/lpr_checker
Sep 13 08:59:38 Finished examples/lpr_checker                                    39s 659MB
Sep 13 08:59:38 Starting examples/lpr_checker/array
Sep 13 09:27:48 Finished examples/lpr_checker/array                           28m10s   4GB
Sep 13 09:27:48 Starting examples/lpr_checker/array/compilation
Sep 13 09:30:28 Finished examples/lpr_checker/array/compilation                2m39s   8GB
Sep 13 09:30:28 Starting examples/lpr_checker/array/compilation/proofs
Sep 13 09:31:52 Finished examples/lpr_checker/array/compilation/proofs         1m23s   6GB
Sep 13 09:31:53 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 13 09:33:15 Finished examples/lpr_checker/array/compilation/proofsARM8     1m21s   5GB
Sep 13 09:33:15 Starting examples/xlrup_checker
Sep 13 09:33:53 Finished examples/xlrup_checker                                  37s 850MB
Sep 13 09:33:53 Starting examples/xlrup_checker/array
Sep 13 09:48:21 Finished examples/xlrup_checker/array                         14m28s   3GB
Sep 13 09:48:21 Starting examples/xlrup_checker/array/compilation
Sep 13 09:49:44 Finished examples/xlrup_checker/array/compilation              1m23s   5GB
Sep 13 09:49:45 Starting examples/xlrup_checker/array/compilation/proofs
Sep 13 09:50:52 Finished examples/xlrup_checker/array/compilation/proofs       1m07s   5GB
Sep 13 09:50:52 Starting examples/pseudo_bool
Sep 13 09:52:24 Finished examples/pseudo_bool                                  1m31s   1GB
Sep 13 09:52:24 Starting examples/pseudo_bool/cnf_encoding
Sep 13 09:52:54 Finished examples/pseudo_bool/cnf_encoding                       30s 722MB
Sep 13 09:52:54 Starting examples/pseudo_bool/graph_encoding
Sep 13 09:53:42 Finished examples/pseudo_bool/graph_encoding                     47s 995MB
Sep 13 09:53:42 Starting examples/pseudo_bool/array
Sep 13 11:00:12 Finished examples/pseudo_bool/array                         1h06m30s   7GB
Sep 13 11:00:12 Starting examples/pseudo_bool/array/compilation
Sep 13 11:14:57 Finished examples/pseudo_bool/array/compilation               14m44s  29GB
Sep 13 11:14:57 Starting examples/pseudo_bool/array/compilation/proofs
Sep 13 11:18:00 Finished examples/pseudo_bool/array/compilation/proofs         3m02s   7GB
Sep 13 11:18:00 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 13 11:19:21 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m20s   7GB
Sep 13 11:19:21 Starting examples/opentheory
Sep 13 11:28:36 Finished examples/opentheory                                   9m15s   2GB
Sep 13 11:28:36 Starting examples/opentheory
Sep 13 11:28:38 Finished examples/opentheory                                      1s  32MB
Sep 13 11:28:38 Starting examples/opentheory/compilation
Sep 13 11:30:41 Finished examples/opentheory/compilation                       2m02s   5GB
Sep 13 11:30:41 Starting examples/opentheory/compilation/proofs
Sep 13 11:31:50 Finished examples/opentheory/compilation/proofs                1m08s   4GB
Sep 13 11:31:50 Starting examples/opentheory/compilation/ag32
Sep 13 11:33:52 Finished examples/opentheory/compilation/ag32                  2m02s   5GB
Sep 13 11:33:52 Starting examples/opentheory/compilation/ag32/proofs
Sep 13 11:35:34 Finished examples/opentheory/compilation/ag32/proofs           1m42s   6GB
Sep 13 11:35:35 Starting examples/sat_encodings
Sep 13 11:36:42 Finished examples/sat_encodings                                1m07s 635MB
Sep 13 11:36:42 Starting examples/sat_encodings/case_studies
Sep 13 11:38:35 Finished examples/sat_encodings/case_studies                   1m53s   1GB
Sep 13 11:38:35 Starting examples/sat_encodings/translation
Sep 13 11:42:36 Finished examples/sat_encodings/translation                    4m00s   1GB
Sep 13 11:42:36 Starting examples/sat_encodings/translation/compilation
Sep 13 11:45:01 Finished examples/sat_encodings/translation/compilation        2m24s   6GB
Sep 13 11:45:01 Starting examples/deflate
Sep 13 11:45:33 Finished examples/deflate                                        31s 469MB
Sep 13 11:45:33 Starting examples/deflate/translation
Sep 13 11:46:42 Finished examples/deflate/translation                          1m08s   1GB
Sep 13 11:46:42 Starting examples/deflate/translation/compilation
Sep 13 11:47:53 Finished examples/deflate/translation/compilation              1m10s   3GB
Sep 13 11:47:53 Starting examples/vipr
Sep 13 11:51:47 Finished examples/vipr                                         3m54s   5GB
Sep 13 11:51:47 Starting examples/vipr/compilation
Sep 13 11:53:03 Finished examples/vipr/compilation                             1m15s   4GB
Sep 13 11:53:03 Starting translator/okasaki-examples
Sep 13 11:57:46 Finished translator/okasaki-examples                           4m43s   1GB
Sep 13 11:57:46 Starting translator/other-examples
Sep 13 11:58:50 Finished translator/other-examples                             1m03s   1GB
Sep 13 11:58:50 Starting compiler/parsing/tests
Sep 13 11:59:26 Finished compiler/parsing/tests                                  36s 872MB
Sep 13 11:59:27 Starting compiler/inference/tests
Sep 13 12:00:00 Finished compiler/inference/tests                                33s   2GB
Sep 13 12:00:00 Starting compiler/printing/test
Sep 13 12:01:31 Finished compiler/printing/test                                1m30s   2GB
Sep 13 12:01:31 Starting icing/flover
Sep 13 12:47:40 Finished icing/flover                                         46m08s   2GB
Sep 13 12:47:40 Starting icing/
Sep 13 13:17:43 Finished icing/                                               30m02s   3GB
Sep 13 13:17:43 Starting icing/examples
Sep 13 13:19:25 Finished icing/examples                                        1m42s   4GB
Sep 13 13:19:25 Starting compiler/repl
Sep 13 13:28:25 Finished compiler/repl                                         8m59s   5GB
Sep 13 13:28:25 Starting unverified/sexpr-bootstrap/x64/64
Sep 13 13:44:44 Finished unverified/sexpr-bootstrap/x64/64                    16m19s  16GB
Sep 13 13:44:44 Starting unverified/sexpr-bootstrap/x64/32
Sep 13 13:57:54 Finished unverified/sexpr-bootstrap/x64/32                    13m09s  15GB
Sep 13 13:57:54 Starting compiler/benchmarks
Sep 13 14:13:33 Finished compiler/benchmarks                                  15m39s   2GB
Sep 13 14:13:33 Starting compiler/bootstrap/compilation/x64/64
Sep 13 14:55:47 Finished compiler/bootstrap/compilation/x64/64                42m13s  63GB
Sep 13 14:55:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 13 15:21:05 Finished compiler/bootstrap/compilation/x64/64/proofs         25m17s  47GB
Sep 13 15:21:05 Starting compiler/bootstrap/compilation/x64/32
Sep 13 16:00:44 Finished compiler/bootstrap/compilation/x64/32                39m38s  64GB
Sep 13 16:00:44 Starting compiler/bootstrap/compilation/x64/32/proofs
Sep 13 16:06:40 Finished compiler/bootstrap/compilation/x64/32/proofs          5m56s  18GB
Sep 13 16:06:40 Starting compiler/bootstrap/compilation/arm8/64
Sep 13 16:58:02 Finished compiler/bootstrap/compilation/arm8/64               51m21s  64GB
Sep 13 16:58:02 Starting compiler/bootstrap/compilation/arm8/64/proofs
Sep 13 17:03:08 Finished compiler/bootstrap/compilation/arm8/64/proofs         5m05s  31GB
Sep 13 17:03:08 Starting compiler/bootstrap/compilation/ag32/32
Sep 13 17:44:36 Finished compiler/bootstrap/compilation/ag32/32               41m27s  64GB
Sep 13 17:44:36 Starting compiler/bootstrap/compilation/ag32/32/proofs
Sep 13 17:51:19 Finished compiler/bootstrap/compilation/ag32/32/proofs         6m42s  19GB
Sep 13 17:51:19 SUCCESS