Coding standards: line breaks

Stream: new members

[Patrick Stevens]

The documentation at https://leanprover-community.github.io/contribute/style.html says nothing about inserting blank lines in proofs; but mathlib seems to strongly prefer no blank lines, even in long proofs. Is this a formal requirement? It makes life harder in any editor that's paragraph-aware; I notice it because I use { and } very heavily in anything with vim bindings, and they are essentially useless in mathlib.

[Patrick Massot]

I don't think it's forbidden, but indeed it's not used much

[Reid Barton]

Don't "paragraph-aware" editors then become "proof-aware"?

[Reid Barton]

I don't really understand the difficulty (also, vim for lean??)

[Reid Barton]

Oh, "vim bindings", okay.

[Reid Barton]

The question seems a bit https://xkcd.com/1172/

[Patrick Stevens]

Sure, I'm not trying to warp the coding conventions just to make Vim work - if I were, I would mandate that lemmas look like this, so that [[ and ]] would work:

lemma foo () : nat :=
begin
{
}
end

[Reid Barton]

I think I've tried to put newlines in the middle of long proofs before, and someone told me to delete them, but it was long ago.

[Patrick Stevens]

Yeah, that happened to me a couple of days ago

[Patrick Stevens]

I can get around it by dropping marks all over the place or by doing a rough count of the number of lines I want to move when I incant a motion, it's just a bit more annoying than it could be

[Reid Barton]

I think the root cause is maybe not the lack of newlines in long proofs :upside_down:

[Patrick Stevens]

Aside from anything else, I am inclined to argue that newlines help readability a lot

[Patrick Stevens]

But if the will of the senate is no newlines, then I'll just get rid of them all in a linting pass pre commit, it's hardly the end of the world

[Reid Barton]

If you want to break up a proof with a newline for readability, it's probably even better to put a comment on that line.

[Reid Barton]

Long proofs should usually be structured with { }, at least.