calc indentation: style guide?

Stream: mathlib4

[Yury G. Kudryashov]

I see different styles of indentation with calc in the library. Should we have a style guide or allow all of them?

-- as a closing tactic-1
calc
  first_term ≤ mid_term := by
    sorry
  _ = last_term := _

-- as a closing tactic-2
calc first_term
  ≤ mid_term := by
      sorry
  = last_term := _

-- to prove a `have`
have H : a = b :=
  -- newline, then one of 2 styles above

-- to prove a `have`
have H : a = b := calc
  a = c := _
  _ = b := _

[Sébastien Gouëzel]

Another one:

  calc
    a long first term
    _ ≤ middle term := by
      sorry
    _ ≤ last term := by
      sorry

[Yaël Dillies]

I personally prefer

have : a = b :=
  calc
    _ = c := _
    _ = _ := _

[Yury G. Kudryashov]

This way a reader can't see the first term

[Yaël Dillies]

Yeah but that's fine because it's usually in the statement

[Yury G. Kudryashov]

Not if you had some simps, rws or applys before.

[Yaël Dillies]

Emphasis on "usually"

[Yury G. Kudryashov]

Then please fix your example to include surrounding code that contains the first and the last terms.

[Emilie (Shad Amethyst)]

You could always have a show a = b before the calc

[Richard Osborn]

Your second example is missing an _ before the =.
I personally don't like the first term being omitted as it should never increase the number of lines nor ruin the formatting if it is written next to calc. If calc first_term is longer than a single line, there may be other problems with the proof. To keep formatting as consistent as possible the following seems like the most robust and readable.

calc first_term
  _ ≤ mid_term := by
      sorry
  _ = last_term := _

[Geoffrey Irving]

^ I also like first_term on the calc line, FWIW. It’s uniform, since then each change corresponds to a further line.

[Ruben Van de Velde]

It depends on the length of the expressions for me - putting the first expression on a separate line makes it much easier to pick out the structure than if you have to scan for a symbol somewhere in the middle of a long line

[Jireh Loreaux]

I disagree about putting the first expression on the calc line. Indeed, the calc keyword will often appear at the end of the preceding line. In such situations it would be weird if the first expression were on that line.

[Eric Wieser]

I think that only happens in the case when Yael's suggestion above can take over, and _ on the first line is fine