feat: add grind.unusedLemmaThreshold option to report unused E-matching activations by kim-em · Pull Request #12805 · leanprover/lean4

kim-em · 2026-03-05T06:51:16Z

This PR adds a set_option grind.unusedLemmaThreshold that, when set to N > 0
and grind succeeds, reports E-matching lemmas that were activated at least N
times but do not appear in the final proof term. This helps identify @[grind]
annotations that fire frequently without contributing to proofs.

🤖 Prepared with Claude Code

mathlib-lean-pr-testing · 2026-03-05T07:58:55Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cbee80d92c37dbbb9c98fe6f7ee4aeb16bb34ff0 --onto f3752861c934c277630cc0dc5a812bbcc8b6f3a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-05 07:58:55)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-10 03:27:04)

leanprover-bot · 2026-03-05T07:58:57Z

Reference manual CI status:

❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cbee80d92c37dbbb9c98fe6f7ee4aeb16bb34ff0 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-05 07:58:56)
❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-04 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-05 09:33:39)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-10 03:27:05)

…ng activations This PR adds a `set_option grind.unusedLemmaThreshold` that, when set to N > 0 and `grind` succeeds, reports E-matching lemmas that were activated at least N times but do not appear in the final proof term. This helps identify `@[grind]` annotations that fire frequently without contributing to proofs. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

kim-em · 2026-03-05T09:59:26Z

This gives lots of juicy data in Mathlib!

mathlib-lean-pr-testing · 2026-03-05T10:34:18Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12805 has successfully built against this PR. (2026-03-05 10:34:16) View Log

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This PR removes the `@[grind →]` attribute from `List.getElem_of_getElem?` and `Vector.getElem_of_getElem?`. These lemmas were identified as problematic in Mathlib by leanprover#12805. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

mathlib-lean-pr-testing · 2026-03-06T01:29:15Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12805 has successfully built against this PR. (2026-03-06 01:29:13) View Log

mathlib-lean-pr-testing · 2026-03-06T03:15:45Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12805 has successfully built against this PR. (2026-03-06 03:15:44) View Log

This PR removes the `@[grind →]` attribute from `List.getElem_of_getElem?` and `Vector.getElem_of_getElem?`. These lemmas were identified as problematic in Mathlib by leanprover#12805. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

This PR removes the `@[grind →]` attribute from `List.getElem_of_getElem?` and `Vector.getElem_of_getElem?`. These were identified as problematic in Mathlib by #12805. 🤖 Prepared with Claude Code Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

This PR removes the `@[grind →]` attribute from `List.getElem_of_getElem?` and `Vector.getElem_of_getElem?`. These were identified as problematic in Mathlib by #12805. 🤖 Prepared with Claude Code Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com> (cherry picked from commit a165292)

This PR removes the `@[grind →]` attribute from `List.getElem_of_getElem?` and `Vector.getElem_of_getElem?`. These were identified as problematic in Mathlib by #12805. 🤖 Prepared with Claude Code Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

This PR replaces `getUsedConstantsAsSet` with grind's existing instance-marking infrastructure for precise unused lemma detection. Each E-matching instantiation proof is wrapped in `mdata` with a unique ID, and `collectUsedOrigins` walks the proof term to find exactly which theorems were used. A new `config.markInstances` flag enables the cheap mdata wrapping and `InstanceMap` population without triggering the expensive trace pipeline (`ParamMinimizer.search`, `checkTactic` replay). The flag is automatically set when `grind.unusedLemmaThreshold > 0`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

kim-em · 2026-03-07T01:04:57Z

!radar

mathlib-lean-pr-testing · 2026-03-07T02:51:31Z

Mathlib CI status (docs):

✅ Mathlib branch lean-pr-testing-12805 has successfully built against this PR. (2026-03-07 02:51:30) View Log

This PR removes the `@[grind →]` attribute from `List.getElem_of_getElem?` and `Vector.getElem_of_getElem?`. These were identified as problematic in Mathlib by #12805. 🤖 Prepared with Claude Code Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

kim-em · 2026-03-10T01:25:18Z

!radar

leanprover-radar · 2026-03-10T01:25:25Z

Benchmark results for 387a975 against f375286 are in. Significant changes detected! @kim-em

🟥 build//instructions: +3.9G (+0.03%)

Large changes (1✅)

✅ compiled/phashmap//instructions: -99.1M (-1.00%)

Small changes (5🟥)

🟥 build/module/Init.Grind.Config//instructions: +51.6M (+2.78%) (reduced significance based on *//lines)
🟥 build/module/Lean.Elab.Tactic.Grind.Config//instructions: +220.5M (+2.79%) (reduced significance based on absolute threshold)
🟥 build/module/Lean.Elab.Tactic.Grind.Main//instructions: +152.7M (+0.90%) (reduced significance based on *//lines)
🟥 build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: +1.0G (+1.37%) (reduced significance based on *//lines)
🟥 build/module/Lean.Meta.Tactic.Grind.Main//instructions: +1.9G (+15.13%) (reduced significance based on *//lines)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

kim-em added the changelog-tactics User facing tactics label Mar 5, 2026

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 5, 2026

kim-em force-pushed the kim/grind-unused-lemma-threshold branch from 813efd9 to 46f6b43 Compare March 5, 2026 08:40

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 5, 2026

Update lean-toolchain for testing leanprover/lean4#12805

d042563

github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Mar 5, 2026

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 5, 2026

Update lean-toolchain for testing leanprover/lean4#12805

4baec98

kim-em marked this pull request as ready for review March 5, 2026 09:58

kim-em requested a review from leodemoura as a code owner March 5, 2026 09:58

mathlib-lean-pr-testing bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 5, 2026

fix: use fully qualified names in grind.unusedLemmaThreshold output

4e4b609

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

kim-em mentioned this pull request Mar 6, 2026

fix: remove @[grind →] from getElem_of_getElem? #12821

Merged

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 6, 2026

Update lean-toolchain for leanprover/lean4#12805

08bfc9f

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 6, 2026

Update lean-toolchain for leanprover/lean4#12805

06f51c7

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2026

Update lean-toolchain for leanprover/lean4#12805

da174c9

mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 7, 2026

Update lean-toolchain for leanprover/lean4#12805

6203387

kim-em added this pull request to the merge queue Mar 10, 2026

github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 10, 2026

chore: merge master (test directory rename)

329c35b

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

kim-em enabled auto-merge March 10, 2026 02:44

kim-em added this pull request to the merge queue Mar 10, 2026

Merged via the queue into master with commit ada5363 Mar 10, 2026
15 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add grind.unusedLemmaThreshold option to report unused E-matching activations#12805

feat: add grind.unusedLemmaThreshold option to report unused E-matching activations#12805
kim-em merged 4 commits intomasterfrom
kim/grind-unused-lemma-threshold

kim-em commented Mar 5, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 5, 2026 •

edited

Loading

Uh oh!

leanprover-bot commented Mar 5, 2026 •

edited

Loading

Uh oh!

kim-em commented Mar 5, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 5, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 6, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 6, 2026

Uh oh!

kim-em commented Mar 7, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 7, 2026

Uh oh!

kim-em commented Mar 10, 2026

Uh oh!

leanprover-radar commented Mar 10, 2026 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

kim-em commented Mar 5, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Mar 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kim-em commented Mar 5, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 5, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 6, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 6, 2026

Uh oh!

kim-em commented Mar 7, 2026

Uh oh!

mathlib-lean-pr-testing bot commented Mar 7, 2026

Uh oh!

kim-em commented Mar 10, 2026

Uh oh!

leanprover-radar commented Mar 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

mathlib-lean-pr-testing bot commented Mar 5, 2026 •

edited

Loading

leanprover-bot commented Mar 5, 2026 •

edited

Loading

leanprover-radar commented Mar 10, 2026 •

edited

Loading