Style guide

Stream: PR reviews

[Sebastien Gouezel]

I have opened a PR to actualize the style guide at https://github.com/leanprover-community/leanprover-community.github.io/pull/155. I won't merge it myself because I am not sure everyone has the same feeling on our current style as I do. Comments/improvements welcome!

[Kevin Buzzard]

Thanks for this! Looks great to me.

[Patrick Massot]

I love that you are now reviewing your own PRs. Who needs AI or other maintainers?

[Kevin Buzzard]

I sometimes review my own PR's when I'm glancing over them and notice a slip -- I make a suggestion and then commit it!

[Kevin Buzzard]

oh lol I just looked and it's exactly what he was doing too :-)

[Floris van Doorn]

Do we want the "single tactic per line, unless 1 line closes the whole goal" style convention?
I myself have basically been doing "anything goes, as long as there are at most 100 characters per line". I feel that there are many combinations of tactics that feel like "1 step" that I like to put on one line, examples:

begin
  ...
  dsimp, simp
end

  ...
  rw [foo], simp_rw [bar],
  ...

  ...
  apply foo, intros x y,
  ...

  ...
  rcases x with ..., rcases y with ...,
  ...

  ...
  apply foo, apply bar,
  ...

I also put many other tactics on 1 line (that often aren't really a single step). For example, here is a snippet from haar_measure.lean:

  apply nat.Inf_le, refine ⟨_, _, rfl⟩, rw [mem_set_of_eq], refine subset.trans h1s _,
  apply bUnion_subset, intros g₁ hg₁, rw preimage_subset_iff, intros g₂ hg₂,

Is the proof more readable if that is 8 lines?

I prefer allowing any number of tactics on one line.

[Kevin Buzzard]

Fighting talk! I completely agree that "one line" can sometimes be very different to "one mathematical idea".

[Eric Wieser]

Arguably you should indicate "one mathematical idea" with a lemma / tactic / comment which contains the name of that idea, but that's perhaps not pragmatic

[Alex J. Best]

I think "1 step" examples should be allowed on one line like dsimp, simp or rw [foo], simp_rw [bar] , but would prefer multiple lines for your last example. I do believe it is a lot more readable if I can step through a proof using the down key, rather than having to move to the next comma manually.
Its also easier to rearrange and fix / modify proofs when you don't have too much happening on one line, at least with most IDEs or text editors, cutting and pasting whole lines are common operations and have easily accessible shortcuts.
I also don't really see what compressing proofs too much helps with when the proof is already long (small golfs to indicate that a lemma is a triviality is ok, but in the haar measure stuff you're really proving things that people may want to read for some reason)

[Floris van Doorn]

Ok, it seems I'm outvoted, and I'm happy to adapt.

Then I suggest adding something like "Multiple tactics are allowed on one line, if they feel like 1 step" with some examples.

[Mario Carneiro]

I routinely use complex lines, and I think many very short lines is a readability issue because you can't see as much of the proof at once. As you've identified, I try to keep it to one "mathematical idea", but this is admittedly vague and I'm not sure we can or should do anything about this.

[Mario Carneiro]

I agree that the "down arrow sequence" should give you a sensible sequence of proof steps. I sometimes deliberately do things like cases bla, clear h because I don't want people to have to look at the intermediate point. That also makes sense with the "one mathematical idea" definition

[Mario Carneiro]

I'm sure that an automated formatter will hate us for this though

[Yury G. Kudryashov]

I often do induction n, { simp }, to discharge the case n = 0 without using two { ... } blocks.

[Sebastien Gouezel]

I have added to the PR a comment that tactics corresponding to a single idea, like cases bla, clear h or induction n, { simp } or rw [foo], simp_rw [bar] can be put on a single line. Don't hesitate to push more changes!