intrusive linters

Stream: mathlib4

[Kim Morrison]

I think many people will try out something simple by creating a new file in Mathlib, with import Mathlib at the top, and then write something:

import Mathlib

def thirtySeven := 37

However this now results in lots of spurious linter warnings that really don't help:

* '-/':
Copyright too short!

note: this linter can be disabled with `set_option linter.style.header false`

The module doc-string for a file should be the first command after the imports.
Please, add a module doc-string before ``.
note: this linter can be disabled with `set_option linter.style.header false`

Can we work out how to have these linters fire for a "real" file, but silent if someone is just trying something out?

[Kim Morrison]

I'm not sure what the heuristic should be... Don't check if the file is less than some length? Don't check unless the file is managed by git (if this is feasible it might be exactly right!)

[Damiano Testa]

lake exe mk_all has a --git flag that only adds the git-managed files, so I am pretty sure that git-managed is possible.

[Damiano Testa]

(I actually wanted the default of lake exe mk_all to be using that flag, but this did not go well with review...)

[Eric Wieser]

Invoking git every time a linter is run sounds a little annoying

[Damiano Testa]

Well, since Mathlib.lean is supposed to be in sync with git-managed, you can read Mathlib.lean.

[Damiano Testa]

So the condition could be "appears in Mathlib.lean".

[Damiano Testa]

Incidentally, that avoids having to deal with git-related issues on weird setups (like, apparently, mine).

[Eric Wieser]

Another reasonable heuristic would be "doesn't use import Mathlib"

[Damiano Testa]

Well, there is another linter that prevents that from entering mathlib... :smile:

[Damiano Testa]

We seem to have linted ourselves in a corner...

[Eric Wieser]

Damiano Testa said:

Well, there is another linter that prevents that from entering mathlib... :smile:

Why? Surely the mk_all check prevents that.

[Damiano Testa]

Ah, import Mathlib.Tactic is disallowed, Mathlib may not be, you are right.

[Damiano Testa]

Anyway, I probably prefer searching inside Mathlib.lean, since you may not want to import Mathlib for a test file anyway.

[Damiano Testa]

The equivalence "git-managed iff imported in Mathlib.lean" is only valid for Mathlib itself, not for a project working with mathlib.

This means that using "appears in Mathlib.lean" is a good solution for mathlib, but for downstream projects it is still git-managed that should be used.

Should this be something to worry about? Is the copyright check/has a doc-module linter just a mathlib linter?

[Damiano Testa]

Anyway, this is a possible implementation for the check:

import Lean.Elab.Command

open Lean Elab Command in
def isInMathlib : CommandElabM Bool := do
  let mlPath := ("Mathlib" : System.FilePath).addExtension "lean"
  if ← System.FilePath.pathExists mlPath then
    let ml ← IO.FS.lines mlPath
    let curr := (← getMainModule).toString
    return (ml.map (·.endsWith curr)).any (·)
  else return false

[Damiano Testa]

#18033

[Damiano Testa]

Feel free to take over the PR and modify it at will! :smile:

[Eric Wieser]

Using docs#Lean.parseImports' feels more robust

[Kim Morrison]

Another alternative is just to disable this linter if Mathlib is imported in the current file.

[Eric Wieser]

Indeed

[Damiano Testa]

I think that not everyone has import Mathlib in all their test files, but I am happy to go with that option if you prefer. I personally almost never have working oleans for all of mathlib, so I virtually never use import Mathlib.

[Damiano Testa]

Anyway, I'm going to sleep now: feel free to claim ownership of the PR!

(Also, with the current implementation, this adds an import to Mathlib.Init, which may be a consideration to keep in mind.)

[Damiano Testa]

I fixed the issue with the linter.

The linter is active if you tell it to be, regardless of whether the file is in Mathilb.lean or not. Otherwise, the linter is only active in files imported in Mathlib.lean.

[Damiano Testa]

As far as heuristics go, this seems a good one to me, but I do not have a strong attachment to it.

[Michael Rothgang]

So, to summarize the discussion: this is about the header linter firing when this is merely annoying.

• this is not about projects depending on mathlib (all style linters are disabled there anyway, and only disabled in mathlib)
• this is not about tests in mathlib (those also disable all linters, right),
• but only about "scratch files inside mathlib": which you use locally to try out something, which are not meant for mathlib.
• the current proposal is to disable the linter whenever a file has an import Mathlib in it.

Is this an accurate summary? Is there anything missing?

[Damiano Testa]

The current PR disables the linter when the file is not imported in Mathlib.lean, though the proposal that seems to have more support is to exclude files that have import Mathlib.

[Michael Rothgang]

Thanks, updated my summary.

[Michael Rothgang]

Assuming the above is correct, I wonder about a more general solution:

• this issue should apply to any "style" linter (such as writing $ instead of <| or $\lambda$ for fun), right?
• would it make sense to introduce an option linter.style.all, which (if set) enables or disables all style linters? Then a scratch file could disable all style linters with one line of additional boilerplate. (Is there a way to have an option not set? I'd like to distinguish "set to True" from "set to False" and "not set explicitly.)

[Edward van de Meent]

arguably, if you want to make a scratch file, don't do it in mathlib. but rather use the playground...

[Michael Rothgang]

I hear a fair number of senior Lean people do have scratch files, though - arguing "you're doing it all wrong" is a difficult stance in general.

[Edward van de Meent]

i'm not saying you're doing it wrong, i'm saying there is a solution which doesn't involve changing linter settings and whatnot

[Kevin Buzzard]

I prefer working in VS Code locally rather than using the playground, especially when I'm at home on my fast machine.

[Kevin Buzzard]

I was independently annoyed when these linters started complaining about my scratch files but chose not to raise the issue and have been instead training myself to ignore all the warnings.

[Kevin Buzzard]

Thinking a bit more about it: definitely VS Code is offering lots of advantages over the playground, for example I can jump to definition and it opens a new tab etc.

[Edward van de Meent]

i don't have a fast machine, so in my experience importing Mathlib on my pc was already slower than the playground... oh well

[Damiano Testa]

I think that having the option of local scratch files that are "linter-free" is almost a necessity.

[Damiano Testa]

As far as I know, docs#Lean.Options do have the 3 settings mentioned: unset, set to true and set to false. I think that having a #scratch_file command that disables the style linters is a good idea as well!

[Damiano Testa]

(That is, whether or not we go with some heuristic for disabling the style linters, also having an explicit command to disable them is probably useful.)

[Michael Rothgang]

Would set_option linter.style.false be reasonable as such a command?

[Michael Rothgang]

That said: I see no downside to implementing that first, and a scratch_file command later. I won't have time for that this week, but feel free to ping me next week :-)

[Kevin Buzzard]

Just to remark that I almost came a cropper with this yesterday. I was rehearsing my Stanford maths department colloquium and I fired up VS Code to just do some random three minute demo. I started with #eval 2+2 (4) and then #check \R (error) and then I explained that Lean knows the rules of maths but hardly any maths itself, and so we fix it by importing the maths library, then I typedimport Mathlib and it was chaos. I was so pleased I'd rehearsed! In the actual talk I did everything within the FLT repo where there were no problems.

[Kim Morrison]

Where are we up to with this? It's still the case that a new file in Mathlib with import Mathlib comes with all sorts of unhelpful warnings.

[Damiano Testa]

Let me try it: I thought that for files that do not appear among the files imported by Mathlib.lean, many (if not all) the warnings would have been silenced.

[Damiano Testa]

Kim, is there any particular linter that you are seeing? I do not see the header linter, not the set_option one saying anything with import Mathlib.

[Kim Morrison]

Screenshot 2024-11-20 at 9.53.24 AM.png

[Damiano Testa]

Are you on an up to date master? :smile:

[Kim Morrison]

Yes

[Kim Morrison]

Note the file is not tracked by git, and is just in amongst random mathlib files.

[Kim Morrison]

(i.e. I saved it wherever the last file I had open happened to be)

[Damiano Testa]

Yes, I noticed and the header linter should be ignoring it...

[Damiano Testa]

Let me try to see what I get locally.

[Damiano Testa]

(opening a file with import Mathlib takes several minutes on my computer, I am not sure why, since lake exe cache get and lake build both turned out successful.)

[Damiano Testa]

Ok, I see the warnings on my computer as well.

[Damiano Testa]

#19267