)]}'
{
  "commit": "2c8a3c89d38080afab202909adcb3951600071de",
  "tree": "21fe48d4f0e8d7e00ba431d675d8d065f1ee6f75",
  "parents": [
    "583131b37da27fce7370223433c0ecf3b6aa7ada"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 15:30:33 2026 +0000"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leomoura@amazon.com",
    "time": "Wed Oct 28 15:30:33 2026 +0000"
  },
  "message": "feat: report reached thresholds in `grind` failure message\n\nThis PR makes the `grind` failure message reported without `+verbose` list the thresholds that were reached, as configuration items the user can raise. For example, `lia` now fails with `` `lia` has failed after reaching the threshold `(splits :\u003d 9)`, use `+verbose` to obtain diagnostic information ``. This applies to `instances`, `ematch`, `splits`, `gen`, `ringSteps`, and `liaSteps`, and to all tactics built on `grind`, such as `lia`, `grind_order`, `grind_linarith`, and `grobner`.\n\nThe threshold checks move from the `+verbose` diagnostics into `getThresholdsReached`, which both the diagnostics and the short failure message use. The `+verbose` output is unchanged.\n\nCo-Authored-By: Claude Opus 5.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "e76fb72b27639aa15e5bc865fa82ee9dd4778101",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean",
      "new_id": "77fa715b2d162ae32e4785ce6e753e330fe24ab5",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean"
    },
    {
      "type": "modify",
      "old_id": "7ebec34ed1e39693527c0c9bcce220c0c681ead5",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/Main.lean",
      "new_id": "273181bf6d397298dba80c1efc31539b5b17503f",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/Main.lean"
    },
    {
      "type": "modify",
      "old_id": "6987c93f86988bb295fc0b7504ed6f62f982ec52",
      "old_mode": 33188,
      "old_path": "src/Lean/Meta/Tactic/Grind/PP.lean",
      "new_id": "8fa34800f77dfa5e384d4af4e5d482a8feef0f32",
      "new_mode": 33188,
      "new_path": "src/Lean/Meta/Tactic/Grind/PP.lean"
    },
    {
      "type": "modify",
      "old_id": "b3241e1a98ec1d5f2e8ecd01e862df7fa2b414e1",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_11081.lean",
      "new_id": "be9d18d789a2d1c0db541ec456db89e263dd21b3",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_11081.lean"
    },
    {
      "type": "modify",
      "old_id": "c83619e17a0eabe39477338d2ff9480e1f9209df",
      "old_mode": 33188,
      "old_path": "tests/elab/grind_11124.lean",
      "new_id": "41d78e12b8a8357cf644ff7fd6518ec40835f565",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_11124.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "c3083e6a16e68ba226f383d4dd3245e1ba107168",
      "new_mode": 33188,
      "new_path": "tests/elab/grind_threshold_msg.lean"
    }
  ]
}