Zulip Chat Archive
Stream: mathlib4
Topic: Poll: Indentation style for `to_additive` docstrings
Thomas Murrills (Aug 13 2025 at 18:51):
I'm currently normalizing the indentation for to_additive docstrings via automation in #28298.
There are two questions I'd like to ask here.
First: What overall indentation for multiline docstrings should be preferred?
(It's my understanding that docstrings should not be indented past their starting column as per this comment, so I'm not including that as an option here.)
A – Unindented
/-- Lorem ipprod dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipprod, nec luctus ex porta a. -/
@[to_additive
/-- Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipsum, nec luctus ex porta a. -/]
and
/-- Lorem ipprod dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipprod, nec luctus ex porta a. -/
@[to_additive /-- Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipsum, nec luctus ex porta a. -/]
B – Indented
/-- Lorem ipprod dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipprod, nec luctus ex porta a. -/
@[to_additive
/-- Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipsum, nec luctus ex porta a. -/]
and
/-- Lorem ipprod dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipprod, nec luctus ex porta a. -/
@[to_additive /-- Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipsum, nec luctus ex porta a. -/]
Thomas Murrills (Aug 13 2025 at 18:51):
/poll What overall indentation should be preferred for to_additive docstrings?
A – Unindented
B – Indented
A and B should both be equally preferred
Thomas Murrills (Aug 13 2025 at 18:57):
The second question:
Should we prefer newlines before docstrings, or prefer starting them inline with to_additive (or neither)?
Using A's unindented convention for example purposes:
a – Prefer newlines
/-- Lorem ipprod dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipprod, nec luctus ex porta a. -/
@[to_additive
/-- Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipsum, nec luctus ex porta a. -/]
b – Prefer inline
/-- Lorem ipprod dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipprod, nec luctus ex porta a. -/
@[to_additive /-- Lorem ipsum dolor sit amet, consectetur adipiscing elit. Nam at lacus molestie, fringilla
massa ut, auctor odio.
Integer aliquet felis ipsum, nec luctus ex porta a. -/]
Thomas Murrills (Aug 13 2025 at 18:58):
/poll Should we prefer to_additive doscstrings start on a newline or inline?
a – Prefer newline
b – Prefer inline
Both a and b are equally fine
Thomas Murrills (Aug 13 2025 at 19:37):
@Yaël Dillies Oops, I didn’t include the “multiline” qualifier in my second question, but maybe this is a good thing. I’ve added an option so that the options are comprehensive. :)
Eric Wieser (Aug 13 2025 at 19:39):
Another consideration is how to format
This
but I think this starts to correlate with earlier choices.
Thomas Murrills (Aug 13 2025 at 19:43):
Right, hypothetically we could make a choice that takes the delimiter into account (e.g. insist on a newline when /-- is alone and remain silent when not) but I wanted to steer clear of the "/--,-/ on their own lines" debate here and keep the number of total poll options in this thread from exploding. :grinning_face_with_smiling_eyes:
Thomas Murrills (Aug 26 2025 at 18:12):
It seems that of the people who have an opinion on this, we generally want
- unindented docstrings
- which start on a newline when (and only when) spanning multiple lines.
Shall we go with that? :)
Thomas Murrills (Aug 26 2025 at 18:13):
Again, this PR will not enforce these style choices in the future; it will just reformat docstrings to match them.
Thomas Murrills (Aug 26 2025 at 18:16):
Though, perhaps we should also consider writing this down somewhere as a style choice? (Unless, of course, there are objections from those who voted for the other options.)
Ruben Van de Velde (Aug 26 2025 at 20:44):
If you go around reformatting, it should be in the style guide - otherwise we'll reject it as style changes that aren't in the style guide, as discussed in the other thread :innocent:
Thomas Murrills (Aug 26 2025 at 20:45):
Makes sense! For the record, what other thread was that?
Ruben Van de Velde (Aug 26 2025 at 20:48):
Last updated: Dec 20 2025 at 21:32 UTC