unused argument linter issue

Stream: FLT

[Kevin Buzzard]

What have I done wrong in FLT#732 ? I have made a definition where I've put in some unused arguments to make the definition mathematically accurate. The unused arguments linter complained so I shut it up with set_option linter.unusedVariables false in but the file still isn't linting, which means CI is failing. And yet I see set_option linter.unusedVariables false in in mathlib too

[Kenny Lau]

I've run into this issue before, it's actually two different linters (arguments vs. variable), and I think the fix is to change the names to _

[Damiano Testa]

I'm not sure: using #lint at the bottom also complains and using _ does not seem to silence the linter either.

[Yaël Dillies]

This looks like a lakefile error: You must have turned on the wrong option for the linter. Unfortunately I don't know much more than that since I haven't quite followed the changes to state of the art linting practices, nor do I have time to investigate further

[Kenny Lau]

Yaël Dillies said:

You must have turned on the wrong option for the linter.

I don't know what exactly this means, but I think I've seen it in Mathlib before.

[Kenny Lau]

I've made #30196 to test it, let's see what the result is.

[Kenny Lau]

My test confirms that mathlib also has the same issue: https://github.com/leanprover-community/mathlib4/actions/runs/18246721632/job/51955653447?pr=30196

[Kenny Lau]

image.png

[Michael Rothgang]

Damiano Testa said:

I'm not sure: using #lint at the bottom also complains and using _ does not seem to silence the linter either.

The unusedArgument linter is an environment linter: the way to silence those is to put @[nolint unusedArgument] in front of the declaration.

[Michael Rothgang]

About the difference of the linters: my understanding is that

• the unusedVariable linter checks for named arguments (typeclasses, explicit or implicit hypotheses) whose names are never used. You can indeed suppress that by prepending an underscore to its name. This is a syntax linter, so can be suppressed by the usual set_option linter.unusedVariable false
• the unusedArgument linter checks for hypotheses (to definition and lemmas) which are never used.

[Michael Rothgang]

def foo (_k : Nat) : Nat := 1

[Michael Rothgang]

triggers the unusedArgument linter (as _k) is never used, but not the unused variable linter (as the variable name starts with an underscore)

[Michael Rothgang]

def foo (k : Nat) : Nat := 1

triggers both linters

[Kenny Lau]

I think the subtle difference between a "syntax linter" and an "environmental linter" might be too difficult for the average lean-user who doesn't know any meta-programming: is there a way to unify both types with set_option?

[Kevin Buzzard]

Michael Rothgang said:

Damiano Testa said:

I'm not sure: using #lint at the bottom also complains and using _ does not seem to silence the linter either.

The unusedArgument linter is an environment linter: the way to silence those is to put @[nolint unusedArgument] in front of the declaration.

@[nolint unusedArguments] seems to have fixed it -- thanks!

[Michael Rothgang]

There's a way to tell which kind of linter you have:

• if you see yellow squiggles in your source, it's a syntax linter (and the warning tells you how to disable it)
• if you need to type #lint, you use the nolint incantation

[Michael Rothgang]

Basically, there are two kinds of linters, and you both encounter their warnings differently and suppress them differently.

[Michael Rothgang]

Note that this does not require any understanding of what a syntax or environment linter is or how it works. (I'm just using these terms so I don't have to invent new ones every time.)

[Kevin Buzzard]

What I don't know is how to look up this information easily (which is why I had to ask) (because I will probably forget all this in a few months)

[Bryan Gin-ge Chen]

At the very least, all our linters should probably remind us how to disable them.

[Kevin Buzzard]

Right -- when I had the unused variables problem I could disable it because the warning told me how to. But #lint didn't give me the hint; I guess the experts figure that "the answer is always @[nolint <name-of-linter>] but I don't know the first thing about linters and I don't really care enough about this stuff to learn properly (or maybe I mean "I learn stuff and then forget quickly because I'm 57 and if I don't use stuff constantly then I forget") so I struggle.

[Michael Rothgang]

Bryan Gin-ge Chen said:

At the very least, all our linters should probably remind us how to disable them.

I agree with this one: the environment linters should also say how they can be disabled. Any volunteers for such a PR to batteries?

[Kenny Lau]

it's not you, none of us in this thread knew

[Bryan Gin-ge Chen]

Michael Rothgang said:

Bryan Gin-ge Chen said:

At the very least, all our linters should probably remind us how to disable them.

I agree with this one: the environment linters should also say how they can be disabled. Any volunteers for such a PR to batteries?

If someone can give me pointers, I can do try and do this in a few days.

[Kenny Lau]

Bryan Gin-ge Chen said:

If someone can give me pointers

https://github.com/leanprover-community/batteries/blob/6f7d05f4955eb5af9799d828b697251bb2c9c0b8/Batteries/Tactic/Lint/Frontend.lean#L194

[Bryan Gin-ge Chen]

(I've been sitting on this for too long so I decided to just open an issue referencing this thread: batteries#1468.)