style proposal: avoid `variable {X} ... variable (X)`

Stream: mathlib4

[Kim Morrison]

A proposal for the style guide. Let's avoid

variable (X)

def foo := ...

variable {X}

in favour of

variable (X) in
def foo := ...

[Kim Morrison]

I would propose that this is "encouraged" rather than required for now, but also that we investigate the possibility of a linter for this.

[Kim Morrison]

I find this style both easier to read, and easier to maintain.

[Kim Morrison]

(I think anytime you need to change the explicitness for two or more consecutive declarations, there should not be any recommendation between repeated variable ... in and changing twice. This can be left up to individual judgement. It's just switching back and forth for a single declaration which I'd like to discourage.)

[Eric Wieser]

I assume we are still fine with

variable {X}

...

section
variable (X)

...

end

...

for when a whole group of declarations want explicit arguments?

[Kim Morrison]

Yes, certainly. This proposal is only about switching the explicitness back and forth before and after a single declaration.

[Eric Wieser]

This isn't something we can lint for because it spans multiple commands, right?

[Kim Morrison]

It would require more complicated linting mechanisms, at least. :-)

[Damiano Testa]

Similar linting mechanisms already exist, though they tend to be brittle to editing code.

[Damiano Testa]

Would it be possible to have a version of Linter that skips the "revert the environment" step? That would allow much better tooling for things such as this one.

[Damiano Testa]

Actually, docs#Lean.Elab.Command.Scope stores the Syntax of the latest variable. Hence, if the linters had access to the scope before a binder update (and there is an RFC that even more than that will become accessible to the linters), then linting this would be probably more robust.

[Damiano Testa]

In case it was too implicit, the Syntax stores position as well, so then you can meaningfully compare the position of the variable commands and the positions of the declarations added in-between them.

[Damiano Testa]

This can be done in an "untouched file" currently. So, it could be a CI linter, or a local one, in case you want to turn it on, but refresh the file if you modify and want up-to-date information.

[Damiano Testa]

There is a prototype at #22389.

[Damiano Testa]

The first flagged issue appears to be docs#Subgroup.gi.

[Damiano Testa]

Next flags are: docs#QuotientGroup.leftRel_apply and docs#QuotientGroup.rightRel_apply, that also look like correct suggestions from the linter!

[Damiano Testa]

The linter flagged 218 exceptions in mathlib.

[Damiano Testa]

#22396 is a first batch of replacements.

[Damiano Testa]

I did it by hand, to make sure that there were no surprises and I think that I can "trust" the linter.

[Damiano Testa]

So, if these changes look ok, I will automate them and produce a second PR with all the exceptions automatically performed.

[Bhavik Mehta]

These all look completely reasonable to me. One slightly odd case is in https://github.com/leanprover-community/mathlib4/pull/22396/files#diff-0300e937246e2c2df8beadd533f7ef501eec68b7ee24aba2d24f7f10883a31ad. The previous version was clearly bad, switching back and forth four times, but I wonder if there's a cleaner replacement? I suspect not, but I wanted to mention it anyway in case others have ideas.

[Damiano Testa]

Bhavik, thanks! I have not checked, but maybe I can disentangle the declarations, so that first come all with one setting, then all the others.

[Damiano Testa]

Curiously, this is also the only place where I added a modification that had not been flagged by the linter, since the final variable update involved more than one variable, but the linter only focuses on single variable updates.

[Riccardo Brasca]

Independently of the linter #22396 is clearly an improvement. I've delegated it. Feel free to merge or wait if you want more time to test the linter.

[Bhavik Mehta]

Damiano Testa said:

Curiously, this is also the only place where I added a modification that had not been flagged by the linter, since the final variable update involved more than one variable, but the linter only focuses on single variable updates.

Just to make sure I'm understanding you correctly, the linter flagged the other two, and this one was added manually?

[Damiano Testa]

Bhavik, that is correct. The linter "saw"

variable (k)  -- flag
decl
variable {k}  -- flag
decl
variable (k)  -- no flag
decl
variable {... k ...}

and the comments on the variable lines tell you the flags.

[Damiano Testa]

Riccardo Brasca said:

Independently of the linter #22396 is clearly an improvement. I've delegated it. Feel free to merge or wait if you want more time to test the linter.

Thanks! I'll merge, since there are several hundred exceptions still to test the linter!

[Bhavik Mehta]

Thanks for the clarification Damiano!

[Damiano Testa]

Essentially, if there is a pattern

variable (X)
declaration
variable {X}

the linter will flag the first variable. The linter ignores the binder types, just makes sure that there is a single variable in the two variable commands and that this variable is the same.

[Damiano Testa]

Since it seems that the suggestions of the linter are good, I'll automate the replacement. If all goes well, this could be a good test for an "auto-correcting linter" that runs in CI only, as the implementation is not robust for "live" actioning.

[Damiano Testa]

#22406 contains the automatic fixes to the warnings that the linter flagged.

[Damiano Testa]

These next PRs should contain the bulk of all the replacements:

[Damiano Testa]

#22412

[Damiano Testa]

#22413

[Damiano Testa]

#22414

[Damiano Testa]

Riccardo, thanks for the quick delegations! :thank_you:

[Damiano Testa]

#22423 with the (hopefully final!) adaptation PR.

[Damiano Testa]

The next issue is whether the linter should be merged or not.