fix: make the omit, unusedSectionVars and loopingSimpArgs linter respect linter.all

[grunweg]

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.)

[fiforeach]

The suggested changes should make the code compile.

However, I would also suggest you add some test cases.

[nomeata]

Please undraft once ready for review

[grunweg]

(CI fails because of a missing changelog label: I cannot add this myself, I believe.)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7fa7ec188763de14a73c266fdc8f3d1b8c79873e --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-20 17:12:08)
• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-03-07 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-09 11:18:00)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7fa7ec188763de14a73c266fdc8f3d1b8c79873e --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-20 17:12:10)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-07 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-09 11:18:02)

[nomeata]

I see Linux Lake failing

[fiforeach]

I see Linux Lake failing

The test tests/lean/run/variable.lean assumes that linter.unusedSectionVars is on. Since this PR changes that linter to respect linter.all and the tests in tests/lean/run are run with -Dlinter.all=false¹ you have to enable that linter manually.

Adding the line

set_option linter.unusedSectionVars true

to the top (say after the first line) of tests/lean/run/variable.lean makes that test pass.

Footnotes

1. https://github.com/leanprover/lean4/blob/master/doc/dev/testing.md#test-suite-organization ↩

[fiforeach]

@grunweg Are you planning on pursuing this further? Since I want to have this feature, I would be happy to continue with this PR.

[grunweg]

I'd like to get this landed, but I won't have time for it this week. You're very welcome to adopt this PR; I'll be happy to look over your changes if you'd like me to. Thanks for the offer!

[nomeata]

I took the liberty to draft this PR. Please undraft when you two are happy with it

[fiforeach]

Ok, I made some changes and made a PR: grunweg#1 (Which seems not very helpful since I merged master...)

Is there a better way to share my changes?

In any case, @nomeata please have a look what I have written there regarding linter.loopingSimpArgs.

[grunweg]

@fiforeach I have squashed all commits into one. Let me know if there is a better way to attribute your co-authorship!

[grunweg]

I am happy with this PR now (assuming it passes). @fiforeach What about you?

[fiforeach]

@grunweg All good from my side. Thanks for asking!

[grunweg]

We are both happy with this PR!

[nomeata]

Were the performance changes when compiling lean expected? Are we running now more linters that way: https://radar.lean-lang.org/repos/lean4/commits/fe3ba4dc4c5b794578df3ea66d399e0203ba73fe

[grunweg]

I didn't expect these, but they don't terribly surprise me either: checking if the linter is enabled now has to do slightly more work, so it's fairly plausible there is an impact. I am a bit surprised by the size of the effect, though.

[nomeata]

Maybe some caching will be needed here at some point

[fiforeach]

The issue is that some files enable all linters

lean4/src/Std/Data/DTreeMap/Internal/Model.lean

Line 21 in 40e8f4c

set_option linter.all true

Previously, the linters linter.omit and linter.loopingSimpArgs were not enabled by this, i.e., they have defValue := false.

The "fix" would be never to use set_option linter.all true in the internal libraries and assume the defaults are enough.

[nomeata]

Ok, whoever enables all linters deserves a slow down :-)