feat: report reached thresholds in `grind` failure message This 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 := 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`. The threshold checks move from the `+verbose` diagnostics into `getThresholdsReached`, which both the diagnostics and the short failure message use. The `+verbose` output is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.