Skip to content

fix: make option linter.unusedSimpArgs respect linter.all#12560

Queued
fiforeach wants to merge 1 commit intoleanprover:masterfrom
fiforeach:issue12559
Queued

fix: make option linter.unusedSimpArgs respect linter.all#12560
fiforeach wants to merge 1 commit intoleanprover:masterfrom
fiforeach:issue12559

Conversation

@fiforeach
Copy link
Contributor

@fiforeach fiforeach commented Feb 18, 2026

This PR changes the way the linting for linter.unusedSimpArgs gets the value from the environment. This is achieved by using the appropriate helper functions defined in Lean.Linter.Basic.

The following now compiles without warning

set_option linter.all false in
example : True := by simp [False]

Fixes #12559

@fiforeach fiforeach requested a review from kim-em as a code owner February 18, 2026 16:03
@fiforeach fiforeach marked this pull request as draft February 18, 2026 16:03
@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 Feb 18, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 18, 2026
Update lean-toolchain for testing leanprover/lean4#12560
552b7a6
@github-actions 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 Feb 18, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 18, 2026
Update lean-toolchain for testing leanprover/lean4#12560
22e6bfb
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Feb 18, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#12560
7beb715
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 18, 2026 •
edited
Loading

Reference manual CI status:

  • 🟡 Reference manual branch lean-pr-testing-12560 build against this PR didn't complete normally. (2026-02-18 17:20:25) View Log
  • ✅ Reference manual branch lean-pr-testing-12560 has successfully built against this PR. (2026-02-18 17:20:33) View Log
  • ✅ Reference manual branch lean-pr-testing-12560 has successfully built against this PR. (2026-02-19 12:24:33) View Log
  • 🟡 Reference manual branch lean-pr-testing-12560 build against this PR didn't complete normally. (2026-02-19 12:27:11) View Log
  • ✅ Reference manual branch lean-pr-testing-12560 has successfully built against this PR. (2026-02-19 17:55:16) View Log
  • 🟡 Reference manual branch lean-pr-testing-12560 build against this PR didn't complete normally. (2026-02-19 17:57:16) View Log
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-03 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-03 10:02:41)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fe3ba4dc4c5b794578df3ea66d399e0203ba73fe --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-09 14:12:10)

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Feb 18, 2026
grunweg
grunweg reviewed Feb 18, 2026
View reviewed changes
Copy link
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for your PR! I am not affiliated to this repository, but I took a look anyway. This is what I would suggest. I can imagine some of these comments would be shared by reviewers from this repository.

@grunweg grunweg mentioned this pull request Feb 18, 2026
Merged
@grunweg
Copy link
Contributor

grunweg commented Feb 18, 2026

I found a few more linters with the same issue and fixed them in a separate PR.

grunweg
grunweg reviewed Feb 19, 2026
View reviewed changes
Copy link
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Two more suggestions from the peanut gallery.

grunweg
grunweg reviewed Feb 19, 2026
View reviewed changes
grunweg
grunweg reviewed Feb 19, 2026
View reviewed changes
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 19, 2026
Update lean-toolchain for leanprover/lean4#12560
f0d80bd
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 19, 2026
Update lean-toolchain for leanprover/lean4#12560
2aa7b02
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Feb 19, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#12560
3f6748a
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 19, 2026
Update lean-toolchain for leanprover/lean4#12560
5db67c2
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 19, 2026
Update lean-toolchain for leanprover/lean4#12560
d3e0bba
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Feb 19, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#12560
29bc3ce
@fiforeach fiforeach marked this pull request as ready for review February 20, 2026 07:18
@nomeata nomeata added the changelog-language Language features and metaprograms label Mar 3, 2026
@nomeata nomeata enabled auto-merge March 3, 2026 08:05
@nomeata nomeata closed this Mar 3, 2026
auto-merge was automatically disabled March 3, 2026 08:22

Pull request was closed

@nomeata nomeata reopened this Mar 3, 2026
@nomeata nomeata enabled auto-merge March 3, 2026 08:22
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 3, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-03 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 10:02:39)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fe3ba4dc4c5b794578df3ea66d399e0203ba73fe --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-09 14:12:08)

auto-merge was automatically disabled March 3, 2026 12:49

Head branch was pushed to by a user without write access

@fiforeach
Copy link
Contributor Author

fiforeach commented Mar 3, 2026

@nomeata #12590 introduced (migrated?) some tests that explicitly checked for the linter being on. I now removed those warnings.

Do you know if those tests (in tests/elab) are run with the linter disabled? The readme does not comment on this.

github-merge-queue bot pushed a commit that referenced this pull request Mar 9, 2026
@grunweg @fiforeach
fix: make the omit, unusedSectionVars and loopingSimpArgs linter resp…
fe3ba4d 
…ect linter.all (#12563)

This PR makes the `omit`, `unusedSectionVars` and `loopingSimpArgs`
linters respect the `linter.all` option:
when `linter.all` is set to false (and the respective linter option is
unset), the linter should not report errors.

Similarly to #12559, these linters should honour the linter.all flag
being set to false. These are all remaining occurrences of this pattern.

This fixes an issue analogous to #12559.
This PR and #12560 fix all occurrences of this pattern. (The only
question is around `RCases.linter.unusedRCasesPattern`: should this also
respect this? I have left this alone for now.)

Co-authored-by: fiforeach <249703130+fiforeach@users.noreply.github.com>
@fiforeach
fix: make option linter.unusedSimpArgs respect linter.all
80d5a91 
This PR changes the way the linting for `linter.unusedSimpArgs` gets the value
from the environment. This is achieved by using the appropriate helper functions
defined in `Lean.Linter.Basic`.

The following now compiles without warning

```lean4
set_option linter.all false in
example : True := by simp [False]
```

Fixes leanprover#12559
@fiforeach
Copy link
Contributor Author

fiforeach commented Mar 9, 2026

@nomeata I rebased onto master and squashed the commits.

@nomeata
Copy link
Collaborator

nomeata commented Mar 9, 2026

Thanks! Squashing isn't necessary, we squash on merge and take PR description for the commit

@nomeata nomeata added this pull request to the merge queue Mar 9, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@nomeata nomeata nomeata approved these changes

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

+1 more reviewer

@grunweg grunweg grunweg left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

Option linter.unusedSimpArgs does not respect linter.all

4 participants

@fiforeach @leanprover-bot @grunweg @nomeata