Improper firing of linter.hashcommand

Stream: mathlib4

[Asei Inoue]

import Mathlib.Data.Real.Sqrt

/-
`#`-commands, such as '#guard', are not allowed in 'Mathlib'
note: this linter can be disabled with `set_option linter.hashCommand false`
-/
#guard "hello, " ++ "world" = "hello, world"

[Damiano Testa]

This seems all correct: what is the issue?

[Asei Inoue]

The linter.hashcommand may be necessary for Mathlib development, but it is unlikely to be needed for all files importing Mathlib.

[Asei Inoue]

I found it annoying that this linter fired when just importing Mathlib.

[Asei Inoue]

Can't we separate the 'developer's linter for a specific library' from the 'linter for users'?

[Asei Inoue]

I know that it is possible to disable this linter in the options settings. That is not the question I want to ask.

[Damiano Testa]

You should import mathlib and be in a file whose path starts with Mathlib.

[Damiano Testa]

Otherwise the linter should be quiet.

[Asei Inoue]

You should import mathlib and be in a file whose path starts with Mathlib.
Otherwise the linter should be quiet.

Is it not possible to read the lakefile configuration and branch by the name of the package?

[Damiano Testa]

Ah, no, this one may only be quiet in tests.

[Eric Wieser]

@Damiano Testa, is it expected that this fires in the web editor?

[Damiano Testa]

It is designed to be active on any file whose path does not start with test, except for the test file of the linter itself.

[Damiano Testa]

I thought that it had been silenced on files that were not in mathlib, but I must be confusing it with some of the other linters.

[Damiano Testa]

In any case, I think that there are always competing desires: projects downstream of mathlib may want to pick and choose which linters they want active and different projects will have different choices. So, neither making the linters always active not always inactive is a good decision.

[Damiano Testa]

The new option-setting is just for the command-line lake build, right?

[Damiano Testa]

So, that is also not really going to solve this issue, I think.

[Damiano Testa]

Maybe there should be a "linter options" file that contains the default value of each linter and each linter reads off from there its default setting.

[Damiano Testa]

So, rather than embedding the defValue of each linter in the option for the linter, that is something that can be configured independently.

[Asei Inoue]

Why not leave it disabled by default and enable it in the Mathlib lakefile?

[Damiano Testa]

I do not think that you can enable or disable linters from the lakefile.

[Damiano Testa]

Otherwise, this would have been the case for all linters, I think.

[Eric Wieser]

Damiano Testa said:

I do not think that you can enable or disable linters from the lakefile.

I think this is new in 4.11?

[Damiano Testa]

It could be: I never used it yet, but it was not clear to me that this was not something that could only be set as an option to lake build.

[Asei Inoue]

Add linter.missingDocs to here works for me....

package «package name» where
  leanOptions := #[
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩,
    ⟨`linter.missingDocs, true⟩
  ]

[Damiano Testa]

Ah, but those are the "built-in" linters. Those you can always set in the lakefile.

[Damiano Testa]

Ok, if it works, then this solves all problems!

[Eric Wieser]

lean4#3403 was the tracking issue for this not working until very recently

[Asei Inoue]

It would be a solution if any linter could be configured in the lakefile as well as the built-in linter.

[Asei Inoue]

so now this issue can be solved?

[Damiano Testa]

Ok, so now everyone is free to set their linter options in the lakefile?

[Damiano Testa]

Time to clean up all the "look for the path and cripple the linter"!

[Asei Inoue]

So nice! :smiley: :tada: This new feature is awesome...! It is a time to a little celebrate dance ₍₍ (ง ˘ω˘ )ว ⁾⁾

[Damiano Testa]

It might even be a policy that every linter's default is false and each project is expected to opt in in the lakefile.

[Asei Inoue]

Some linters would like it to be enabled by default. ex: unusedVariable

[Eric Wieser]

The danger with using the new weak arguments if that if you typo a linter name then it doesn't run at all

[Eric Wieser]

(or more realistically, if mathlib decides to rename the linter)

[Damiano Testa]

Maybe a deprecation system could be enforced

[Asei Inoue]

A possible solution is to specify the location where the linter is defined in lakefile and to make an error if the file is reached but there is no linter...

[Michael Rothgang]

Damiano Testa said:

Time to clean up all the "look for the path and cripple the linter"!

Feel free to push #15521 to completion :-)

[Sebastian Ullrich]

Eric Wieser said:

(or more realistically, if mathlib decides to rename the linter)

You phrased that like it could be an issue for downstream users but why would they need weak in that case? If they want to use a linter, shouldn't they make sure to import it everywhere in their project?

[Michael Rothgang]

To clarify: in mathlib, you would need to put weak.linter.longLine. Projects downstream of it can/should be able to simply use linter.longLine.

[Sebastian Ullrich]

(future improvements that could allow linters to be used without being imported notwithstanding)

[Eric Wieser]

Ah, I think I misunderstood how name resolution worked for options, indeed if this only affects mathlib itself then there is much less to worry about

[Mario Carneiro]

Damiano Testa said:

It might even be a policy that every linter's default is false and each project is expected to opt in in the lakefile.

No, I think it is usually pretty clear when a linter should be default on or default on only in mathlib. Linters which are useful generally and try to improve code quality should be enabled by default, and linters which try to maintain mathlib quality standards or enforce "house rules" of mathlib should be disabled by default and enabled in the mathlib lakefile.

Here's my triage of which is which:

Global:

• globalAttributeIn
• haveLetLinter
• dupNamespace
• unusedTacticLinter

Mathlib local:

• hashCommandLinter
• missingEndLinter
• cdotLinter
• longLineLinter
• oldObtainLinter (unless this is supposed to be a deprecation warning?)
• refineLinter (although maybe it can be made global if we get refine?)
• setOptionLinter

[Damiano Testa]

Ok, sounds great!

[Ruben Van de Velde]

Yeah, I think old obtain should warn on dependencies so we can remove it

[Damiano Testa]

#15616