)]}'
{
  "commit": "d81d2b8cc75b9dfed18f7db01d78fb4451562130",
  "tree": "e1efd9e56ce3adafb3fe6d38353a1514b32d4ba4",
  "parents": [
    "b21ac7949a8f8f5953ed789c9fcea07998ecedf2"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Nov 01 04:37:07 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Sun Nov 01 04:37:07 2026 +0000"
  },
  "message": "feat: bound grind case splits by the size of the search tree\n\nThis PR replaces the `grind` option `splits` with `branches`, which limits the total number of branches that case splitting may create during a proof search (default 1024). Previously, `grind`, `lia`, and the related tactics allowed at most 9 case splits along each branch of the search, so a goal with a long chain of cheap case splits failed even when its proof was tiny. For example, a hypothesis `x ≤ 0 ∨ 100 ≤ x ∨ x \u003d 2 ∨ x \u003d 4 ∨ … ∨ x \u003d 36` whose disjuncts are each refuted immediately needed 17 case splits in a row and exceeded the limit. Such goals are now proved with the default configuration, while the total amount of case splitting stays bounded.\n\nA case split with `n` cases creates `n - 1` new branches, and case splits that turn out to be irrelevant to the proof are not counted. In `grind \u003d\u003e …` mode, each `finish` starts with a fresh budget. When the limit is reached, the error message says so, e.g., \"`lia` has failed after reaching the threshold `(branches :\u003d 1024)`\", and `grind (branches :\u003d n)` raises it.\n\nMigration:\n* `splits` is deprecated and reports a warning, which can be disabled with `set_option linter.deprecated false`.\n* `splits :\u003d 0` still disables case splitting, and is equivalent to `branches :\u003d 0`.\n* Other values of `splits` are ignored. If a proof needs more case splitting than the default allows, use `branches :\u003d n`.\n* `grobner (splits :\u003d n)` no longer enables case splitting. Use `grobner (branches :\u003d n)`.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "04b4898f0030612c4d846957eec52c210d0a77cd",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Config.lean",
      "new_id": "613084813fb3141eec1a7d0f427a68ce735e6416",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Config.lean"
    },
    {
      "type": "modify",
      "old_id": "2425a75e4608bdfa3121dfd6e3ae444c5a1888a4",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Lint.lean",
      "new_id": "a276423c9e7ec20bbc9764ee480566613e8b4d44",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Lint.lean"
    },
    {
      "type": "modify",
      "old_id": "02ced42651e2d5be5a7f64d643ea4315776c3f94",
      "old_mode": 33188,
      "old_path": "src/Init/Grind/Tactics.lean",
      "new_id": "5a52e0a87cdfbc24db3ec3e3fe1c5354d61d5030",
      "new_mode": 33188,
      "new_path": "src/Init/Grind/Tactics.lean"
    },
    {
      "type": "modify",
      "old_id": "62a3ca395b8190331f451e825a48091acd12d95c",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Config.lean",
      "new_id": "ce987f7b44681fd65c2491e4ac3d5bbbe91d0cf0",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Config.lean"
    },
    {
      "type": "modify",
      "old_id": "baaffbdb8c06bacbc85d4d76dccce77946002704",
      "old_mode": 33188,
      "old_path": "src/Lean/Elab/Tactic/Grind/Lint.lean",
      "new_id": "adc1334c5a948dd02830ffa600fde913cab48d03",
      "new_mode": 33188,
      "new_path": "src/Lean/Elab/Tactic/Grind/Lint.lean"
    },
    {
      "type": "modify",
      "old_id": "e597141f7f818e7ae46ddfebc9cbc29113185603",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Finish.lean",
      "new_id": "e89ecb9c18abf0cc6900723c1d4fa247d729eaa6",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Finish.lean"
    },
    {
      "type": "modify",
      "old_id": "9c73daa5faf7a9fe47496be7dc03e2223c852592",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/MBTC.lean",
      "new_id": "57d0a67844987680c635693ffcf2439c31c8f322",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/MBTC.lean"
    },
    {
      "type": "modify",
      "old_id": "273181bf6d397298dba80c1efc31539b5b17503f",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Main.lean",
      "new_id": "9e58b5df8252ac3800ca9c5c9b90b30a5e16e3a7",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Main.lean"
    },
    {
      "type": "modify",
      "old_id": "8fa34800f77dfa5e384d4af4e5d482a8feef0f32",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/PP.lean",
      "new_id": "971fc0be76ac5ae5b9c2be495f8e70f32812195f",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/PP.lean"
    },
    {
      "type": "modify",
      "old_id": "082cb0cdcd9009cb998a333518e9d2478fe671ca",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Split.lean",
      "new_id": "ee7a0c646a7328af43e152b34ba750ff116958ed",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Split.lean"
    },
    {
      "type": "modify",
      "old_id": "a4291fcfd213478720d8e7e24c4c3916332e2a3f",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Types.lean",
      "new_id": "0ae2011088823f2c23b129b01c5f8804f97b6bea",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Types.lean"
    },
    {
      "type": "modify",
      "old_id": "955decc54f9f4ed7554929ea3464d9c6b92a69fd",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_11539.lean",
      "new_id": "9361823d0669cbb649948a914d6dc9c897da233a",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_11539.lean"
    },
    {
      "type": "modify",
      "old_id": "c5846da95390958b6724cb8f6cea9d4eca640419",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_ac_1.lean",
      "new_id": "bcf3e39e14f8ab2f1b13d9c5dc047e7fcca90cac",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_ac_1.lean"
    },
    {
      "type": "modify",
      "old_id": "5cb4578bcf500e947a972b98bb3ec64b42b0c37d",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_beta_generation_check.lean",
      "new_id": "c896ce0b622cc3a589faf2880d724260d40c000f",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_beta_generation_check.lean"
    },
    {
      "type": "modify",
      "old_id": "d722a0027b388d962b0cabbfd8b0a734c1a199fd",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_bool_diseq.lean",
      "new_id": "429488129c6372ac25462f2e8b27a0d07c8f72bd",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_bool_diseq.lean"
    },
    {
      "type": "modify",
      "old_id": "1561b6a55c19c9e98dd922ceb5b1f07452997888",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_bool_prop.lean",
      "new_id": "1e3c039e016193fe5ef86927ec2f7256010b5014",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_bool_prop.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "168e5813d485a0efae2b7645953f06a642340daa",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_branches.lean"
    },
    {
      "type": "modify",
      "old_id": "e78dfb7a5284cd8063474d54c85e9c3fbda54262",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_canon_bug_2.lean",
      "new_id": "cb67b67a529323edfabaaef89e921f9c26af5127",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_canon_bug_2.lean"
    },
    {
      "type": "modify",
      "old_id": "9c02ddeb413f09c8cc3d177fb608879d53c0adb8",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_cutsat_nat_eq.lean",
      "new_id": "1c5a5013f75781f3156f6aa569dfdad560910fcb",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_cutsat_nat_eq.lean"
    },
    {
      "type": "modify",
      "old_id": "4b6e7559a7bdf6fe64b225b00e2c395d0c9098b6",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_dep_match_overlap.lean",
      "new_id": "531b0029ae4aa0d210adbe536112b6dc2d94b343",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_dep_match_overlap.lean"
    },
    {
      "type": "modify",
      "old_id": "fb3a9d3416e684cd7ef29e57a413f772c658d302",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_diseq.lean",
      "new_id": "2d7fec1cd20051c01b46cfcae516b89bb7815f80",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_diseq.lean"
    },
    {
      "type": "modify",
      "old_id": "dd1fd344ff3fa2ea2a2ecc64343d760b4ca7f6b6",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_getLast_dropLast.lean",
      "new_id": "c26b7a9ee3e6ff1f9ce08385e71bbf7a6186dc66",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_getLast_dropLast.lean"
    },
    {
      "type": "modify",
      "old_id": "fdb39c9fd00497b4be29d3e7e0d4ad84333fc264",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_guide.lean",
      "new_id": "a66c63c0299acafb22b9f3ef22bcfca6ad1117b3",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_guide.lean"
    },
    {
      "type": "modify",
      "old_id": "7199e619059a7fb8a2342d24777d9c46ee8b494f",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_guide_2.lean",
      "new_id": "e50146949251531ea433643a38bec1cd94f6289b",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_guide_2.lean"
    },
    {
      "type": "modify",
      "old_id": "253cb576e44e0bedcbdad347cf136082422cbcee",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_hom_list.lean",
      "new_id": "fe470225db17e7f28638aac121e95cf7a4ee4683",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_hom_list.lean"
    },
    {
      "type": "modify",
      "old_id": "7f150c7072e13871ac3ccf20413dc8d462341432",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_lazy_ite.lean",
      "new_id": "40d64c502c9fcdc0ddae69b9a4ce6da8c85c127a",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lazy_ite.lean"
    },
    {
      "type": "modify",
      "old_id": "d9fb794bc3a2ee45a91be35e4d181e3a8cbe6710",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_list_erase.lean",
      "new_id": "74e35f948d51099ae3a2a9221b822f5674f08df2",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_list_erase.lean"
    },
    {
      "type": "modify",
      "old_id": "b3f200c27daf18103fd6e60ac2b81c868ae47f54",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_lookahead.lean",
      "new_id": "35076ecc887d4f6abcd015f97df46deadc962f3a",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_lookahead.lean"
    },
    {
      "type": "modify",
      "old_id": "c0e1e297144f4cce47b7f32b881798aeb36d4119",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_match_eq_propagation.lean",
      "new_id": "0947cdeb105a6467dd3ab1b9ed3ae290d78b7921",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_match_eq_propagation.lean"
    },
    {
      "type": "modify",
      "old_id": "7746180035648129a66b6c6f06994972523d477b",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_nochrono.lean",
      "new_id": "a2795b4d6d87d40d9a48adbdbf4d7ff6e53216bc",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_nochrono.lean"
    },
    {
      "type": "modify",
      "old_id": "898a7f5119bd1763680223d2ee7471513ebee260",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_norm_sym_match.lean",
      "new_id": "62e81be44ec15c08aefaba407a6df8e76d80d867",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_norm_sym_match.lean"
    },
    {
      "type": "modify",
      "old_id": "258d7791d0241c09b91e8fa31bc1ccbda8bfa1ae",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_omega_tests.lean",
      "new_id": "3ec2bdab29d115140b7983239ce8df16799c8334",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_omega_tests.lean"
    },
    {
      "type": "modify",
      "old_id": "8360cddeb45152e5582fc711d0887ed063c8b2bc",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_order_1.lean",
      "new_id": "a71f2c8326a52fbdc5d66ea12a7b81b20490c15f",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_order_1.lean"
    },
    {
      "type": "modify",
      "old_id": "4374fffe8c436823ac6066518cd079ab6198ea7c",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_order_2.lean",
      "new_id": "26bdd7dc6cbc301fea4be2e8a6aa4dc38b8dd78c",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_order_2.lean"
    },
    {
      "type": "modify",
      "old_id": "6f66759bb80be104392a18c8ec58b73c0a9c5ed8",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_order_3.lean",
      "new_id": "abec6c50a7158468392ae0972aedfe1323b2e07c",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_order_3.lean"
    },
    {
      "type": "modify",
      "old_id": "3788923aa992a364efffb3d093fe0134bb09c864",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_order_eq.lean",
      "new_id": "59c9d9134b4c1506c2eb775ddc1bd1d83eac415d",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_order_eq.lean"
    },
    {
      "type": "modify",
      "old_id": "f4602f5cc40ffdfbda439c822b6ba2cebbc6116d",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_order_propagation.lean",
      "new_id": "33741e895bc7d6b03fa0c8272235b225709bd7a3",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_order_propagation.lean"
    },
    {
      "type": "modify",
      "old_id": "e5b47b771d161a894fe75fcbb1fe69105c1e3b69",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_power_reentrant.lean",
      "new_id": "8f58359445f77227338b75e9a3344dda61f57a46",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_power_reentrant.lean"
    },
    {
      "type": "modify",
      "old_id": "99beaa1fc058aa658206b3cac637ad90bd08ea9f",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_ring_2.lean",
      "new_id": "76526e702c55c9c9f4aeebffcb7d72a6e1a97f03",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_ring_2.lean"
    },
    {
      "type": "modify",
      "old_id": "74fb9eeaa994a465c2c9d7da5e13f15ec568150c",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_split_arith_imp.lean",
      "new_id": "d8f12c6ad85b47475a27d64da6b7d42fcab72f75",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_split_arith_imp.lean"
    },
    {
      "type": "modify",
      "old_id": "dfb4b5e0418c5cf746f563b46ed1a3e0ee9819a2",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_t1.lean",
      "new_id": "37e9b4494f3ed8c9fad6816522166a8469fcae19",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_t1.lean"
    },
    {
      "type": "modify",
      "old_id": "c3083e6a16e68ba226f383d4dd3245e1ba107168",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_threshold_msg.lean",
      "new_id": "304897081f9b173218ea06128260c8af7cedbc8a",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_threshold_msg.lean"
    },
    {
      "type": "modify",
      "old_id": "ad52ef648d4f6cfe536bcd5d21ca3011209fa4df",
      "old_mode": 33188,
      "old_path": "tests/elab/lia_or_hull.lean",
      "new_id": "9683a1f228be7bcb01cdc68f78d95507e0918c22",
      "new_mode": 33188,
      "new_path": "tests/elab/lia_or_hull.lean"
    },
    {
      "type": "modify",
      "old_id": "c00081d8341083f0d3e62f4520f27060add7be57",
      "old_mode": 33188,
      "old_path": "tests/elab_bench/grind_bitvec2.lean",
      "new_id": "25104df656f4c40ec6d9ca84e1279eba681ad58e",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/grind_bitvec2.lean"
    },
    {
      "type": "modify",
      "old_id": "477fa1f1b62f9f9b2f422ec8fa8a486bb839924a",
      "old_mode": 33188,
      "old_path": "tests/elab_bench/grind_list2.lean",
      "new_id": "9fe55d3b09315047b8bf1db22a09ea4e401fdb1e",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/grind_list2.lean"
    },
    {
      "type": "modify",
      "old_id": "e77134a085f13d7768cb49d1ff60c78c913c1568",
      "old_mode": 33188,
      "old_path": "tests/elab_bench/lia_case_splits.lean",
      "new_id": "d2c6b159b5ab24588646c8a5f2a808b6cee9e963",
      "new_mode": 33188,
      "new_path": "tests/elab_bench/lia_case_splits.lean"
    },
    {
      "type": "modify",
      "old_id": "f167720fa043217d5b5dabe911df1e03aa7ba06f",
      "old_mode": 33188,
      "old_path": "tests/lean/grind/experiments/bitvec.lean",
      "new_id": "0b4cd9e5b4a3d03cd0b67048f41bd95c0a9a4af7",
      "new_mode": 33188,
      "new_path": "tests/lean/grind/experiments/bitvec.lean"
    },
    {
      "type": "modify",
      "old_id": "79024ee0a774f5c7ddac3aae09f00790531c065e",
      "old_mode": 33188,
      "old_path": "tests/lia_perf/lia_oss_verify_4.lean",
      "new_id": "7768fc929f8dafea53d9e575198075f33ada3a11",
      "new_mode": 33188,
      "new_path": "tests/lia_perf/lia_oss_verify_4.lean"
    },
    {
      "type": "modify",
      "old_id": "84ef5547459e613d25aadd7003ecfb60ea1c9632",
      "old_mode": 33188,
      "old_path": "tests/lia_perf/lia_oss_verify_failing.lean",
      "new_id": "76dca6dc597ff231e04077dc34707b29b8c57321",
      "new_mode": 33188,
      "new_path": "tests/lia_perf/lia_oss_verify_failing.lean"
    }
  ]
}