Zulip Chat Archive

Stream: PR reviews

Topic: Style guide


view this post on Zulip Sebastien Gouezel (Jan 03 2021 at 11:42):

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!

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 11:50):

Thanks for this! Looks great to me.

view this post on Zulip Patrick Massot (Jan 03 2021 at 11:57):

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

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 11:58):

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!

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 12:06):

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

view this post on Zulip Floris van Doorn (Jan 03 2021 at 23:00):

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.

view this post on Zulip Kevin Buzzard (Jan 03 2021 at 23:01):

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

view this post on Zulip Eric Wieser (Jan 03 2021 at 23:05):

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

view this post on Zulip Alex J. Best (Jan 03 2021 at 23:20):

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)

view this post on Zulip Floris van Doorn (Jan 04 2021 at 01:46):

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.

view this post on Zulip Mario Carneiro (Jan 04 2021 at 03:00):

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.

view this post on Zulip Mario Carneiro (Jan 04 2021 at 03:03):

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

view this post on Zulip Mario Carneiro (Jan 04 2021 at 03:03):

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

view this post on Zulip Yury G. Kudryashov (Jan 04 2021 at 06:06):

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

view this post on Zulip Sebastien Gouezel (Jan 04 2021 at 07:42):

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!


Last updated: May 06 2021 at 11:23 UTC