Unused variables linter

Stream: lean4

[Uranus Testing]

Is there a way to disable this recently added linter in the whole Lake package at once (i.e. without adding set_option linter.unusedVariables false everywhere)?

[Sebastian Ullrich]

Yes, you should be able to set moreLeanArgs := #["-Dlinter.unusedVariables=false"] in your lakefile. And/or moreServerArgs to disable it in the editor.

[Uranus Testing]

Yes, it works. Thanks!

[Sebastian Ullrich]

Apart from that, we are open to suggestions for improving the lint of course :)

[Mario Carneiro]

One thing that might help (not sure if this is what Uranus Testing was dealing with) which I discovered when deploying an unused variables linter of my own is that declarations that use sorry should be exempted from the linter

[Sebastian Ullrich]

I was thinking of excluding those with errors, which I suppose is almost but not quite the same

[Mario Carneiro]

I think that theorems with errors could also be exempted but they are much less likely to be a pervasive "how do I turn off this linter globally" problem compared to use of sorry

[Mario Carneiro]

because usually you won't have hundreds of theorems with errors

[Sebastian Ullrich]

Wow, that's quite a number of sorrys. But it shouldn't hurt excluding them.

[Mario Carneiro]

you must not be watching the #condensed mathematics stream. :) There are regular reports there on the number of sorrys left and it's in that ballpark; the compiler file I'm working on right now has 203 sorrys in 1400 lines

[Sebastian Ullrich]

Nice. At some point, flycheck-mode would give up just from the number of sorry warnings.

[Mario Carneiro]

well, technically it's an axiom called sorry because that many yellow squiggles would drive me nuts

[Sebastian Ullrich]

Understandable, but that complicates making it disable the other linter

[Mario Carneiro]

that's true. I did a file-level disable for my project

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/1205

[Kevin Buzzard]

I think that right now we have around 60 sorries in condensed maths

[Sebastian Reichelt]

Just updated Lean and got lots of "unused variable" warnings, but I don't quite understand. E.g. I get a warning if I name a type class parameter without using the name within the definition. But if I remove the name, that also changes the interface for users of the definition, in case I want to provide an explicit argument. Should parameters be excluded, maybe?

[Xubai Wang]

Why not use _ or _a as parameter name? Does the underscore prefix matter for you interface?

[Sebastian Ullrich]

@Sebastian Reichelt Yes, this specific case was left unresolved in the initial implementation. My favorite solution would still be https://github.com/leanprover/lean4/pull/1190#discussion_r889594858 though.

[Sebastian Ullrich]

(Do you often need to explicitly specify inst-implicit arguments? That seems like an anti pattern)

[Mario Carneiro]

Here's another false positive:

example (P : α → Prop) : (∃ a, P a ∧ a = x) → P x
| ⟨_, sb, rfl⟩ => sb

[Mario Carneiro]

There also appears to be a separate error where putting the cursor over the commas in the lambda-match yields an infoview error:

example (s : α → Prop) : (∃ a, s a ∧ a = x) → s x :=
  λ ⟨_, sb, rfl⟩ => sb
   -- ^

Error updating: Error fetching goals: {"stack":"Error: unknown constant 'Set._example.match_1'\n\tat /home/mario/.vscode/extensions/leanprover.lean4-0.0.78/dist/extension.js:2:542515\n\tat /home/mario/.vscode/extensions/leanprover.lean4-0.0.78/dist/extension.js:2:542809\n\tat Immediate.<anonymous> (/home/mario/.vscode/extensions/leanprover.lean4-0.0.78/dist/extension.js:2:543171)\n\tat processImmediate (node:internal/timers:464:21)","message":"unknown constant 'Set._example.match_1'","code":-32603}. Try again.

[Sebastian Ullrich]

Let me guess, the last one doesn't happen with def?

[Sebastian Ullrich]

The first example looks like https://github.com/leanprover/lean4/issues/1214

[Mario Carneiro]

It has some vague resemblance to lean4#1214 but it seems different since in this case the variable doesn't even have a user-given name, and it's also not referred to by name in the body. But possibly a solution to that one would also solve this?

[Mario Carneiro]

and yes your guess is right about the second one, it seems like it's looking for a definition that example only temporarily added to the environment

[Mario Carneiro]

Here's another example, also possibly from the same issue:

example : Nat → Bool
| 0 => false
| _+1 => true
--^ unused variable `n._@.Mathlib.Test._hyg.24`

[Sebastian Ullrich]

Is that with https://github.com/leanprover/lean4/pull/1221?

[Mario Carneiro]

I'm on june 17 nightly, so no

[Mario Carneiro]

both of these are fixed on june 19 nightly (not the infoview issue though)

[Sebastian Reichelt]

Sebastian Ullrich said:

(Do you often need to explicitly specify inst-implicit arguments? That seems like an anti pattern)

Sorry, missed this. It happens rarely (sometimes because I want to, sometimes because I can't figure out why type class synthesis fails). But when writing a library, the names are part of the API; that's why I was a little concerned in general (not so much directly related to my code).

I did run into another issue, though: For some reason, the notation let _ : α ← x fails with expected ':=' at the colon. Is that a bug?