style guide for comments?

Stream: lean4

[Kim Morrison]

I think the consensus is:

/-- Doc-comments that fit on one line are great! -/
/--
And when they require
multiple
lines, the delimiters should go on their own line, but variation is permitted here.

No indentation is required in block comments.
-/
-- All comments, single line or otherwise, have a space after the `--`, `/-` or `/--`, and a space before the `-/`.
-- Comments should have appropriate punctuation.
-- They don't need to be complete sentences, but can be. (This previously said they should be!)
/-- We prefer the indicative mood over the imperative, because it tends to be more robust to appearing in difference locations (hovers, embedded in manuals, etc). -/
/- Comments should always come *before* the thing they are talking about, never after. -/

Or at least, I remember David being surprised that everyone in the FRO happily agreed that this was consensus. :-)

Is that is this case --- is this documented somewhere? If not, let's!

[Rida Hamadani]

In fact, the doc style guide contains examples which seem to imply that delimiters shouldn't go on their own lines in the second case.

[Kim Morrison]

Indeed! I hope we can change that. :-)

[Rida Hamadani]

#475

[Kim Morrison]

Looks great to me, but let's leave 24 hours in case bikeshedding is required here. :-)

[Thomas Murrills]

Kim Morrison said:

-- Comments should typically be complete sentences, with punctuation.

Should this maybe be broadened to something like “or complete grammatical phrases” (also with punctuation)? The style guide has this example, which is not a complete sentence but looks ok to me (or at least, there are docstrings of the same form which look ok):

/-- The brackets corresponding to a given `BinderInfo`. -/
def brackets : …

Plus, docstrings on functions of the form “Does x” seem ok; there’s an imperative-mood docstring in the style guide which would still look ok to me if indicative (“Finds”/“replaces”instead of “Find”/“replace”), but might be unnecessarily cluttered if prefixed with “mapPrefix finds…” or “This function finds…”

/-- Find the largest prefix `n` of a `Name` such that `f n != none`, then replace this prefix
with the value of `f n`. -/
def mapPrefix : …

But, there could be an argument/preference for insisting on complete sentences here.

[Kim Morrison]

Yeah, I agree that complete sentences is asking too much.

[Utensil Song]

Could there be examples for inductive mood v.s. imperative?

[Kim Morrison]

Do you mean here, or in the style guide?

[Utensil Song]

I mean in the style guide.

[Damiano Testa]

Some of the constraints about doc-strings could be enforced by a syntax linter: would that be desirable?

I think that regular comments (i.e. non-doc-strings) are (almost) completely invisible to lean linters.

[Yaël Dillies]

Personally I don't think delimiters should go on their own lines. That's just wasted space in the editor

[Michael Rothgang]

Thanks for initiating this discussion!

Re: /-- The brackets corresponding to a given `BinderInfo`. -/,
I actually prefer omitting a full stop here: to me, this is not a complete sentence, hence should not get a full stop. (I do not care a lot, so would not personally rewrite lots of docstrings to match my style - but I would prefer changing the style guide accordingly.)

[Utensil Song]

Maybe

- Comments should have appropriate punctuation.
- They don't need to be complete sentences, but can be. (This previously said they should be!)
+ Comments should be complete sentences with appropriate punctuation, or complete grammatical phrases with optional punctuation.

[Utensil Song]

And maybe

- lines, the delimiters should go on their own line, but variation is permitted here.
+ lines, the delimiters could go on their own line, or be on the same lines of comments, as long as the same style is used in a file consistently.

[Eric Wieser]

Yaël Dillies said:

Personally I don't think delimiters should go on their own lines. That's just wasted space in the editor

Without this rule we end up with a lot of

/-- this is
    a long message that I decided to indent -/

which leads to confusion about whether comments should be indented

[Yaël Dillies]

Why don't we just disallow indenting?

[Jovan Gerbscheid]

I was using the imperative mood quite a bit, not knowing the consensus, so documenting this would be helpful.

[Richard Osborn]

For multiline comments, the rule could be to put /-- is on its own line, but -/ does not have to be. If there are multiple paragraphs, I think putting -/ on its own line would then be preferred.

[Johan Commelin]

I am in favour of Yaël Dillies's proposal: delimiters at the start/end of a line, no indenting.

Even though large screens are getting cheaper, I still think putting delimiters on their own lines is somewhat wasting vertical screen real estate.

[Kim Morrison]

I would be strongly opposed to a rule that says you can't put delimiters on their own line. (Note the FRO's internal style guide now says they must be on their own lines!)

But I guess I can compromise with either variant being allowed. :-)

[Johan Commelin]

Yeah, I didn't mean to forbid the other options. I just meant to indicate what my preferred style is.

[Mario Carneiro]

I'd prefer consensus on this in mathlib. I've already been imposing this style on Batteries based on what I perceived the most common style to be: single line comments are fine, otherwise comment delimiters are on their own line with no indentation. By the way another aspect that might tilt the preference here: using -/ on the same line as the markdown ``` at the end of a markdown code snippet causes highlighting to break:

/-- This is a nifty lean function:
```
def nifty := Nat.succ
``` -/
def nifty := Nat.zero

[Jireh Loreaux]

I would also prefer consensus. In the past, I've found myself doing both. Personally, I'd just as soon stick with the FRO on this for uniformity, even at the cost of a bit of vertical space.

[Eric Wieser]

Mario Carneiro said:

I've already been imposing this style on Batteries based on what I perceived the most common style to be: single line comments are fine, otherwise comment delimiters are on their own line with no indentation.

I slightly prefer @Richard Osborn's rule of "delimiters on own line if there are paragraphs", with the reading that a code block or double blank line is always a new paragraph.

[James Gallicchio]

Lean is also already far denser than most programming languages in terms of info per line. There's very little boilerplate (good), but the high density can make it hard for me to read sometimes. So I'm in favor of all style preferences that add some whitespace, including putting /-- on its own line :-)

[Matthew Ballard]

I like gofmt

[Joachim Breitner]

Though on mathlib I expect people will want golfmt. (SCNR)

[Kim Morrison]

/-- and -/ on their own lines also seems much easier for tools to get right by themselves. Having them inline with the comments seems likely to require aesthetic judgement calls. :-)

[Thomas Murrills]

“Delimiters on their own lines iff the docstring contains paragraphs” seems tool-enforceable! :)

A different option is “Delimiters on their own lines iff the body takes up >2 lines”. I feel like a two-line docstring with delimiters inline is ok, but a three-line one starts getting dense.

(Plus, putting delimiters on their own line doubles the line count in the 2-line body case, which contributes to the awkward feeling, I think, but only increases it by 2/3 in the 3-line case…)

[Thomas Murrills]

(This of course trivially avoids the markdown code block issue, as you need at least 3 lines for a code block.)

[François G. Dorais]

Thomas Murrills said:

“Delimiters on their own lines iff the docstring contains paragraphs” seems tool-enforceable! :)

Unless said tool is expected to have basic understanding of markdown.

[François G. Dorais]

I would further add that single line comments should not use markdown other than *..* and **..**. TeX math should be limited too but we shouldn't expect a tool to actually enforce anything in there.

[Eric Wieser]

Allowing only bold and italic seems pretty arbitrary to me. Surely /-- `foo x y` foos `x` with `y` -/ is fine? What inline markdown syntax are you trying to forbid?

[François G. Dorais]

Sorry, an incomplete thought was partly expressed :/ I did not mean to exclude inline code.

The problem is: what's a paragraph? That becomes murky if you expect the tool to understand markdown. Then again you don't want the tool to ignore markdown altogether. So markdown's definition of paragraph can't be used but markdown can't be ignored.

I think this is a case where someone needs to write the tool to do the right thing and then let people struggle to explain what it actually does...

[Thomas Murrills]

Isn’t “contains a paragraph” just “contains "\n\n" or "\n```"”? How does markdown enter into it?

[Thomas Murrills]

Hmm, I suppose you’ve got to account for bullets too…but beyond that, are there other markdown paragraph sources?

I’m starting to see how markdown could have the potential to be an issue (at least on the implementation side) if we used a paragraph definition, though…I suppose it would depend on how easy it really is to check for paragraphs.

[Jireh Loreaux]

I really think it makes more sense to go with the simplest approach: multiline comments get the delimiters on their own lines.

[Jireh Loreaux]

At the very least, it's easier to remember and explain.

[Jon Eugster]

I agree, either #lines > 2 or #lines > 1 seems like a very simple rule and seems completely sufficient. I kinda liked the former one for exactly the reasons Thomas mentioned.

[Kyle Miller]

In principle I agree with "multiple lines, use /-- and -/ on their own line." But, with structure fields, I'm still tempted to allow that one line to be flowed across multiple lines, like here.

Maybe an easy-to-explain rule is "/-- and -/ don't have to go on their own line if the comment has just been reflowed to meet the 100 character line rule"? This probably should only be allowed for two to maybe three lines.

[Patrick Massot]

I am amazed by Kyle’s negotiation skills in this “I agree with this idea that only single line comments should have delimiters on the same line, but what about single line comments that span multiple lines?”.

[Patrick Massot]

And I also agree that the structure field example that he cited would look worse with delimiters on their own lines.

[Mario Carneiro]

I've also been using same-line /-- for structure fields and inductive constructors, although both positions seem defensible here

[Antoine Chambert-Loir]

Is it the place to advocate for the use of semantic line breaks in comments?

[Johan Commelin]

It's always the right place to advocate for that.

[François G. Dorais]

I now even more strongly believe in the last part of my earlier comment:

I think this is a case where someone needs to write the tool to do the right thing and then let people struggle to explain what it actually does...

I think there is much stronger agreement on what is actually right than explaining and defining what is right. Let's write a draft tool and then quibble on the very rare edge cases.

[Michael Rothgang]

François G. Dorais said:

I now even more strongly believe in the last part of my earlier comment:

I think this is a case where someone needs to write the tool to do the right thing and then let people struggle to explain what it actually does...

I think there is much stronger agreement on what is actually right than explaining and defining what is right. Let's write a draft tool and then quibble on the very rare edge cases.

If the tool is reasonable, I'd be very happy to just agree on "whatever that tool does" (modulo bugs).

[Michael Rothgang]

Just like a code formatter can alleviate many formatting discussions.