Duplication in style linters

Stream: mathlib4

[Damiano Testa]

Currently, the 100-character limit is enforced by two linters;

• a syntax linter, highlighting exceptions live,
• a text-based linter that runs in CI.

I have an open PR for a syntax linter for long files that already has a text-based one and I am also thinking about a syntax "header linter", for checking the presence of doc-module string.

[Damiano Testa]

The reason for not removing the text-based linter once the syntax one is available is that the syntax linter is only active on files that import the linter, while the text-based ones crawl all .lean files that they can find.

There are just under 600 files that do not import the linters, of which ~170 are Tactic-ish.

[Damiano Testa]

Should style syntax linters be imported at the very beginning, so that they can really replace their text-based analogues, or is the duplication not a big deal?

[Ruben Van de Velde]

I think it's generally an issue that linters don't work on all code. That's really unexpected behaviour

[Johan Commelin]

Would it help if we start a new Lean package MathlibLinters in the same git repo as Mathlib and move all the linters there? So that all of mathlib can import those linters?

[Johan Commelin]

(And then maybe MathlibLinters can't lint itself...)

[Yaël Dillies]

Johan Commelin said:

(And then maybe MathlibLinters can't lint itself...)

But that's okay, right?

[Damiano Testa]

I can understand that a linter cannot lint anything that it imports (or itself), but even with the package, I still think that you need to have a "root" Mathlib file that is imported by all of Mathlib and that imports the linters.

[Damiano Testa]

I should add: I like the idea of a Linter-package!

[Johan Commelin]

Having such a root file is probably a good idea. That way we can guarantee that a bunch of stuff from core/std/batteries is available everywhere. This need has come up before.

[Damiano Testa]

Ok, so should I simply create an import-only file with

import Lean
import Batteries

and import this file in all Mathlib files that import no Mathlib file?

[Damiano Testa]

Somehow, I still think that there will be some special casing among Mathlib files...

[Michael Rothgang]

Thanks for starting this thread! I think having a root file importing all style linters would be great to have! (Can we then write an env_linter ensuring this file is transitively imported everywhere? :zany_face:)

[Jon Eugster]

I thought @Kim Morrison or somebody had a good reason against plain import Batteries and spent some time removing all such occurences in mathlib, or do I misremember?

[Yaël Dillies]

Correct me if I'm wrong, but I believe it was at a time where many things where being upstreamed from mathlib and having Batteries imported everywhere was getting in the way of knowing what to do next. If my understanding is accurate, this was a temporary situation and we can revert back to import mathlib everywhere

[Ruben Van de Velde]

I don't think we want to import all of batteries in (nearly) all mathlib files, but it would make more sense in the top level Mathlib.lean

[Johan Commelin]

I think we can have some root file that is imported in all of mathlib. The precise contents of that root file can change over time. I would start conservatively, and only have a bunch of linters/tactics in there.

[Damiano Testa]

There are 143 files in Mathlib that import no Mathlib file. Everything else imports one of these.

Should I create a Mathlib/Init.lean file that is imported in all these 143 files?

[Damiano Testa]

Together with automation to make sure that Mathlib.Init is always imported by contains the files that import no Mathlib file?

[Damiano Testa]

Btw, these are the current "roots" of Mathlib:

Mathlib.Algebra.HierarchyDesign     Mathlib.Tactic.CasesM           Mathlib.Tactic.Recall
Mathlib.CategoryTheory.Category.Init    Mathlib.Tactic.Change           Mathlib.Tactic.Recover
Mathlib.CategoryTheory.ConcreteCategory Mathlib.Tactic.Check            Mathlib.Tactic.ReduceModChar.Ext
Mathlib.Combinatorics.SimpleGraph.Init  Mathlib.Tactic.Clean            Mathlib.Tactic.Relation.Rfl
Mathlib.Control.Combinators     Mathlib.Tactic.Clear_           Mathlib.Tactic.Relation.Symm
Mathlib.Control.ULift           Mathlib.Tactic.ClearExcept      Mathlib.Tactic.Rename
Mathlib.Data.Array.Defs         Mathlib.Tactic.ClearExclamation     Mathlib.Tactic.Says
Mathlib.Data.Array.ExtractLemmas    Mathlib.Tactic.Coe          Mathlib.Tactic.Set
Mathlib.Data.ByteArray          Mathlib.Tactic.Constructor      Mathlib.Tactic.SetLike
Mathlib.Data.Finset.Attr        Mathlib.Tactic.Continuity.Init      Mathlib.Tactic.SimpIntro
Mathlib.Data.Int.Align          Mathlib.Tactic.Conv         Mathlib.Tactic.SimpRw
Mathlib.Data.Int.Notation       Mathlib.Tactic.Eqns         Mathlib.Tactic.Simps.NotationClass
Mathlib.Data.Matroid.Init       Mathlib.Tactic.Eval         Mathlib.Tactic.Spread
Mathlib.Data.MLList.Dedup       Mathlib.Tactic.ExistsI          Mathlib.Tactic.Substs
Mathlib.Data.MLList.IO          Mathlib.Tactic.Explode.Datatypes    Mathlib.Tactic.SuccessIfFailWithMsg
Mathlib.Data.Nat.Notation       Mathlib.Tactic.ExtendDoc        Mathlib.Tactic.SudoSetOption
Mathlib.Data.Ordering.Basic     Mathlib.Tactic.ExtractGoal      Mathlib.Tactic.SuppressCompilation
Mathlib.Data.String.Defs        Mathlib.Tactic.FailIfNoProgress     Mathlib.Tactic.Trace
Mathlib.Data.Sym.Sym2.Init      Mathlib.Tactic.Find         Mathlib.Tactic.TryThis
Mathlib.Deprecated.Aliases      Mathlib.Tactic.FunProp.Decl     Mathlib.Tactic.TypeCheck
Mathlib.Deprecated.HashMap      Mathlib.Tactic.FunProp.StateList    Mathlib.Tactic.TypeStar
Mathlib.Init.Data.List.Instances    Mathlib.Tactic.FunProp.ToBatteries  Mathlib.Tactic.UnsetOption
Mathlib.Init.Data.Quot          Mathlib.Tactic.GCongr.ForwardAttr   Mathlib.Tactic.Use
Mathlib.Init.Data.Sigma.Basic       Mathlib.Tactic.Generalize       Mathlib.Tactic.Variable
Mathlib.Init.Data.Sigma.Lex     Mathlib.Tactic.GuardGoalNums        Mathlib.Tactic.Widget.SelectInsertParam
Mathlib.Init.Quot           Mathlib.Tactic.GuardHypNums     Mathlib.Topology.Sheaves.Init
Mathlib.Init.Set            Mathlib.Tactic.Have         Mathlib.Util.AddRelatedDecl
Mathlib.Lean.Elab.Term          Mathlib.Tactic.HaveI            Mathlib.Util.AssertExists
Mathlib.Lean.EnvExtension       Mathlib.Tactic.HelpCmd          Mathlib.Util.AssertNoSorry
Mathlib.Lean.Exception          Mathlib.Tactic.InferParam       Mathlib.Util.AtomM
Mathlib.Lean.Expr.Basic         Mathlib.Tactic.Lemma            Mathlib.Util.CompileInductive
Mathlib.Lean.GoalsLocation      Mathlib.Tactic.Linarith.Oracle.SimplexA Mathlib.Util.CountHeartbeats
Mathlib.Lean.Json           Mathlib.Tactic.Linter.DocModule     Mathlib.Util.Delaborators
Mathlib.Lean.LocalContext       Mathlib.Tactic.Linter.GlobalAttributeIn Mathlib.Util.DischargerAsTactic
Mathlib.Lean.Message            Mathlib.Tactic.Linter.HashCommandLinter Mathlib.Util.Export
Mathlib.Lean.Meta           Mathlib.Tactic.Linter.HaveLetLinter Mathlib.Util.GetAllModules
Mathlib.Lean.Meta.Basic         Mathlib.Tactic.Linter.Lint      Mathlib.Util.IncludeStr
Mathlib.Lean.Meta.DiscrTree     Mathlib.Tactic.Linter.OldObtain     Mathlib.Util.MemoFix
Mathlib.Lean.Meta.KAbstractPositions    Mathlib.Tactic.Linter.RefineLinter  Mathlib.Util.Qq
Mathlib.Lean.Meta.Simp          Mathlib.Tactic.Linter.Style     Mathlib.Util.SleepHeartbeats
Mathlib.Lean.Name           Mathlib.Tactic.Linter.UnusedTactic  Mathlib.Util.Superscript
Mathlib.Lean.PrettyPrinter.Delaborator  Mathlib.Tactic.Measurability.Init   Mathlib.Util.SynthesizeUsing
Mathlib.Lean.Thunk          Mathlib.Tactic.MinImports       Mathlib.Util.Tactic
Mathlib.Tactic.AdaptationNote       Mathlib.Tactic.Monotonicity.Attr    Mathlib.Util.TermBeta
Mathlib.Tactic.ApplyWith        Mathlib.Tactic.NthRewrite       Mathlib.Util.Time
Mathlib.Tactic.ArithMult.Init       Mathlib.Tactic.Observe          Mathlib.Util.WhatsNew
Mathlib.Tactic.Attr.Register        Mathlib.Tactic.PPWithUniv       Mathlib.Util.WithWeakNamespace
Mathlib.Tactic.Bound.Init       Mathlib.Tactic.ProjectionNotation

[Jon Eugster]

Ruben Van de Velde said:

but [import Batteries] would make more sense in the top level Mathlib.lean

As this seems an independent topic which so far everybody agreed on (see previous discussion on Zulip) here is a PR adding import Batteries in the mk_all script: #15810

[Damiano Testa]

And #15811 is the PR creating Mathlib.Init and importing it in all Mathlib files that do not import any Mathlib file.

[Damiano Testa]

I kept the file Mathlib.Init small: it only consists of a comment.

[Kim Morrison]

I would like some rules about Mathlib.Init (documented in the file):

• no bucket imports (Batteries/Lean/etc)
• every import has a comment explaining why the import is there
• strongly prefer avoiding files that themselves have imports beyond Lean, and when that is warranted there is a comment that explains the transitive imports

Having a bolus of imports at the bottom of everything unfortunately makes my life more difficult, so I would like to keep close control of what goes in this file.

That said, I agree there is room for putting some things here!

[Kim Morrison]

And I 100% agree that is is unacceptable for import Mathlib to not give you the kitchen sink, and I apologise that my past importing trimming has broken this. :-)

[Damiano Testa]

Should these rules just be written in a comment at the top of Mathlib.Init, or should there be some dedicated infrastructure (probably a linter) that tries to enforce them?

[Johan Commelin]

Let's start with just a comment. If that isn't sufficient we can scale up

[Michael Rothgang]

I think #15811 is good to go. (I wouldn't mind removing the script from that PR, but keeping it until a linter is added is also fine with me.)

[Damiano Testa]

Michael Rothgang said:

I think #15811 is good to go. (I wouldn't mind removing the script from that PR, but keeping it until a linter is added is also fine with me.)

I was going to expand a little on the comment that the file already has, basically explaining what Kim said above: should I do that, or is the PR good to go as is (assuming !bench is happy)?

[Michael Rothgang]

Either way is fine with me. That comment should be expanded - but I don't mind when this happens. (It should happen by the time that file gains actual content.)

[Damiano Testa]

I have a local version with the expanded comment and current master merged into it. I will push as soon as the bench results are in.

[Damiano Testa]

In case you are curious, this is the comment:

/-
This is the root file in Mathlib: it is imported by virtually *all* Mathlib files.

For this reason, the imports of this files are carefully curated.
Any modification involving a change in the imports of this file should be discussed beforehand.

Here are some general guidelines:
* no bucket imports (e.g. `Batteries`/`Lean`/etc);
* every import needs to have a comment explaining why the import is there;
* strong preference for avoiding files that themselves have imports beyond `Lean`, and
  any exception to this rule should by accompanied by a comment explaining the transitive imports.
-/

[Damiano Testa]

The entire !bench build failed, and I just pushed the update.

[Jon Eugster]

/-! right?

[Damiano Testa]

Ah, should it be a doc?

[Jon Eugster]

Might as well, or is there a reason not to make it the module docstring?

[Damiano Testa]

I updated and pushed it as a doc-module!

[Damiano Testa]

I was just wondering about the copyright linter, but we'll see if it complains!

[Damiano Testa]

Ok, the copyright linter is not happy, but I am just going to add an exception: I do not think that this file should have a copyright (or maybe yes, but not in my name!).

[Damiano Testa]

@Michael Rothgang the copyright linter was unhappy with no copyright (which is fine), but seems to be unhappy now again after I --updated the style exceptions: did I do something wrong? I simply ran $ lake exe lint-style --update and did not write by hand the exceptions.

[Michael Rothgang]

Let me investigate!

[Damiano Testa]

Thanks! The current failure is after the --update, the previous failure was when the copyright was missing.

[Damiano Testa]

(Only the latest failure is unexpected.)

[Michael Rothgang]

Ah! I see what is going on. (First off, running lake exe lint-style --update should do the right thing!) Secondly, what's happening is that lint-style.py complains about ERR_COP. It is not used any more to having copyright headers to ignore. If you put this into nolints-style.txt, everything is fine.

[Michael Rothgang]

I'll file a PR to recognise this error code back in lint-style.py, as long as it's still there.

[Damiano Testa]

Well, maybe the file should have a copyright, I do not know. I simply find that the copyright for this file should be maybe "the mathlib community", not me! :smile:

[Michael Rothgang]

Michael Rothgang said:

I'll file a PR to recognise this error code back in lint-style.py, as long as it's still there.

#15833

[Damiano Testa]

So, you are saying to add the same lines that were added to the exceptions also to the nolints file?

[Michael Rothgang]

Damiano Testa said:

So, you are saying to add the same lines that were added to the exceptions also to the nolints file?

No - just move them to nolints-style.txt instead.

[Michael Rothgang]

(Or decide to add a copyright header to Mathlib.Init.)

[Damiano Testa]

Michael Rothgang said:

Michael Rothgang said:

I'll file a PR to recognise this error code back in lint-style.py, as long as it's still there.

#15833

Does this mean that if this change becomes live, the exceptions should be moved back to the style-exceptions file?

[Damiano Testa]

(In case you are wondering, I am withholding pushing to the PR since these changes will mess up the lake build step, even though they do not actually affect the computed cache!)

[Michael Rothgang]

Not necessarily. There are two files for style exceptions. nolints-style.txt is meant for permanent exceptions (such as due to a simple-minded linter, or special files like this). style-exceptions.txt is for transient exceptions, and supposed to eventually become empty.

[Damiano Testa]

Ah, got it! Thanks for the explanation!

[Damiano Testa]

I just left the PR with bors!

[Michael Rothgang]

I've gone ahead and proposed #15845, to import all enabled mathlib syntax linters in Mathlib.Init. (This is just a first cut; I expect small refinements to be made.) Comments welcome!

[Michael Rothgang]

(And, of course, this will require fixing any linter complains which show up now that the linters run on larger parts of mathlib. There are certainly a fair number of "missing end" warnings.)

[Michael Rothgang]

The first prerequisite to landing #15845 has landed :tada:.
#15872 backports a few more fixes (+22, -7 lines; should be quick to review).
The remaining diff should be about +90, -50 lines, i.e. reviewable in itself.
@Kim Morrison I'm interested in your opinion on the linters moved to Mathlib.Init - I would of course prefer not to make your life harder by moving extraneous material into it.

[Jeremy Tan]

@Michael Rothgang how could I adapt the cdot linter to catch instances of $ used as <|?

[Damiano Testa]

Jeremy Tan said:

Michael Rothgang how could I adapt the cdot linter to catch instances of $ used as <|?

I think that the SyntaxNodeKind for $ is «term_$__», so you could probably latch onto that. In this case, $ and <| do not actually share the SyntaxNodeKind, so I do not think that you will need to look at the corresponding atom.

[Jeremy Tan]

This isn't working?

/-- The `dollarSyntax` linter flags uses of `<|` that are achieved by typing `$`. -/
register_option linter.dollarSyntax : Bool := {
  defValue := true
  descr := "enable the `dollarSyntax` linter"
}

namespace DollarSyntaxLinter

/-- `findDollarSyntax stx` extracts from `stx` the syntax nodes of `kind` `$`. -/
partial
def findDollarSyntax : Syntax → Array Syntax
  | stx@(.node _ kind args) =>
    let dargs := (args.map findDollarSyntax).flatten
    match kind with
      | ``«term_$__» => dargs.push stx
      | _ => dargs
  |_ => #[]

@[inherit_doc linter.dollarSyntax]
def dollarSyntaxLinter : Linter where run := withSetOptionIn fun stx ↦ do
    unless Linter.getLinterValue linter.dollarSyntax (← getOptions) do
      return
    if (← MonadState.get).messages.hasErrors then
      return
    for s in findDollarSyntax stx do
      Linter.logLint linter.dollarSyntax s m!"Please use '<|' and not '$` for the pipe operator."

initialize addLinter dollarSyntaxLinter

end DollarSyntaxLinter

[Jeremy Tan]

oh, it works

[Jeremy Tan]

#15913

[Eric Wieser]

Regarding style linters, can we move them to a separate file from non-style linters? We might even want a linter.style option that disables only the style linters and not the behavioral ones

[Michael Rothgang]

I'm happy to move them out (and even wondered such before). However, what is a "style linter" for you? Let me look at #15616 and the in-progress linters we have; what do you think about the following? I think it makes sense to think along the criteria of "is this a style linter" and "what is is default state?" (globally true, on in mathlib etc., off by default).
What do you think about the following? Perhaps actually making this change so should wait for #15616 and #15845 to land, to avoid modifying the same files over and over, but I'm happy to do so.

[Michael Rothgang]

Global linters, not style

• globalAttributeIn (globally on)
• haveLetLinter (off/only warn on in-progress proofs)
• dupNamespace (globally on)
• structureInType (globally on)
• unusedTacticLinter (globally on)
• the "confusing variables" linter #15400 (on in mathlib? globally? still under development)
• the "open classical" linter; the DecidableEq linter (on in mathlib? globally?)
• the checkAsSorry linter (on in mathlib? off in mathlib?)
• the "repeated typeclass assumption" linter #14731 (if/when that lands; probably off by default)
• the minImports linter (currently off by default)
• an eventual linter for a assert_not_exists existing could go here, and be on by default

Definitely style linters: some of these are specific to mathlib, but perhaps not all

• the multiGoal linter #12339 (on in mathlib)
• the "flexible linter" #11821 (off by default, for now)
• "cdot", "dollar sign" and "lambda syntax" linters (on in mathlib)
• "admit instead of sorry" (on in mathlib)
• "pedantic" linter (that might border on a baby formatter; off by default)
• "module docstring" linter #15794 (on in mathlib? on by default?)
• the `assertNotExists" style linter (on in mathlib)
• the "long line" and "long file" linters (on in mathlib)
• is "missing end" also a style linter? (on in mathlib)
• the terminal refine linter (off by default)

Something of a middle category

• hash commands" and set_option might be something else, as these are more about "this looks like debugging code in production?
• the oldObtain and refine linter are restriction lints (as Rust's clippy would call them)
• so is the papercut linter #13999 (perhaps off by default)

[Damiano Testa]

There is a proliferation of linters that target very specific style guidelines and have almost identical implementations:

• the cdot linter for · vs .;
• the dollarSyntax linter for <| vs $;
• the lambdaSyntax linter for fun vs λ;
• the admit linter for sorry vs admit.

Should these all have their own separate implementation as different linters, or should they be unified into a single linter that checks each one of these guidelines?

[Mario Carneiro]

from a performance perspective, they should be unified, but they may present as multiple linters (with e.g. separate options for turning them off)

[Damiano Testa]

Ok, I agree. I was thinking that they could take a Syntax option, rather than a Bool. Does this seem reasonable?

[Damiano Testa]

so you would do (untested) set_option linter.style <| true to activate one of them selectively.

[Mario Carneiro]

how does that relate?

[Mario Carneiro]

I'm saying that without changing the user-facing presentation of the linters, the linters should be implemented in a single pass with implementation in one file

[Mario Carneiro]

linter.style should not be a linter, that sounds like a class of linters

[Damiano Testa]

Right, this is also what I was thinking and I was trying to think about how to activate the unique linter for checking only one of the style guidelines at a time.

[Mario Carneiro]

they would just be set_option linter.dollarSyntax et al

[Damiano Testa]

Ah, and these options are not options of a linter that checks the syntax, but options that are read by a linter that then scans the syntax once and isolates whatever it should?

[Damiano Testa]

Let me try to explain: there would be an option for each one of dollar, lambda,... and a single linter that sees which ones of these options are on and flags the syntax accordingly.

[Damiano Testa]

Is this what you are suggesting?

[Mario Carneiro]

yes

[Damiano Testa]

I think that similar groupings may be desirable for other linters as well, especially the ones that inspect the infotrees, since those are actually expensive and some perform very similar checks.

[Damiano Testa]

This probably also means defining a function analogous to the logLint function but that works for non-Bool-valued options. Or maybe not, since the Boolvalued options exist anyway.

[Kim Morrison]

Michael Rothgang said:

I'm interested in your opinion on the linters moved to Mathlib.Init - I would of course prefer not to make your life harder by moving extraneous material into it.

Yes, I'm happy with these!

[Michael Rothgang]

May I then ping #15845 again, which is waiting for review?

[Michael Rothgang]

After merging, this PR fails in Data.String.Basic, for reasons I fail to understand. (Importing Batteries, for instance, does not fix it.) Does somebody have a moment to take a look and help?

[Ruben Van de Velde]

    simp only [compare, compareOfLessAndEq, instLT, List.instLT, lt_iff_toList_lt, toList]

looks like this now finds docs#compare instead of whatever it should be

[Ruben Van de Velde]

Probably much of Mathlib.Tactic.Linter.TextBased should be namespaced

[Michael Rothgang]

:bulb: I see now: the TextBased linter has a compare method, which shadows this one :man_facepalming: Thanks for the debugging help; I'll make a PR to namespace those declarations.

[Michael Rothgang]

#16203 namespaces the declarations for the TextBased linter

[Michael Rothgang]

#16212 moves the setOption linter option to style: should be a quick and easy review

[Michael Rothgang]

#16269 removes the text-based line length linter, as the longLine syntax linter is now transitively imported in every file (via Mathlib.Init).