Linter options; variable shadowing

Stream: new members

[Mako Bates]

Hi all, I'm a new user.

What's the normal way to set up linter warnings in my IDE (in my case, neovim)?
I'm coming from Haskell, where I've gotten comfortable with ghc-options: -Wall; is there any equivelent?

I see that I'm getting some linting for free with the lean.nvim plugin, specifically unused variable. But I'm not getting warned about variable shadowing, which feels amazingly dangerous in the context of or-patterns.
Specifically, I'd expect something in my toolchain to complain about a situation like this:

def foo : Nat := 999
def bar : Nat ⊕ Nat -> Nat
  | .inl foo | .inr _foo => foo
#eval bar (.inl 10)  -- 10
#eval bar (.inr 10)  -- 999

Am I the only one who think's it's crazy to let a variable use-site be simultaneously shadowed and not shadowed?

[Aaron Liu]

Mako Bates said:

which feels amazingly dangerous in the context of or-patterns.

Lean has an infoview, you can see in the infoview exactly which variables you have in scope, and there's also hover info attached to most of the syntax (including identifiers like foo) that tells you what it is. And if something does go wrong and you go to prove theorems about your functions you won't be able to prove the theorems. So I think it's not as bad as Haskell.

[Mako Bates]

Thanks for the response!
I'm unconvinced that the info/hover views and theorem-proving habits make these kinds of mistakes moot. Putting together a working example was a fun introductory exercise though!

abbrev isEven (n : Nat) : Prop := ∃ n', n = (n' * 2)

-- example: two is even
def n : Nat := 2
theorem two : isEven n := by exists 1

inductive Even : Type where
  | double : Nat -> Even
  | addTwo : Even -> Even

def Even.toNat : Even → Nat
  | .double n | .addTwo _e => n * 2
  -- Should say `| .addTwo e => (toNat e) + 2`

theorem even (e : Even) : isEven (e.toNat) := match e with
  | .double n | .addTwo e' => by exists n

Here the function Even.toNat contains a mistake, exactly like the earlier bar.
But our theorem e has exactly the same superposition-shadowing, so it works without ever indicating there might be a problem.

(Of course first I put together the not-broken version, which was longer and more illuminating.)

[Julian Berman]

I'll not opine on how easy it is to make a mistake in these kinds of cases -- but just on behalf of lean.nvim, it adds very little here, instead we benefit from all the hard work of lean itself plus linters written by wonderful people like @Damiano Testa and many many others; what you see is basically just output from those. It might be one could write one for these kinds of variable shadowing cases as well in which case it'd just immediately work in Neovim as well.

[Mako Bates]

Ah; yes that is the more important question! How does one see/configure the linter lean.nvim is using? I have seen that there are other linters I could apply to a project, but if I'm going to set one up I'd like nvim to show it.

[Julian Berman]

lean.nvim is invoking Lean's build tool lake, so the warnings you see should match what you see from lake build, and configuring additional options is done in your lakefile, or by importing a linter in a file of your project. There are of course a bunch of examples of writing such a linter in Mathlib, e.g. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Linter/EmptyLine.lean is a random one