linter requests

Stream: mathlib4

[Matthew Ballard]

Perhaps a separate topic to record these is useful?

I have one: a linter that warns you if you are building data using tactics.

[Damiano Testa]

Oh, this could leverage a lot of the have vs let linter.

[Joseph Tooby-Smith]

Maybe this is not possible or already exists, but I would love to have a linter that checks for pointless parentheses (i.e. pairs of parentheses that can be deleted with no ill effect).

[Damiano Testa]

Linters can do a lot of things and this is certainly in scope!

[Damiano Testa]

There is a "pedantic" linter in the works that checks how closely your code matches the output of pretty-printing it. I suspect that unnecessary parenthesie are there too, but there is a lot. (#15535)

[Michael Rothgang]

#15941 looks at some of its warnings on mathlib: help fixing these (if appropriate) or merging some of the fixes is welcome.

[Violeta Hernández]

Would it be possible to have a linter for putting hypotheses in variable? From what I understand doing so is not ideal

[Yaël Dillies]

It would, but I have argued it is ideal in some situations

[Violeta Hernández]

Here's another idea: a linter for using Type instead of Type*

[Michael Rothgang]

One a linter when using Type _ instead of Type*. (This was discussed before; in a calm moment, I'll edit in the link.)

[Adomas Baliuka]

Just for completeness sake: "a linter that flags unwanted unicode".

I have no idea how to implement it technically (been reading the metaprogramming book but not sure how to parse individual characters) and also there would need to be some discussion about what "unwanted" should be. (My suggestion would be "everything that's not on a whitelist, which can grow over time").

Previously discussed here

[Michael Rothgang]

Adomas Baliuka said:

Just for completeness sake: "a linter that flags unwanted unicode".

I have no idea how to implement it technically (been reading the metaprogramming book but not sure how to parse individual characters) and also there would need to be some discussion about what "unwanted" should be. (My suggestion would be "everything that's not on a whitelist, which can grow over time").

Previously discussed here

In terms of infrastructure, you could certainly piggy-back on the text-based linters in Mathlib.Tactic.Linter.TextBased (or try to use a syntax linter... but that might be harder/you may have to distinguish more cases). The former are text-based, so have no understanding of Lean syntax (in particular, the linter would also complain about using unicode symbols in comments etc., which might actually be fine).

Or is your question more about the "splitting the string into unicode codepoints"?

[Michael Rothgang]

(Though, searching for "is this a substring" hopefully would side-step this question.)

[Adomas Baliuka]

(deleted)

[Michael Rothgang]

Looks like a reasonable start. Perhaps the following is obvious to you (in that case, please proceed), otherwise:

• you need to define a newUnicode variant of the styleError
• you should add your linter to allLinters
• Right now, your check is not quite what we want, as it would also complain about the letter a, the number 0 or some common symbols. But the idea works.

[Michael Rothgang]

(Edit: I see you deleted your post now. It contained a start towards linting against the above.)

[Adomas Baliuka]

@Michael Rothgang Thanks! I deleted because I didn't want to hijack this thread and, as you said, had to do some more modifications that cannot be usefully shortened into what could be posted here. I think I will just make a PR and see what happens.

[Violeta Hernández]

How about: linter for theorem and instance names that are too long!

[Violeta Hernández]

We've got a bunch of bad autogenerated instance names like docs#NumberField.instIsLocalizedModuleIntNonZeroDivisorsSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealRestrictScalarsSubtype, which are so long you can't even call them explicitly without triggering the long line linter

[Violeta Hernández]

And they clutter search results on the docs

[Yaël Dillies]

Violeta, you have no idea what instance names we had when you were away :face_with_hand_over_mouth:

[Rida Hamadani]

I still come across the old instance names while searching for lemmas on moogle.ai, some of those can fill my whole screen!

[Tristan Figueroa-Reid]

Would collapsing subsequent calls of subst be a good linter? (Are there any linters that look at adjacent tactic calls at all, like collapsing rw/rwa ... and assertion to rwa?)

[Damiano Testa]

A brief check suggests that there are about 15 files containing consecutive substs.

[Damiano Testa]

In terms of actual implementation of the linter, I do not think that there are already linters that check consecutive tactics "syntactically". There are some linters that track metavariables, looking for two tactics modifying a given goal in sequence (possibly with some different intervening tactics in-between). If you decide to do the metavariable-tracking, then the linter will be quite a bit more involved.

[Damiano Testa]

Here are a couple of examples of some straightforward and not-so-straightforward lints:

example {a b c} (ha : a = 0) (hb : b = 0) (hc : c = 0) : a = b + c := by
  subst ha
  subst hb
  subst hc
  rfl

example {a b c} (ha : a = 0) (hb : b = 0) (hc : c = 0) : a = b + c := by
  subst ha; subst hb
  subst hc
  rfl

example {a b c} (ha : a = 0) (hb : b = 0) (hc : c = 0) : a = b + c := by
  subst ha
  apply id
  subst hb hc
  rfl

example {a b} (ha : a = 0) (hb : b = 0) : a = b ∧ True := by
  constructor
  subst ha
  case right =>
    trivial
  subst hb
  rfl

[Damiano Testa]

Some of the substs above are "syntactically" consecutive, others are "semantically" consecutive.

[Damiano Testa]

There are some ongoing discussions about general linter performances, but the idea of collapsing consecutive substs seems reasonable. Still, unless this is intended mostly as a learning exercise, try to gather some support, since every new linter means adding more potential warnings and there is a fine balance between being useful and being annoying!

[Damiano Testa]

There are a few linters that maybe should not be running constantly, but rather every once in a while in an automated process and I think that this linter would be one of them: it is rare to have consecutive substs, so having the linter constantly running may be a little wasteful, but it is also good to clean up code, even if "after the fact".

[Damiano Testa]

This kind of periodic clean up is not automated, but I have been thinking about it for some time and would like to see it implemented.

[Bolton Bailey]

Tristan Figueroa-Reid said:

Would collapsing subsequent calls of subst be a good linter? (Are there any linters that look at adjacent tactic calls at all, like collapsing rw/rwa ... and assertion to rwa?)

I have added this to the wishlist, along with some of the earlier suggestions @Violeta Hernández and @Matthew Ballard made, hope that's all right.

[Michael Rothgang]

My wish for today: write a "low-level performance optimisation tactic linter", which tries to replace one tactic with a "faster" one if that is possible. Let's use the replacement "continuity -> fun_prop" as an example. This cannot always be done, but if it can, fun_prop is usually faster (sometimes by a lot). This linter would tell you "this continuity call can be replaced by fun_prop" could be useful.

More specifically, I'm thinking of a syntax linter which does the following, for every pair (slower_tactic, faster_tactic).

• look for occurrences of the slower_tactic tactic
  • careful: do ignore default parameters
  • occurrences inside proofs (of theorems, instances or definitions) should be fine
• try to replace this by the faster_tactic tactic
• elaborate the result: if there are no errors, print a message about the replacement. Otherwise, do nothing.

As a start, the pair (continuity, fun_prop) and (measurability, fun_prop) could be a start.

[Michael Rothgang]

@Damiano Testa In case you're bored and want to write a performance-enhancing linter instead :-)

[Damiano Testa]

My experience with figuring out what is faster using linters is that it is hard to avoid "caching": linters will usually re-elaborate some syntax that has already been elaborated and, in the process, will have access to cached computations. This makes speed tests performed by linters somewhat unreliable.

[Bolton Bailey]

Michael Rothgang said:

As a start, the pair (continuity, fun_prop) and (measurability, fun_prop) could be a start.

Seems like something tryAtEachStep could be helpful with.

[Michael Rothgang]

Damiano Testa said:

My experience with figuring out what is faster using linters is that it is hard to avoid "caching": linters will usually re-elaborate some syntax that has already been elaborated and, in the process, will have access to cached computations. This makes speed tests performed by linters somewhat unreliable.

Good point! In the case of fun_prop and continuity, in my experience the former is ~always a lot faster, so I don't need any speed comparisons. Telling me which ones can be replaced should suffice. :-)

[Violeta Hernández]

A pair I've encountered a few times is (aesop, simp_all).

[Tristan Figueroa-Reid]

Michael Rothgang said:

More specifically, I'm thinking of a syntax linter which does the following, for every pair (slower_tactic, faster_tactic).

• look for occurrences of the slower_tactic tactic
  • careful: do ignore default parameters
  • occurrences inside proofs (of theorems, instances or definitions) should be fine
• try to replace this by the faster_tactic tactic
• elaborate the result: if there are no errors, print a message about the replacement. Otherwise, do nothing.

Since I imagine that this would be very slow like tryAtEachStep, it might be a good idea to categorize these slow linters in such a way that one could manually run them for a specific file/theorem: one could use this to golf-lint only files changed in a PR, for example. (This could also contain linters regarding simp - for example, permuting simp only calls with multiple theorems to see if there exists a potential call to simp_rw)

(note: I just noticed that this was mentioned about 10 messages ago - since this is being brought up more often, though, it might be a good time to consider implementing such a system.)

[Tristan Figueroa-Reid]

Also (taking advantage of the slowness of this linter) it would be nice if that tactic was transitive - e.g. cases when simp_all can just be simp.

[Robin Carlier]

The file file#CategoryTheory/Bicategory/Functor/Lax has this in its first few non-docstring lines

open Category Bicategory

open Bicategory

Of course, removing the second open does not impact the file.

Can we lint against reopening an already-open namespace?

[Ruben Van de Velde]

Perhaps one used to be open_locale

[Yaël Dillies]

Robin Carlier said:

Can we lint against reopening an already-open namespace?

This is probably incredibly difficult since eg open Foo Bar Foo means

1. "Open Foo"
2. "Open Bar and Foo.Bar"
3. "Open Foo, Bar.Foo and Foo.Bar.Foo"

[Michael Rothgang]

True - but there is a different, more pragmatic way: lint in "superfluous opens". Whenever an open statement can be removed and the file still compiles, emit a warning that the open statement is superfluous.

[Michael Rothgang]

There is an "unused variable" linter by Damiano Testa (which should be very similar in terms of implementation), so you can probably copy a lot from there.

[Michael Rothgang]

The hardest part might be fixing all violations in mathlib :-)

[Ruben Van de Velde]

Speaking of, @Damiano Testa, did you ever finish that work?

[Damiano Testa]

No, I got tired of the mindless PRs after many iterations! I can try to pick it up again, but it was not especially fun! :slight_smile:

[Damiano Testa]

In terms of the "duplicated open" linter, there are exceedingly few declarations that have a repeated namespace, almost all in core with repeated Lean. I'll try to give an exhaustive list later, when I'm back at a computer. I have not investigated how many namespaces appear in different orders throughout mathlib, but I suspect that most repeated opens could be removed.

[Ruben Van de Velde]

@Damiano Testa DO you mind if I merge master into #17715?

[Damiano Testa]

Of course not: feel free to do that and remove some unused variables!

[Damiano Testa]

There are some incorrect answers that I already know, but almost all warning should be correct.

[Damiano Testa]

You have to wait until the end of the file has been parsed before you get any warning though.

[Damiano Testa]

(I don't remember how Elab.async affected the linter, though.)

[Ruben Van de Velde]

Done, will see what comes out

[Ruben Van de Velde]

Not much -

argument
  es.getElems
has type
  TSyntaxArray `Lean.Parser.Command.structParent : Type
but is expected to have type
  Array (TSyntax `term) : Type

That's not gonna be for me today

[Damiano Testa]

When I'm back at a computer, I'll try to fix it and will report here!

[Damiano Testa]

I have not forgotten about this, I tried fixing the linter, but there are some deeper changes that have affected the linter: I need to think about how to make it work again!

[Damiano Testa]

Yaël Dillies said:

Robin Carlier said:

Can we lint against reopening an already-open namespace?

This is probably incredibly difficult since eg open Foo Bar Foo means

1. "Open Foo"
2. "Open Bar and Foo.Bar"
3. "Open Foo, Bar.Foo and Foo.Bar.Foo"

It turns out that Lean already stores all the various open namespaces conveniently, so the linter does not have a lot of extra work to do.

[Damiano Testa]

In #25362 there is a draft linter, which still needs work, but I will not have time to think about it.

[Damiano Testa]

#25361 contains the first few exceptions that the linter flagged.

[Damiano Testa]

Now that the linter ran on all of mathlib, it reports that there are approx 500 files with a duplicated open.

[Michael Rothgang]

(Does this also handle the case "open Foo" cannot be removed, but replaced by "open scoped Foo"?)

[Damiano Testa]

No, this is simply checking whether the new open namespace creates a duplicated open namespace.

[Damiano Testa]

Checking whether open scoped would be enough is harder, since I am not sure that there is any record in the environment of which declarations used open/open scoped, other than that they have been added to the environment.

[Damiano Testa]

By the way, the linter does not detect whether an open is unused, it merely detects if it is superfluous, since the namespace is already open.

[Damiano Testa]

And even the "superfluous" part may have false positives, due to potential intricacies in how namespaces can look like. In the files that I looked at, there were no false positives, but sometimes it was not entirely straightforward to figure out which opens to remove/reorder.

[Damiano Testa]

Since this came up, the linter does not prevent opening a namespace and not using it. It simply prevents that an already open namespace is opened again. So, open X X is not allowed, but section open X end is allowed.

[Tristan Figueroa-Reid]

This was discussed in #Is there code for X? > weaker wlog, but we should have a linter for uses of wlog without this to recommend some equivalent, more descriptive tactic. It is still up in the air what to recommend (by_cases with a negated statement seems to be the most used equivalent form from the conclusion of that conversation).

[Robin Carlier]

Can we lint against universes mvars? See #mathlib4 > `grind ext` and universe-level metavariable

I think the issue described in this thread shows that these are actually tech debt (they are breaking future automation, and slow things down), and I believe we’re quite in debt in Mathlib.

[Michael Rothgang]

So, an 80% solution would be to lint on Category that is not Category.{v} , right?

[Robin Carlier]

Yes, that would be good already!

[David Ang]

Can there be a linter that discourages => in favour of \mapsto (or the other way)?

[Michael Rothgang]

That linter is easy to write. The hard part is forming consensus on it. If you do the latter, I'm happy to do the former.

[Michael Rothgang]

(And we just need a volunteer to fix the several thousand such occurrences in mathlib. :-))

[Aaron Liu]

can't we just be inconsistent

[Ruben Van de Velde]

Or can we lint in the other direction? :innocent:

[Dexin Zhang]

I don't know whether it is technically possible, but I hope for a linter to detect instance diamonds in variables.

[Violeta Hernández]

What about a linter for universe-polymorphic types which have been initialized at universe 0?

[Violeta Hernández]

This can of course be intentional, so you should be able to disable the linter, but it can also lead to some really annoying to debug problems.

[Violeta Hernández]

(I'm thinking things like Ordinal.{0}, Cardinal.{0}, etc.)

[Eric Wieser]

Can we lint against the use of ↑ in places where it expands to a no-op?

[David Loeffler]

We have a linter that detects absence of a focussing dot when there are multiple goals. Can we have the converse, i.e. a linter that detects presence of unnecessary focussing dots when there is only a single goal anyway? I've often seen this in PR reviews.

[Violeta Hernández]

How would you differentiate the last dot in a set from a dot all on its own?

[Michael Rothgang]

That linter exists in a PR (I can dig up the PR later) --- the question was how to phase in that linter, as there are a many (if I remember correctly, in the order of 2000 violations). Writing an auto-fixer for this would be nice, and is perhaps not too difficult --- there was recent discussion in this direction.

[Michael Rothgang]

These PRs are #12411 and #12416 --- which contains both the linter implementation as well as a number of mathlib adaptations (which are by now thoroughly outdated).

[Damiano Testa]

The last dot in a set already gets special treatment, in that it is allowed, but not required.

[Damiano Testa]

I forget the details, but I think that this was still the case for the stricter multiGoal linter: it requires cdots in the right places, but the last one is optional.

[Damiano Testa]

If I remember correctly, the way in which it worked is as follows. Assuming that indentation is correct, which the current linter almost guarantees, you can then deduce syntactically where a proof ends and then work your way backwards to where it should have started.

[Bolton Bailey]

I think there is an issue in that whether or not to put the last dot is sometimes a matter of taste and perhaps should be up to the contributor. For example, if there is a by_cases, you may or may not want that the second case has a focusing dot depending on whether or not the first case is considered a trivial side case.

[Eric Wieser]

Should the dot be forbidden in:

rw [close_the_main_goal_with_some_hyp]
. rw [close_the_side_goal]

[Eric Wieser]

The dot here acts as a partial indication that this can't be combined into a single rw

[Damiano Testa]

I don't have a strong opinion for what the linter should do with the non-mergeable rw. What it very likely does is to flag that cdot as redundant. Tracking metavariables across tactic calls is usually straightforward, but can be arbitrarily complicated, and the linter defers almost all of its logic to simply counting how many goals are present. So, one goal means "same" goal, even if it really should be a side goal.

[Damiano Testa]

The flexible linter has a somewhat more refined view on metavariable tracking, but the multiGoal mostly (maybe only) tracks number of available goals before and after the tactic calls.

[Snir Broshi]

Hello, I'd like to suggest a linter for unnecessary usage of |> and <|:

def foo := Nat.fib |>.Injective
def bar := Nat.fib <| 5

I like using these but sometimes after a refactor they become unnecessary, and I don't always notice. Thoughts?

[Snir Broshi]

Also in a similar vein, a linter that forces using <| or |> or dot notation where possible. e.g.

• Polynomial.degree X => X.degree
• Nat.fib (2 * 3) => Nat.fib <| 2 * 3
• (2 * X).degree => 2 * X |>.degree

These are style choices so I'm not talking about enabling them in mathlib, but rather letting users choose to enable them on their local VSCode

[Damiano Testa]

Personally, I find that

• Nat.fib (2 * 3) => Nat.fib <| 2 * 3
• (2 * X).degree => 2 * X |>.degree

is opposite to my preference.

[Jovan Gerbscheid]

We could have a linter that suggests to change replace h into have h if there was no variable h before.

[Ruben Van de Velde]

And perhaps for obtain when there's no pattern, just an identifier

[Snir Broshi]

This simp_rw can be replaced with either simp or rw (with the same list of lemmas), and if it's replaced with simp we can remove the first 3 lemmas (though the unused simp linter doesn't flag them all).
Maybe a linter that suggests such replacements is good? Though simp_rw might have benefits I'm not aware of, maybe it's faster

[Jovan Gerbscheid]

There is a benefit of simp_rw over simp that you can see all of the rewrites happen in the infoview as you move your cursor through the list of arguments. This is the same as in rw.

[Ruben Van de Velde]

Additionally, if your simp_rw call breaks, you'll typically know exactly at which point things start to go wrong. And sometimes simp [...] can be sensitive to the order that it applies the lemma - for example if you have a lemma that simplifies f x = y but you also added eq_comm which should only apply after the first lemma

[Snir Broshi]

So replacing simp_rw -> rw (when possible) is always non-worse (same or better), right?

[Ruben Van de Velde]

Unless it has weird performance impact, or it implies splitting a single simp_rw into alternating rw/simp_rw, I think I'd agree with that

[Harald Husum]

In the draft pull request #31386 i have a couple of python scripts that I've used to detect and fix files that had more than one H1 header in docstrings. After processing the results, I found that there were almost no false positives among the >100 files flagged.

This makes me wonder whether the detection script could be transformed into a useful linter. Not sure whether this is something I want to invest effort in yet, but I thought I should air the possibility in order to get a sense of how valuable community members would perceive this to be.

[Damiano Testa]

The current python linters that are present in mathlib are mostly considered technical debt, waiting to be replaced by Lean scripts.

So, I would prefer if this were Lean-based, rather than python-based.

[Bryan Gin-ge Chen]

At some point we'll be switching to using Verso in our docstrings, so if we want to lint docstrings, it might be worth looking into whether we should build something using that. (FWIW it looks like the markup for headers is the same as in markdown)

[Chris Henson]

I agree that it is best to wait for Verso docstrings for this kind of linter, because it seems much more reliable once there is a robust markdown-like parser that can be used to identify headers.

[Harald Husum]

Thanks for the feedback, guys. FWIW, I took it for granted that it would have to be ported to Lean. But waiting for Verso seems like a good idea.

The last PR with fixes of these issues was merged today, so hopefully there won't be too many files to deal with when the time comes to make a linter out of this.

[Calle Sönne]

A potential linter could be one checking for "bad" uses of constructors (ones which abuse def-eq). By this I mean that certain types come with a preferred constructor that is not the standard one, e.g. in category theory we have the constructor Prod.mkHom that avoids def-eq abuse:

/-- Construct a morphism in a product category by giving its constituent components.
This constructor should be preferred over `Prod.mk`, because lean infers better the
source and target of the resulting morphism. -/
abbrev mkHom {X₁ X₂ : C} {Y₁ Y₂ : D} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) : (X₁, Y₁) ⟶ (X₂, Y₂) :=
  ⟨f, g⟩

The linter could work by having a list of "preferred constructors", so in this case whenever a morphism of type (X₁, Y₁) ⟶ (X₂, Y₂) is constructed using the standard constructor, the linter would flag this, and ask the user to either disable the linter if the reason is good, or use mkHom(which also comes with notation). The reason I ask is that the file that defines Prod.mkHom itself is riddled with uses of the old constructor as well!

I couldn't find if this had been suggested before.

[Yaël Dillies]

Calle Sönne said:

in category theory we have the constructor Prod.mkHom that avoids def-eq abuse

It is certainly not meant to avoid defeq abuse. It's instead meant to help unification out

[Yaël Dillies]

I am more and more leaning towards the stance that anything counting as defeq abuse should be completely disallowed by setting the transparency or visibility appropriately. Eg if a constructor is truly meant not to be used, then it should be private.

[Yaël Dillies]

There's a master student at my uni playing around with detecting defeq abuse, and it's been a nightmare explaining him the rules :half_frown:

[Chris Henson]

Is there documentation that spells out these defeq abuse rules?

[Calle Sönne]

Yaël Dillies said:

Calle Sönne said:

in category theory we have the constructor Prod.mkHom that avoids def-eq abuse

It is certainly not meant to avoid defeq abuse. It's instead meant to help unification out

Okay I don't actually know what "defeq abuse" means exactly, but have I understood correctly that its there to help out simp?

[Calle Sönne]

Yaël Dillies said:

I am more and more leaning towards the stance that anything counting as defeq abuse should be completely disallowed by setting the transparency or visibility appropriately. Eg if a constructor is truly meant not to be used, then it should be private.

Well in this case this would mean making Prod.mk private which I don't think is a good idea.

[Yaël Dillies]

Defeq abuse happens when we set our declarations to the secret "human-irreducible" transparency that Lean doesn't know about

[Yaël Dillies]

Calle Sönne said:

in this case this would mean making Prod.mk private which I don't think is a good idea.

No, that's not really what it means. It instead means that (X₁, Y₁) ⟶ (X₂, Y₂) should be defined as a custom one-field structure whose constructor should be made private.

[Aaron Liu]

I still don't get it. If I have a definition and I have a bunch of places I'm using it how do I tell if it's defeq abuse?

[Yaël Dillies]

You can't. That's my point

[Yaël Dillies]

That's why we should be more diligent making things private/irreducible so that the only available spelling of an operation is the preferred one

[Calle Sönne]

Okay I agree with this :)

[David Loeffler]

PR #32587 fixes some trivial documentation mis-formatting which is caused by the presence of "non-breaking space" Unicode characters (which look identical to usual spaces but aren't read as such by the docs compiler). @Violeta Hernández and I both agree it would be nice to have a linter against this – I'm not sure there's any good reason for a non-breaking space ever to appear in a Lean code file.

[Michael Rothgang]

This would be an easy text-based linter - happy to review a PR!

[David Loeffler]

Non-breaking space linter PR up at #32646.