indentation, by

Stream: mathlib4

[Yury G. Kudryashov]

Which style is preferred now?

lemma blabla := by
  foo

or

lemma blabla :=
  by
  foo

?

[Heather Macbeth]

I believe the former, so for long declarations

lemma blablabl (h1 : a = 3)
    (extra_long_hypothesis_takes_a_lot_of_space : 3 = 4) :
    goal_is_also_long := by
  exact my_proof

[Heather Macbeth]

(4 space indent for subsequent lines of statement, by on same line as goal, 2 space indent for proof)

[Yury G. Kudryashov]

I asked because mathport sometimes generates the second style.

[Heather Macbeth]

My impression is that it does this sometimes when there's an error in the proof it generated and it got confused about what syntax is what.

[Ruben Van de Velde]

Oh, is that if? I'd been wondering why it happened too

[Mario Carneiro]

This behavior of mathport is a bug. I don't think it has to do with errors in the proof (because mathport never actually tries to elaborate the expression), there is just some combination of indentation and context that is causing this behavior in the formatter. It would be great if someone could make a MWE; you can usually demonstrate these things without even using mathport because the formatter is in core

[Mario Carneiro]

As a general rule, don't take the output of mathport as gospel regarding the style guide. It gets pretty close, but it's still lacking a lot of features relative to a real source code formatter - it was originally only intended for pretty printing, so if it does something odd consider that it might be a bug and don't copy the bug into your own style!

[Moritz Firsching]

see also mathlib4#1525 mathlib4#1523 and mathlib#1529

[Moritz Firsching]

Fix files during port with

awk -i inplace '{do {{if (match($0, "^  by$") && length(p) < 98 && (!(match(p, "^[ \t]*--.*$")))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}' ./Mathlib/File/Im/Porting.lean