Disabling the VSCode linter for unused variables

Stream: lean4

[CK]

Hello - How can one disable the unused variable linter in VS Code.

note: this linter can be disabled with "set_option linter.unusedVariables false"

[Henrik Böving]

You are supposed to paste the set_option linter.unusedVariables false into the file that you wish to disable it in.

[CK]

Thanks, this works! Maybe we might need to specify somewhere in the infoview that one needs to add that line to the file itself rather than setting it on VSCode preferences etc..

[Henrik Böving]

Note that linters do not have anything to do with vscode at all, they are parts of Lean, the program, VSCode merely shows them to you.

[Jon Eugster]

Another option is to prefix the corresponding variable with a _ in the code, e.g. _myVar.

I think this is the preferred way to indicate that you are intentionally not using that specific variable (but sometimes it's not possible to do that, e.g. for names of function arguments).

[Patrick Massot]

I think the separation between Lean and its various editor integration is something that is very confusing to beginners, and very hard to keep in mind for existing users who write documentation. For us it is completely obvious that linters have nothing to do with the VSCode or vim or emacs support, and we would never think of saying it. But for beginners the whole Lean experience is one giant blob and it is not obvious at all. The issue also arise with the separation between Core Lean, batteries and Mathlib.

[Patrick Massot]

And maybe the standard teaching resources do not discuss any set_option early. If you have never seen set_option anywhere then it is not clear at all where they should go.

[Patrick Massot]

@CK what are you reading to learn Lean? We could check whether we can add an explanation of set_option there.

[Patrick Massot]

Going back to the actual question, I strongly advise you to very rarely disable this linter. It is very useful for mathematics and completely crucial for programming.

[Patrick Massot]

@Jeremy Avigad I just checked and we never explain set_option in #mil. So users who learn Lean using our book will not know where to put it if they see it in an error message or on zulip (see this thread for an example).

[CK]

@Patrick Massot Thank you for understanding. I am a beginner to Lean programming and loving the journey so far. I started using it at SRI SSFT '24 where we had lecture and lab sessions with David Christiansen and Leo De Moura. In so far as the material, I am primarily using the following two books:

1. https://leanprover.github.io/theorem_proving_in_lean/
2. Theorem Proving in Lean - Jeremy Avigad, Leo De Moura, and Soonho Kong
   However, I was looking into the book (second link) and there is a chapter on setting options. Which is what I should have referred before asking here.

[Kevin Buzzard]

Those are the same book, right?

[CK]

They are different versions of the same book. The link points to the latest version of the book (2023 edit) and the PDF is an older version (2016). Define-Predicate-Lean.pdf

[Patrick Massot]

What is the point of reading the old version?

[CK]

That was the version shared during the seminar.