Disabling all linters

Stream: new members

[fiforeach]

I would like to disable all linters. I have found that set_option linter.all false does not work as I expected.

Consider the following example

-- Warnings for `linter.unusedVariables` and `linter.unusedSimpArgs`
example (n : Nat) : 1 = 1 := by simp [Or.inl]

-- Warning for `linter.unusedSimpArgs`
set_option linter.all false in
example (n : Nat) : 1 = 1 := by simp [Or.inl]

-- No warnings
set_option linter.all false in
set_option linter.unusedSimpArgs false in
example (n : Nat) : 1 = 1 := by simp [Or.inl]

This is confusing because linter.unusedSimpArgs is not set:

#eval return Lean.Elab.Tactic.linter.unusedSimpArgs.get? (← Lean.getOptions)
-- none

So basically I would like to know

1. Why is set_option linter.all false not sufficient in the example above? In particular, why is it that linter.unusedSimpArgs is not defaulting to the value of linter.all?
2. Is there a way to disable all linter warnings without listing all options explicitly?

[Michael Rothgang]

I think you have found a bug in the unusedSimpArgs linter --- as in, I would also expect it to honour that option. In general, setting linter.all to false should disable all linters. I believe @Joachim Breitner worked on the unusedSimpArgs linter: can you comment if this is indeed a bug, or I am overlooking something?

[Michael Rothgang]

My other question for you is, of course: why do you want to disable all linters? Often, linters tell me things I can improve in my code. Disabling them temporarily is useful, but in the end I still want to run them.

[fiforeach]

Thanks for the clarification.

Michael Rothgang said:

My other question for you is, of course: why do you want to disable all linters?

During development. I agree that the linter provides helpful information and the long-term goal is to address all the issues.

[Joachim Breitner]

Michael Rothgang schrieb:

I think you have found a bug in the unusedSimpArgs linter --- as in, I would also expect it to honour that option. In general, setting linter.all to false should disable all linters. I believe Joachim Breitner worked on the unusedSimpArgs linter: can you comment if this is indeed a bug, or I am overlooking something?

Yes, that looks like a bug. Issue (and maybe a PR if simple) welcome.

[fiforeach]

Joachim Breitner said:

Yes, that looks like a bug. Issue (and maybe a PR if simple) welcome.

Ok, thanks. Looks like the linter linter.unusedSimpArgs did not fetch the options correctly.

I filed issue #12559 and created PR #12560.

[Joachim Breitner]

Thanks!

[Michael Rothgang]

lean4#12563 fixes the remaining such linters. (Help adding tests would be very very welcome!)

[Michael Rothgang]

I wonder: should RCases.linter.unusedRCasesPattern also respect the linter? (And, by the way: is there a reason for the option name? I would have expected linter.unusedRCasesPattern or perhaps linter.rcases.unusedPattern instead of the current name.)

[Michael Rothgang]

My PR fails to build, though - and I neither understand the bootstrapping dance in Lean core, nor have I managed to set up a development environment. Can I summon an expert to help me fix the PR? (For instance, @Jovan Gerbscheid, can we trade? I'll review a non-difficult PR or yours and you fix up my branch to compile?)

[Jovan Gerbscheid]

What I do in my copy of the lean4 repo is to change the content of the lean-toolchain file to whatever toolchain I want to use (e.g. copy the content of the lean-toolchain file in mathlib). lets you make small changes, like your PR, without having to build lean locally.

For your PR in particular, I'm guessing you're either missing an import, or haven't opened some required namespace.

[Joachim Breitner]

May I suggest to keep PRs as draft until they are ready for review? This is more smooth than having to check CI status