RFC: discoverability of linter options

[hargoniX]

Proposal

Once a linter emits a warning the message of that warning should contain the name of the option that disables the linter. Currently this option can basically only be found "by accident" through the auto completion of set_option.

Rust does something similar to this:

fn test(x : u32) -> u32 {
    0
}

yields:

warning: unused variable: `x`
 --> src/lib.rs:1:9
  |
1 | fn test(x : u32) -> u32 {
  |         ^ help: if this is intentional, prefix it with an underscore: `_x`
  |
  = note: `#[warn(unused_variables)]` on by default

(the corresponding incantation to disable it would be #[allow(unused_variables)])

I propose that the equivalent code in Lean:

def test (x : UInt32) : UInt32 := 0

which currently yields:

unused variable `x` [linter.unusedVariables]

should yield something along the lines of

unused variable `x`
note: this lint can be disabled with `set_option linter.unusedVariables false`

I'm not familiar with the linter framework right now but ideally this should be generically possible across all linters.

• User Experience: Users will easily discover the options to disable linters as opposed to discovering the feature by accident or in the future by reading that specific part of the docs.

• Beneficiaries: All Lean users that aren't aware of these options but want to fiddle with linter settings.

• Maintainability: I don't think this is much of a change in terms of maintainability. The only thing to keep in mind is if we end up changing the option names we must reflect that in the messages.

Community Feedback

I know of at least one user that would like this feature to exist and it does seem reasonable to me.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[digama0]

Once a linter emits a warning the message of that warning should contain the name of the option that disables the linter.

It does though? It's written right there in the message. But I agree that using a set_option line specifically would be more copy-pasteable.

This is very easy to implement, you just have to change this line to use a different message and it will affect all linters.

[hargoniX]

That's great! I wasn't sure (didn't look at the code yet) if this is actually guaranteed to be the name of the option or just a coincidence, will send a PR!

[digama0]

It is, that's why it's printed in the message 😄