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.