8000 feat: set_option tactic.simp.warnUnused by nomeata · Pull Request #8895 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: set_option tactic.simp.warnUnused #8895

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
wants to merge 21 commits into from
Closed

feat: set_option tactic.simp.warnUnused #8895

wants to merge 21 commits into from

Conversation

nomeata
Copy link
Collaborator
@nomeata nomeata commented Jun 20, 2025

This PR adds the tactic.simp.warnUnused tactic that will warn about
unused simp arguments (off by default).

This is off by default because it may report false positives when the simp invocation is run multiple times, e.g. inside all_goals or inside a macro. Fixing this would be good, but requires some more design and possible infrastructure.

This closes #4483.

Depends on #8815.

nomeata added 19 commits June 16, 2025 14:59
@nomeata
refactor: elab simp arguments to declarative result, apply later
9dab528
@nomeata
stash
363c2f0
@nomeata
starArg handling
403b314
@nomeata
Rename
23b1a6f
@nomeata
Subltety around erasing simp entries
4235402
@nomeata
Merge branch 'nightly-with-mathlib' of https://github.com/leanprover/…
a55ddae 
…lean4 into joachim/simp-arg-elab
@nomeata
Kick CI
4cf7999
@nomeata
Default argument
fdc4e00
@nomeata
docstring
d959e63
@nomeata
Add function back for compat with mathlib
4a2bb97
@nomeata
Clean up SimpTheorems.lean a bit (group API by type, mild renaming)
6c5d06b
@nomeata
Recover .erase/eraseCore behavior
54871f6
@nomeata
elabSimpArg withRef
e7cce2c
@nomeata
More refactoring
780d3f1
@nomeata
MkSimpContextResult.addStar
76c0309
@nomeata
Simplify addStar further
7f47d19
@nomeata
Merge commit '3b2990b381' into joachim/simp-arg-elab
bcc8d86
@nomeata
Keep simp args around
1bae07d
@nomeata
feat: set_option tactic.simp.warnUnused
fcef7b1 
This PR adds the `tactic.simp.warnUnused` tactic that will warn about
unused simp arguments (off by default).

This closes #4483.
@nomeata nomeata added the changelog-language Language features, tactics, and metaprograms label Jun 20, 2025
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 20, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8895
931485d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8895
b6d4576
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jun 20, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Jun 20, 2025 •
edited
Loading

Mathlib CI status (docs):

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8895
b0d85a1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 20, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8895
9e4714a
@nomeata
Copy link
Collaborator Author
nomeata commented Jun 20, 2025

closing in favor of the more ambitious #8901, but we may come back to this.

@nomeata nomeata closed this Jun 20, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@digama0 digama0 Awaiting requested review from digama0 digama0 will be requested when the pull request is marked ready for review digama0 is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

RFC: Make simp only warn on unused list elements
2 participants
@nomeata @leanprover-community-bot
0