Linting standards for mathlib

Stream: mathlib4

[Thomas Murrills]

A couple of questions about how happy we should make the linter:

1. Should comments and docstrings both stick to the ≤ 100 character line limit? I'd imagine that we wouldn't want odd newlines appearing suddenly in docstrings (but rather let the dosctring-viewer handle word wrapping itself, since it'll likely display it in a proportional font, which can make newlines after 100 characters seem out of place), but I'm not sure.

[Jireh Loreaux]

No, everything is cut to 100 chars; this is the same as in mathlib3. The docstrings are formatted by doc-gen4, so it's not really an issue.

[Thomas Murrills]

2. I have a lot of definitions that only are to be used within the file. Should these also have a docstring to make the linter happy? Or should they be marked private or something like that?

[Jireh Loreaux]

As for the linter, you should make it perfectly happy always (* technically there are certain circumstances where it's okay to add a nolint attribute, but those are comparatively rare).

[Mario Carneiro]

(there is one exception to the line length limit, which is lines that contain a URL; those usually can't be line-broken and are excluded by the style linter)

[Thomas Murrills]

There's some special context here: I'm basing my current work off of an existing file in Lean/Elab, which doesn't have docstrings nor private declarations for most definitions. Also I've noticed several comments and docstrings (none of which contain a URL) in the source file that are > 100 characters. Should those be changed?

[Mario Carneiro]

Leo has a giant monitor and does not observe the 100 character line length convention

[Jireh Loreaux]

I don't think Lean 4 core has the same linting restrictions as Mathlib.

[Thomas Murrills]

Hmmm. Should I make sure my additions are lint-free and then somehow turn off the linter on this particular file, since it's a minimally-invasive modification of StructInst.leanin lean 4 core? Or should I wrangle its original contents into conformity?

[Thomas Murrills]

And, as part of this: how should I handle the missing docstrings on 95% of the function's existing definitions (which aren't used outside the file)?

[Mario Carneiro]

everything should be lint-free

[Mario Carneiro]

If it's intended as a modification to StructInst.lean then it should be a PR to core and then the linters don't matter

[Scott Morrison]

Although note that some changes (not sure here!) that could go in core, should not, for sake of not using up core developer's bandwidth. mathlib4 is happy to take things in the meantime, but in that case wants complete lint compliance. :-)

[Thomas Murrills]

Ok! But, if we put it in mathlib in the meantime, with an eye towards putting it in core eventually...does that mean attaching a docstring to every function in this file without one (about 101 declarations), even though they're just used within the file and nowhere else?

Which, I mean, I guess I could—I understand it well enough by now! 😅 I just wonder if my mathlib-contribution time could be put to better use. (Or should I maybe attach an empty/copy-pasted docstring?)

[Yaël Dillies]

Only definitions need docstrings.

[Thomas Murrills]

Yes, but #lint tells me there are 101 of those in this file. :upside_down:

[Thomas Murrills]

This file just defines a term elaborator, so all of its definitions only really go towards that. So if there's a way I can private them all or something...not sure if that would fix it anyway, though.

[Yaël Dillies]

Then you're in for a rough time :upside_down:

[Scott Morrison]

Hmm... I'm inclined to say it's still valuable, since of course core should have the doc-strings too. :-) But I hear your pain.

[Scott Morrison]

Adding all those doc-strings might be a nice present to go along with the core PR. :-)

[Jireh Loreaux]

Yeah. Core could always use more doc strings.

[Thomas Murrills]

Ok, I'll give the docstrings a shot! :)

[Thomas Murrills]

Alright! Docstrings written, linting (and build) passed! :smiling_face: Still a couple design choices that can be made/tweaked/confirmed and some comment cleanup once that's done, but it's up and running! :)