Job 2829

CakeML:9aa9f0b16f66815a9423d8ec6b6efbcf85455f90
  [mlstring] Add common prefix/suffix theorems [May 09 13:37:28]
#1174 (mlstring-common-prefix-suffix)
Merging into:63412ddda50a374aecb96ebb92c6e16501c63332
  Merge pull request #1173 from CakeML/extracleans-in-developers [May 14 05:30:33]
HOL:37389f39aa1f331637b2525ad92fdba43703a13e
  Progress with defining connected component notion within fsgraph [May 12 07:08:10]
Machine:pavlova

May 14 09:44:47 Claimed job
May 14 09:44:56 Building HOL
May 14 09:55:35 Starting developers
May 14 09:55:39 Finished developers                                               3s 184MB
May 14 09:55:40 Starting developers/bin
May 14 09:55:46 Finished developers/bin                                           4s 591MB
May 14 09:55:46 Starting misc
May 14 09:56:42 Finished misc                                                    55s   2GB
May 14 09:56:43 Starting compiler/proofs
May 14 11:32:08 Finished compiler/proofs                                    1h35m22s  28GB
May 14 11:32:09 Starting compiler/bootstrap/translation
May 14 17:13:13 Finished compiler/bootstrap/translation                     5h41m02s  85GB
May 14 17:13:14 Starting semantics/ffi
May 14 17:13:23 Finished semantics/ffi                                            8s 549MB
May 14 17:13:24 Starting semantics
May 14 17:13:25 Finished semantics                                                0s  55MB
May 14 17:13:26 Starting semantics/proofs
May 14 17:13:49 Finished semantics/proofs                                        22s 870MB
May 14 17:13:50 Starting semantics/alt_semantics
May 14 17:14:10 Finished semantics/alt_semantics                                 19s 869MB
May 14 17:14:11 Starting semantics/alt_semantics/proofs
May 14 17:24:30 Finished semantics/alt_semantics/proofs                       10m17s   2GB
May 14 17:24:31 Starting basis/pure
May 14 17:24:33 Finished basis/pure                                               0s  93MB
May 14 17:24:34 Starting translator
May 14 17:26:06 Finished translator                                            1m31s   3GB
May 14 17:26:07 Starting compiler/parsing
May 14 17:26:09 Finished compiler/parsing                                         0s  59MB
May 14 17:26:10 Starting characteristic
May 14 17:26:12 Finished characteristic                                           1s 116MB
May 14 17:26:12 Starting translator/monadic
May 14 17:26:14 Finished translator/monadic                                       1s 115MB
May 14 17:26:15 Starting translator/monadic/monad_base
May 14 17:26:17 Finished translator/monadic/monad_base                            0s  51MB
May 14 17:26:18 Starting basis
May 14 17:28:44 Finished basis                                                 2m25s   4GB
May 14 17:28:45 Starting compiler
May 14 17:28:48 Finished compiler                                                 1s 210MB
May 14 17:28:49 Starting compiler/inference
May 14 17:28:51 Finished compiler/inference                                       1s 115MB
May 14 17:28:52 Starting compiler/backend/reg_alloc
May 14 17:28:53 Finished compiler/backend/reg_alloc                               0s  56MB
May 14 17:28:54 Starting compiler/backend/gc
May 14 17:28:56 Finished compiler/backend/gc                                      1s 142MB
May 14 17:28:57 Starting compiler/backend
May 14 17:29:02 Finished compiler/backend                                         4s 267MB
May 14 17:29:03 Starting compiler/encoders/asm
May 14 17:29:04 Finished compiler/encoders/asm                                    0s  84MB
May 14 17:29:05 Starting compiler/encoders/x64
May 14 17:29:07 Finished compiler/encoders/x64                                    0s  84MB
May 14 17:29:08 Starting compiler/encoders/arm7
May 14 17:29:09 Finished compiler/encoders/arm7                                   0s  84MB
May 14 17:29:10 Starting compiler/encoders/arm8
May 14 17:29:12 Finished compiler/encoders/arm8                                   0s  83MB
May 14 17:29:13 Starting compiler/encoders/arm8_asl
May 14 19:31:48 Finished compiler/encoders/arm8_asl                         2h02m34s  42GB
May 14 19:31:49 Starting compiler/encoders/mips
May 14 19:31:50 Finished compiler/encoders/mips                                   0s  88MB
May 14 19:31:51 Starting compiler/encoders/riscv
May 14 19:31:53 Finished compiler/encoders/riscv                                  0s  84MB
May 14 19:31:54 Starting compiler/encoders/ag32
May 14 19:31:55 Finished compiler/encoders/ag32                                   0s  83MB
May 14 19:31:56 Starting compiler/encoders/tests
May 14 19:31:58 Finished compiler/encoders/tests                                  0s 113MB
May 14 19:31:59 Starting compiler/encoders/monadic_enc
May 14 19:32:01 Finished compiler/encoders/monadic_enc                            1s 135MB
May 14 19:32:02 Starting compiler/backend/x64
May 14 19:32:04 Finished compiler/backend/x64                                     1s 137MB
May 14 19:32:05 Starting compiler/backend/arm7
May 14 19:32:07 Finished compiler/backend/arm7                                    1s 138MB
May 14 19:32:08 Starting compiler/backend/arm8
May 14 19:32:10 Finished compiler/backend/arm8                                    1s 138MB
May 14 19:32:11 Starting compiler/backend/mips
May 14 19:32:13 Finished compiler/backend/mips                                    1s 137MB
May 14 19:32:14 Starting compiler/backend/riscv
May 14 19:32:16 Finished compiler/backend/riscv                                   1s 137MB
May 14 19:32:17 Starting compiler/backend/ag32
May 14 19:33:22 Finished compiler/backend/ag32                                 1m03s   3GB
May 14 19:33:23 Starting compiler/backend/pattern_matching
May 14 19:33:24 Finished compiler/backend/pattern_matching                        0s  53MB
May 14 19:33:25 Starting compiler/parsing/ocaml
May 14 19:35:07 Finished compiler/parsing/ocaml                                1m41s   1GB
May 14 19:35:08 Starting compiler/printing
May 14 19:35:10 Finished compiler/printing                                        1s 107MB
May 14 19:35:11 Starting compiler/parsing/proofs
May 14 19:35:12 Finished compiler/parsing/proofs                                  0s  60MB
May 14 19:35:13 Starting compiler/inference/proofs
May 14 19:35:15 Finished compiler/inference/proofs                                1s 115MB
May 14 19:35:16 Starting compiler/backend/semantics
May 14 19:38:20 Finished compiler/backend/semantics                            3m02s   3GB
May 14 19:38:21 Starting compiler/backend/reg_alloc/proofs
May 14 19:38:23 Finished compiler/backend/reg_alloc/proofs                        1s 114MB
May 14 19:38:23 Starting compiler/backend/proofs
May 14 19:39:09 Finished compiler/backend/proofs                                 44s   2GB
May 14 19:39:10 Starting compiler/backend/serialiser
May 14 19:39:12 Finished compiler/backend/serialiser                              1s 142MB
May 14 19:39:13 Starting compiler/encoders/x64/proofs
May 14 19:49:24 Finished compiler/encoders/x64/proofs                         10m09s   4GB
May 14 19:49:24 Starting compiler/encoders/arm7/proofs
May 14 20:02:37 Finished compiler/encoders/arm7/proofs                        13m11s  11GB
May 14 20:02:38 Starting compiler/encoders/arm8/proofs
May 14 20:09:51 Finished compiler/encoders/arm8/proofs                         7m12s   4GB
May 14 20:09:52 Starting compiler/encoders/arm8_asl/proofs
May 14 20:59:10 Finished compiler/encoders/arm8_asl/proofs                    49m16s  20GB
May 14 20:59:10 Starting compiler/encoders/mips/proofs
May 14 21:09:05 Finished compiler/encoders/mips/proofs                         9m53s   5GB
May 14 21:09:06 Starting compiler/encoders/riscv/proofs
May 14 21:17:11 Finished compiler/encoders/riscv/proofs                        8m03s   3GB
May 14 21:17:12 Starting compiler/encoders/ag32/proofs
May 14 21:20:02 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
May 14 21:20:03 Starting compiler/backend/x64/proofs
May 14 21:20:33 Finished compiler/backend/x64/proofs                             28s   2GB
May 14 21:20:33 Starting compiler/backend/arm7/proofs
May 14 21:21:03 Finished compiler/backend/arm7/proofs                            29s   2GB
May 14 21:21:04 Starting compiler/backend/arm8/proofs
May 14 21:21:36 Finished compiler/backend/arm8/proofs                            30s   2GB
May 14 21:21:37 Starting compiler/backend/arm8_asl
May 14 21:21:58 Finished compiler/backend/arm8_asl                               20s   2GB
May 14 21:21:59 Starting compiler/backend/mips/proofs
May 14 21:22:28 Finished compiler/backend/mips/proofs                            28s   2GB
May 14 21:22:29 Starting compiler/backend/riscv/proofs
May 14 21:22:59 Finished compiler/backend/riscv/proofs                           29s   2GB
May 14 21:23:00 Starting compiler/backend/ag32/proofs
May 14 21:36:30 Finished compiler/backend/ag32/proofs                         13m28s   5GB
May 14 21:36:31 Starting compiler/backend/cv_compute
May 14 21:37:38 Finished compiler/backend/cv_compute                           1m06s   1GB
May 14 21:37:39 Starting cv_translator
May 14 21:57:33 Finished cv_translator                                        19m52s   8GB
May 14 21:57:34 Starting candle
May 14 21:57:34 Finished candle                                                   0s  12MB
May 14 21:57:35 Starting candle/set-theory
May 14 21:58:08 Finished candle/set-theory                                       32s   1GB
May 14 21:58:09 Starting candle/syntax-lib
May 14 21:58:11 Finished candle/syntax-lib                                        0s  94MB
May 14 21:58:12 Starting candle/standard
May 14 21:58:13 Finished candle/standard                                          0s  13MB
May 14 21:58:14 Starting candle/standard/syntax
May 14 21:58:26 Finished candle/standard/syntax                                  10s 752MB
May 14 21:58:27 Starting candle/standard/semantics
May 14 22:00:19 Finished candle/standard/semantics                             1m52s   1GB
May 14 22:00:20 Starting candle/standard/monadic
May 14 22:00:22 Finished candle/standard/monadic                                  1s 119MB
May 14 22:00:23 Starting candle/standard/ml_kernel
May 14 22:02:06 Finished candle/standard/ml_kernel                             1m41s   4GB
May 14 22:02:07 Starting candle/standard/ml_kernel/lisp
May 14 22:02:08 Finished candle/standard/ml_kernel/lisp                           0s  46MB
May 14 22:02:09 Starting candle/overloading
May 14 22:02:10 Finished candle/overloading                                       0s  12MB
May 14 22:02:11 Starting candle/overloading/syntax
May 14 22:05:17 Finished candle/overloading/syntax                             3m05s   2GB
May 14 22:05:18 Starting candle/overloading/semantics
May 14 22:16:20 Finished candle/overloading/semantics                         11m00s   5GB
May 14 22:16:21 Starting candle/overloading/monadic
May 14 22:18:35 Finished candle/overloading/monadic                            2m13s   2GB
May 14 22:18:36 Starting candle/overloading/ml_kernel
May 14 22:25:49 Finished candle/overloading/ml_kernel                          7m12s   5GB
May 14 22:25:50 Starting candle/overloading/ml_checker
May 14 22:28:02 Finished candle/overloading/ml_checker                         2m11s   6GB
May 14 22:28:03 Starting candle/prover
May 14 22:37:33 Finished candle/prover                                         9m29s   5GB
May 14 22:37:34 Starting candle/prover/compute
May 14 22:37:36 Finished candle/prover/compute                                    1s 152MB
May 14 22:37:37 Starting pancake
May 14 22:37:39 Finished pancake                                                  1s 139MB
May 14 22:37:40 Starting pancake/semantics
May 14 22:39:51 Finished pancake/semantics                                     2m10s   2GB
May 14 22:39:52 Starting pancake/parser
May 14 22:40:17 Finished pancake/parser                                          23s 480MB
May 14 22:40:18 Starting pancake/static_checker
May 14 22:40:55 Finished pancake/static_checker                                  36s   1GB
May 14 22:40:56 Starting pancake/proofs
May 14 22:57:13 Finished pancake/proofs                                       16m15s   7GB
May 14 22:57:14 Starting compiler/dafny
May 14 23:00:14 Finished compiler/dafny                                        2m58s   9GB
May 14 23:00:14 Starting compiler/dafny/translation
May 14 23:19:37 Finished compiler/dafny/translation                           19m22s  18GB
May 14 23:19:38 Starting compiler/dafny/compilation
May 14 23:22:38 Finished compiler/dafny/compilation                            2m59s  12GB
May 14 23:22:39 Starting compiler/dafny/semantics
May 14 23:23:16 Finished compiler/dafny/semantics                                35s   1GB
May 14 23:23:17 Starting characteristic/examples
May 14 23:24:41 Finished characteristic/examples                               1m23s   4GB
May 14 23:24:42 Starting tutorial/solutions
May 14 23:27:10 Finished tutorial/solutions                                    2m26s   3GB
May 14 23:27:11 Starting translator/monadic/examples
May 14 23:30:04 Finished translator/monadic/examples                           2m52s   4GB
May 14 23:30:05 Starting examples
May 14 23:36:10 Finished examples                                              6m03s   4GB
May 14 23:36:10 Starting examples/compilation
May 14 23:36:11 Finished examples/compilation                                     0s  12MB
May 14 23:36:12 Starting examples/compilation/x64
May 14 23:43:14 Finished examples/compilation/x64                              7m01s   4GB
May 14 23:43:15 Starting examples/compilation/x64/proofs
May 14 23:45:37 Finished examples/compilation/x64/proofs                       2m21s   4GB
May 14 23:45:38 Starting examples/compilation/ag32
May 14 23:47:32 Finished examples/compilation/ag32                             1m52s   3GB
May 14 23:47:33 Starting examples/compilation/ag32/proofs
May 14 23:48:34 Finished examples/compilation/ag32/proofs                      1m00s   5GB
May 14 23:48:35 Starting examples/lpr_checker
May 14 23:49:05 Finished examples/lpr_checker                                    29s   1GB
May 14 23:49:06 Starting examples/lpr_checker/array
May 15 00:15:10 Finished examples/lpr_checker/array                           26m03s  19GB
May 15 00:15:11 Starting examples/lpr_checker/array/compilation
May 15 00:17:31 Finished examples/lpr_checker/array/compilation                2m18s   7GB
May 15 00:17:31 Starting examples/lpr_checker/array/compilation/proofs
May 15 00:18:36 Finished examples/lpr_checker/array/compilation/proofs         1m03s   6GB
May 15 00:18:37 Starting examples/lpr_checker/array/compilation/proofsARM8
May 15 00:19:45 Finished examples/lpr_checker/array/compilation/proofsARM8     1m07s   6GB
May 15 00:19:46 Starting .
May 15 00:19:50 Finished .                                                        2s 320MB
May 15 00:19:51 Starting examples/xlrup_checker
May 15 00:20:26 Finished examples/xlrup_checker                                  34s   1GB
May 15 00:20:27 Starting examples/xlrup_checker/array
May 15 00:33:20 Finished examples/xlrup_checker/array                         12m51s   8GB
May 15 00:33:20 Starting examples/xlrup_checker/array/compilation
May 15 00:34:23 Finished examples/xlrup_checker/array/compilation              1m01s   4GB
May 15 00:34:24 Starting examples/xlrup_checker/array/compilation/proofs
May 15 00:35:21 Finished examples/xlrup_checker/array/compilation/proofs         56s   5GB
May 15 00:35:22 Starting examples/pseudo_bool
May 15 00:36:54 Finished examples/pseudo_bool                                  1m31s   2GB
May 15 00:36:55 Starting examples/pseudo_bool/cnf_encoding
May 15 00:37:24 Finished examples/pseudo_bool/cnf_encoding                       27s   1GB
May 15 00:37:25 Starting examples/pseudo_bool/graph_encoding
May 15 00:38:07 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
May 15 00:38:08 Starting examples/pseudo_bool/array
May 15 01:47:22 Finished examples/pseudo_bool/array                         1h09m13s  35GB
May 15 01:47:23 Starting examples/pseudo_bool/array/compilation
May 15 01:57:30 Finished examples/pseudo_bool/array/compilation               10m06s  18GB
May 15 01:57:31 Starting examples/pseudo_bool/array/compilation/proofs
May 15 02:00:04 Finished examples/pseudo_bool/array/compilation/proofs         2m31s   6GB
May 15 02:00:05 Starting examples/pseudo_bool/array/compilation/proofsARM8
May 15 02:01:19 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m13s   6GB
May 15 02:01:20 Starting examples/opentheory
May 15 02:10:02 Finished examples/opentheory                                   8m40s   5GB
May 15 02:10:03 Starting examples/opentheory/compilation
May 15 02:11:38 Finished examples/opentheory/compilation                       1m34s   6GB
May 15 02:11:39 Starting examples/opentheory/compilation/proofs
May 15 02:12:40 Finished examples/opentheory/compilation/proofs                  59s   4GB
May 15 02:12:41 Starting examples/opentheory/compilation/ag32
May 15 02:14:20 Finished examples/opentheory/compilation/ag32                  1m37s   7GB
May 15 02:14:20 Starting examples/opentheory/compilation/ag32/proofs
May 15 02:15:57 Finished examples/opentheory/compilation/ag32/proofs           1m35s   8GB
May 15 02:15:58 Starting examples/sat_encodings
May 15 02:16:57 Finished examples/sat_encodings                                  58s 893MB
May 15 02:16:58 Starting examples/sat_encodings/demo
May 15 02:16:59 Finished examples/sat_encodings/demo                              0s  10MB
May 15 02:17:00 Starting examples/sat_encodings/case_studies
May 15 02:18:43 Finished examples/sat_encodings/case_studies                   1m42s   1GB
May 15 02:18:44 Starting examples/sat_encodings/translation
May 15 02:22:25 Finished examples/sat_encodings/translation                    3m39s   3GB
May 15 02:22:26 Starting examples/sat_encodings/translation/compilation
May 15 02:24:23 Finished examples/sat_encodings/translation/compilation        1m55s   5GB
May 15 02:24:24 Starting examples/deflate
May 15 02:24:51 Finished examples/deflate                                        26s 755MB
May 15 02:24:52 Starting examples/deflate/translation
May 15 02:25:57 Finished examples/deflate/translation                          1m03s   4GB
May 15 02:25:58 Starting examples/deflate/translation/compilation
May 15 02:26:49 Finished examples/deflate/translation/compilation                49s   3GB
May 15 02:26:50 Starting examples/vipr
May 15 02:30:02 Finished examples/vipr                                         3m11s   4GB
May 15 02:30:03 Starting examples/vipr/compilation
May 15 02:31:01 Finished examples/vipr/compilation                               56s   4GB
May 15 02:31:02 Starting translator/okasaki-examples
May 15 02:35:02 Finished translator/okasaki-examples                           3m59s   3GB
May 15 02:35:03 Starting translator/other-examples
May 15 02:37:23 Finished translator/other-examples                             2m19s   3GB
May 15 02:37:24 Starting translator/other-examples/auxiliary
May 15 02:37:25 Finished translator/other-examples/auxiliary                      0s  13MB
May 15 02:37:26 Starting compiler/parsing/tests
May 15 02:38:00 Finished compiler/parsing/tests                                  32s   1GB
May 15 02:38:01 Starting compiler/inference/tests
May 15 02:38:37 Finished compiler/inference/tests                                34s   2GB
May 15 02:38:38 Starting compiler/printing/test
May 15 02:39:48 Finished compiler/printing/test                                1m09s   5GB
May 15 02:39:49 Starting icing/flover
May 15 03:12:18 Finished icing/flover                                         32m28s   1GB
May 15 03:12:19 Starting icing/flover/Infra
May 15 03:12:20 Finished icing/flover/Infra                                       0s  13MB
May 15 03:12:21 Starting icing/flover/semantics
May 15 03:12:22 Finished icing/flover/semantics                                   0s  14MB
May 15 03:12:23 Starting icing/
May 15 03:38:41 Finished icing/                                               26m17s   4GB
May 15 03:38:42 Starting icing/examples
May 15 03:39:59 Finished icing/examples                                        1m16s   3GB
May 15 03:40:00 Starting compiler/repl
May 15 03:47:46 Finished compiler/repl                                         7m44s   6GB
May 15 03:47:46 Starting unverified/sexpr-bootstrap/x64/64
May 15 03:51:37 Finished unverified/sexpr-bootstrap/x64/64                     3m49s  19GB
May 15 03:51:38 Starting unverified/sexpr-bootstrap/x64/32
May 15 03:54:54 Finished unverified/sexpr-bootstrap/x64/32                     3m15s  16GB
May 15 03:54:55 Starting compiler/benchmarks
May 15 03:55:42 Finished compiler/benchmarks                                     45s 712MB
May 15 03:55:42 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
May 15 03:55:46 Finished compiler/benchmarks/cakeml_benchmarks/cakeml             2s 247MB
May 15 03:55:47 Starting compiler/benchmarks/mlton_benchmarks/cakeml
May 15 03:55:50 Finished compiler/benchmarks/mlton_benchmarks/cakeml              2s 241MB
May 15 03:55:51 Starting compiler/bootstrap/compilation/x64/64
May 15 04:23:56 Finished compiler/bootstrap/compilation/x64/64                28m04s  94GB
May 15 04:23:57 Starting compiler/bootstrap/compilation/x64/64/proofs
May 15 04:48:11 Finished compiler/bootstrap/compilation/x64/64/proofs         24m13s  58GB
May 15 04:48:12 Starting compiler/bootstrap/compilation/x64/32
May 15 05:17:07 Finished compiler/bootstrap/compilation/x64/32                28m54s  89GB
May 15 05:17:08 Starting compiler/bootstrap/compilation/x64/32/proofs
May 15 05:21:23 Finished compiler/bootstrap/compilation/x64/32/proofs          4m14s  24GB
May 15 05:21:24 Starting compiler/bootstrap/compilation/arm8/64
May 15 06:06:13 Finished compiler/bootstrap/compilation/arm8/64               44m47s 110GB
May 15 06:06:14 Starting compiler/bootstrap/compilation/arm8/64/proofs
May 15 06:10:59 Finished compiler/bootstrap/compilation/arm8/64/proofs         4m44s  31GB
May 15 06:11:00 Starting compiler/bootstrap/compilation/ag32/32
May 15 06:39:26 Finished compiler/bootstrap/compilation/ag32/32               28m24s  82GB
May 15 06:39:27 Starting compiler/bootstrap/compilation/ag32/32/proofs
May 15 06:44:19 Finished compiler/bootstrap/compilation/ag32/32/proofs         4m52s  29GB
May 15 06:44:20 SUCCESS