Zulip Chat Archive

Stream: new members

Topic: Coding standards: line breaks


view this post on Zulip Patrick Stevens (May 17 2020 at 11:34):

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.

view this post on Zulip Patrick Massot (May 17 2020 at 11:34):

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

view this post on Zulip Reid Barton (May 17 2020 at 11:37):

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

view this post on Zulip Reid Barton (May 17 2020 at 11:38):

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

view this post on Zulip Reid Barton (May 17 2020 at 11:38):

Oh, "vim bindings", okay.

view this post on Zulip Reid Barton (May 17 2020 at 11:39):

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

view this post on Zulip Patrick Stevens (May 17 2020 at 11:45):

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

view this post on Zulip Reid Barton (May 17 2020 at 11:45):

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.

view this post on Zulip Patrick Stevens (May 17 2020 at 11:45):

Yeah, that happened to me a couple of days ago

view this post on Zulip Patrick Stevens (May 17 2020 at 11:46):

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

view this post on Zulip Reid Barton (May 17 2020 at 11:46):

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

view this post on Zulip Patrick Stevens (May 17 2020 at 11:47):

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

view this post on Zulip Patrick Stevens (May 17 2020 at 11:47):

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

view this post on Zulip Reid Barton (May 17 2020 at 11:48):

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.

view this post on Zulip Reid Barton (May 17 2020 at 11:58):

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


Last updated: May 13 2021 at 21:12 UTC