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.

[Michael Rothgang]

Can we have a linter for using the if tactic inside proofs? by_cases is usually much more readable.

[Michael Rothgang]

A few tactic analysis linters what would be great to have: look for pairs of tactics that can be combined.

• by_cases followed by push_neg in the second branch (-> by_cases!); similarly for by_contra and wlog
• rw followed by assumption (-> rwa)
• can we also look for rw followed by an exact which could be an assumption? edit: this might not be a good idea though, see below
• filter_upwards followed by intro

[Snir Broshi]

You can also combine two consecutive intro/intros/refine/apply/exact/exacts/use/existss if line length permits (usually, though I once encountered a case where combining breaks things)

[Jovan Gerbscheid]

I sometimes dislike rwa when reading proofs, because it doesn't tell me which assumption was used. Why is rwa even a thing in the first place?

[Ruben Van de Velde]

Okay, but then would you also remove (or frown upon) assumption?

[Michael Rothgang]

Snir Broshi said:

You can also combine two consecutive intro/intros/refine/apply/exact/exacts/use/existss if line length permits (usually, though I once encountered a case where combining breaks things)

Subsequent intros are already linted (by default). use or exists are a good idea, agreed.

[Michael Rothgang]

With refine/apply/exact/exacts, I'm not convinced by a general rule: combining these is not always a good idea, on my opinion.

[Anne Baanen]

Jovan Gerbscheid said:

I sometimes dislike rwa when reading proofs, because it doesn't tell me which assumption was used. Why is rwa even a thing in the first place?

rwa has a number of surprises: rwa at h does not mean h is used to close the goal, if rw closes the original goal but leaves a side condition then rwa tries to use assumption instead on that side condition, ...

[Jovan Gerbscheid]

Ruben Van de Velde said:

Okay, but then would you also remove (or frown upon) assumption?

I'm not saying we should ban assumption (for example all_goals assumption is a nice thing), but I think replacing exact h with assumption is not a good golf. And I don't think people would replace exact h with assumption very often, but the very fact that rwa exists is an incentive to replace exact h with assumption in the form of rwa.

[Damiano Testa]

I'm not a big fan of rwa either: there are situations where it is acceptable, but should not be used extensively, in my opinion.

[Michael Rothgang]

Two more ideas:

• have := something followed by positivity should be written positivity [something]
• have := something followed by finiteness should be written finiteness [something]
  Both cases only apply to reasonably short proof terms; I think "does the have use :=, no by and no name" should be a decent heuristic. I'm not sure if the tactic analysis framework has easy access to this information, though.

[Chris Henson]

This applies to grind as well, and I think you could also check if the have can be eliminated entirely.

[Jovan Gerbscheid]

Does grind have an unused argument linter yet? Or should we make one by simply trying to remove arguments one by one?

[Chris Henson]

I know there are places with unused args that I found while making the latest weekly linting PR, so I don't think so. Maybe this is not straightforward, because grind? doesn't suggest a minimal set either. When doing it by hand, I remove one by one.

[Ruben Van de Velde]

Anne Baanen said:

if rw closes the original goal but leaves a side condition then rwa tries to use assumption instead on that side condition, ...

Didn't that get fixed?

[Ruben Van de Velde]

Apparently not

[Kim Morrison]

Recording some linter ideas from #mathlib4 > Possible PR: Poisson integral and Herglotz representation @ 💬:

• ensure people write π, not Real.pi
• ensure neighbourhoods notation is used

[Kim Morrison]

(@Moritz Doll then replied saying he might be interested in writing a "properly use notation" linter.)

[Damiano Testa]

There is a deprecatedSyntax linter that can probably be used for this.

[Michael Rothgang]

I'll be happy to review a PR adding such a check!

[Moritz Doll]

Damiano Testa said:

There is a deprecatedSyntax linter that can probably be used for this.

Thanks that is a good reference, I found the cdotLinter, which is already pretty close. I want write a version where you can tag a notation, so that it automatically gets added to a list which the linter checks, so it is slightly more complicated

[Damiano Testa]

Making this genuinely user extensible seems a little tricky to "get right": the new command should have a place for the old syntax, one for the new syntax and one for the error message. Also, right now, these checks can be activated or deactivated individually. If you want to preserve that functionality, there should also be a mechanism that would create the various options.

[Damiano Testa]

One way to get started would be to move part of the logic to an environment extension, storing (deprecated syntax, preferred syntax, warning message).

[Kim Morrison]

Further linter requests:

1. Detect use of @ notation in term mode that isn't actually necessary.
2. Detect syntactically identical tactic branches e.g. X; \. Y; \. Y and suggest X <;> Y instead.
3. Detect when a tactic block generates a term that pretty prints with length < \epsilon * (length of tactic block), but doesn't need to "name lemmas" particularly more.

[Jovan Gerbscheid]

I think there should be a linter that checks whether definitions marked as meta are actually used for meta purposes. This would mean that it is either used in another meta definition, or that it is used to implement a tactic/attribute/command/elaborator/delaborator/app_unexpander/initialize etc.

And for files that are meta imported, there should be at least one definition in there that wasn't already marked meta, and satisfies the above criterion.

[Kim Morrison]

Could we have a linter for

refine ... ?_ ...
exact ...

but where substituting the exact into the refine results in a typechecking error?

[Kim Morrison]

The general pattern of refine followed by exact is okay for pedagogical purposes ("here is the structure of the term I need, but there are some tedious proofs I will defer until later" --- although even then refactoring to a have followed by an exact seems much clearer as long as the type annotation on the have is not insane), but I would really like to avoid using refine then exact to achieve some more complicated elaboration guidance that is not explained in the source.

[Kim Morrison]

Perhaps, before having such a linter, reviewers could simply watch out for this antipattern and flag it.

[Kim Morrison]

I would like to point out some examples of this antipattern, introduced in #20041, which today wasted my time diagnosing when their elaboration changed slightly, and I was dumped into a type-checking problem without enough context. I've PR'd a change to these proofs in #35059; I'm not claiming that the replacement proofs are particularly better except that they work on both master and nightly-testing. If someone would like to replace them again in a follow-up PR that would be great.

[Kim Morrison]

Linking to #mathlib4 > Type typo @ 💬, containing a discussion about a linter for Type in arguments of declarations (it's fine in return types). Someone would need to survey the existing exceptions.

[Johan Commelin]

Kim Morrison said:

Perhaps, before having such a linter, reviewers could simply watch out for this antipattern and flag it.

It is somewhat hard to spot this, right? Because half of the time, it might pass as "pedagogical purposes" if you don't inspect very carefully.

[Michael Rothgang]

Would you like to help with writing a linter? A linter is even better than relying on manual review :-)

[Johan Commelin]

Not sure if you are asking me or Kim. But I currently don't have the skills to write that linter, and don't have the time to learn those skills :sad:

[Damiano Testa]

I think that the tactic framework that Anne developed should make that fairly accessible, but I am not currently able to volunteer for this task!

[Chris Henson]

The tactic analysis framework part seems straightforward, but what would be the best way to identify which ?_ corresponds to the term from exact?

[Michael Rothgang]

Would linting for refine followed by exact (and the goal is closed then) --- but where the equivalent exact call fails, do the trick? It would catch some of the errors above, at least.

[Chris Henson]

Yes, detecting refine followed by exact seems most straightforward and limits you to roughly this. My question was about how to distinguish between the holes that are solved by unification versus where we want to replace with the term from exact.

[Jovan Gerbscheid]

When using refine, the holes solved by unification are written as _, and the holes that leave a new goal are written as ?_. So you should be able to tell this purely from the syntax.

[Chris Henson]

They should be written this way, but nothing is stopping you from writing ?_ where _ should be used, right? Otherwise, I agree.

[Damiano Testa]

I agree with what Jovan said. There are some rare cases where this may not apply, but you may uncover situations were you can replace ?_ by _ and maybe you should!

[Damiano Testa]

refine should mostly fail, if you tell it to not unify stuff that it could.

[Damiano Testa]

If you just look for refine followed by exact there will be a lot of cases where this was a decision due to line length or proof readability, so checking the failure of the replacement will really be essential, I think.

[Chris Henson]

If okay for the linter to also identify these replacements of ?_ for _, then then it seems fine to replace the first ?_ syntactically and rerun the tactic, as the tactic analysis framework allows. This seems to make most sense as an addition to the weekly linting set.

[Chris Henson]

(And as you say, just report a warning on failure because most times it will still succeed.)

[Jovan Gerbscheid]

If a refine creates one goal, and the number of ?_ is not one, then something fishy is going on and so I'd say it's worth having a linter warning for this too.

[Floris van Doorn]

Kim Morrison said:

Could we have a linter for

refine ... ?_ ...
exact ...

but where substituting the exact into the refine results in a typechecking error?

I'm not sure that this is a antipattern in general.
If the elaborator needs help, this pattern is an easy way to tell it "elaborate this argument last".
What is the proposed fix if this linter fires? Give more implicit arguments explicitly?

docs#LibraryNote.comp_of_eq_lemmas contains a concrete example: suppose we want to prove the following in term mode without using docs#ContinuousAt.comp_of_eq.

import Mathlib

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} (f : X → X → Y)
    (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
    ContinuousAt (fun x ↦ f x x) x₀ := by sorry

Now the following isn't pretty, but how would you like it to be formatted instead? (The linter should probably give such instructions):

import Mathlib

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} (f : X → X → Y)
    (hf : ContinuousAt (Function.uncurry f) (x₀, x₀)) :
    ContinuousAt (fun x ↦ f x x) x₀ := by
  refine ContinuousAt.comp (g := Function.uncurry f) ?_ (continuousAt_id.prodMk continuousAt_id)
  exact hf

[Floris van Doorn]

Chris Henson said:

They should be written this way, but nothing is stopping you from writing ?_ where _ should be used, right? Otherwise, I agree.

Can you give an example where you can use both ?_ and _ in a refine, and Lean doesn't give an error in either case? I think that Lean (mostly) checks that you're using the correct one.

[Chris Henson]

Maybe this is too minimized, but I had in mind examples like

import Mathlib

variable {G : Type u} [inst : AddCommMagma G] (a b : G)

example : a + b = b + a := by
  refine @add_comm G _ a b

example : a + b = b + a := by
  refine @add_comm G ?_ a b

where you could easily write either for an instance parameter while typing quickly.

[Jovan Gerbscheid]

Ah I see! Indeed I think having a linter warning for this would be nice.

[Chris Henson]

Maybe this should be a separate linter? Based on the original discussion I have written an initial version of a linter using the tactic analysis framework. It's not more than a dozen lines when limited to finishing exact/refine, so I think the more important piece is Floris's questions about if this is really an antipattern and what the suggested alternative is.

[Jovan Gerbscheid]

I think what is causing the problem in the original example that Kim Morrison encountered is that there was a ▸ rewrite happening inside the refine, making the proof much more brittle.

[Eric Wieser]

(deleted)

[Michael Rothgang]

@Robin Carlier said on github:

Perhaps we could even consider linting against exposed Classical.choose _, forcing APIs to provide both the definition and a characterizing property?

[Kim Morrison]

I was considering whether we could write a linter about rfl theorems of the form theorem foo : f args = value := rfl which were not labelled as @[simp]. Probably this should be restricted to cases where f is defined the in same file as foo.
There would be some false positives, surely, so some extra noise to turn these off. But this seems to be a quite common reviewer suggestion that turns up in PRs, so is high value from the point of view of automating review work.
Recent examples: #35432 (@Oliver Nash)

[Kim Morrison]

Another one we could do is have a (user extensible via registration) list of types, e.g. Equiv, Iso, Functor, LinearMap, ... where it is a linter warning if you fail to write @[simps] or have at least some simp lemmas for projections?
Again, this comes up regularly in manual reviews. This might be a bit harder to specify well, however, and it may only work as an environment linter, because it has to wait to see if simp lemmas are written manually after the definition.
Recent examples: #35452 (@Robin Carlier / @Joël Riou)

[Kim Morrison]

Another one is arguments duplicated with section variables. Maybe the test is just "can any argument which has identical type to something in the current section variables (are those even available to a linter?) be omitted without changing the elaboration of the theorem?"
Recent examples: #35479

[Kim Morrison]

And then we could lint (only as an environment linter), for named instances where the name is never used in Mathlib.
Recent example: #35488

[Robin Carlier]

A thing to keep in mind about linting against named instances is that when the instance carries data and has a @[simps] tag, naming it is a way to somehow control the name of the resulting lemmas even if the instance name is not explicitly mentioned in Mathlib.

[Violeta Hernández]

What about a linter for public declarations containing the word aux? There seem to be hundreds of these. And surely we'd prefer for these to have better names, or be private altogether.