Bikeshedding: newlines around headers, universe, variables

Stream: mathlib4

[Fernando Chu]

Thanks for doing this! I'm glad I'm not the only one that was slightly uncomfortable with the lack of a convention :)

Here are some more bikesheds I've noticed, if you (or anyone) would like to fix:

1. Spacing in the introduction of the files. I.e. we have a sequence 1. the copyright 2. the imports, 3. the docstring, 4. the end of docstring -/ marker, and 5. the lean code. Some files put a space (or more!) in between some of these steps, some don't, etc.
2. Should the title for the introduction docstring be /-! # Title or /-! \n # Title? Similarly for titles of sections.
3. Should one line docstrings be closed in the same line, or in the next one? (I've been told it should be in the same line, but there are plenty that don't do this, and I don't see this in the guidelines)
4. Some docstrings/comments just end a line and continue to the next line despite not being close to the line character limit, e.g. this
5. No convention of break lines in between universe/variable and namespace/section declarations. (My own preference is that there should be no line breaks in between universe and variable, and a line break between every other pair)

[Michael Rothgang]

(3) has been discussed in a different thread: as I understand it, there's some consensus, but there are (at least) 2500 doc-strings to fix. So that will only happen with some automated help.

[Michael Rothgang]

Let me move this to a different thread: trying to keep the bikeshedding somewhat searchable.

[Notification Bot]

3 messages were moved here from #mathlib4 > Style :bicycle: : indenting second lines in doc-strings by Michael Rothgang.

[Michael Rothgang]

Re (4): some doc-strings in mathlib use semantic line breaks (I believe), but these are a great minority.
If you see a doc-string which fits (4) but is not a semantic line break, feel free to make a PR. (I don't think these are very high priority, though. I'm making the doc-string changes because I have a linter written which can enforce them.)