docBlame

Stream: mathlib4

[Reid Barton]

Can we tone down the docBlame linter a bit? It's pretty silly to document notation, for instance

[Reid Barton]

In particular local notation

[Mario Carneiro]

You should generally be using @[inherit_doc] on all notations, it's a bit rote right now

[Reid Barton]

I'm also skeptical of the value of documenting fields of structures. I see it makes sense in a programming context (where fields tend to have some meanings which cannot be determined from their names and types alone) but in a math context this rarely happens, especially when the fields are Prop-valued.

[Reid Barton]

It seems like we are enforcing the equivalent of

  // add 1 to i
  i++;

-style comments

[Reid Barton]

(Plus, during the port is the wrong time to add such comments)

[Mario Carneiro]

Regarding the last point, we still have nolints.json if you want to leave the documentation to someone else

[Mario Carneiro]

I'm generally skeptical of the claim that there are any statements that don't benefit from being written in english. Personally I would have the doc requirements much higher than they are currently are, basically one on every theorem, but I think that's too much to ask at this point.

[Mario Carneiro]

Even if occasionally you cheat and put some "add 1 to i" style comment some times, the overall effect on the library of passive "write anything at all, please" doc requirements is really massive

[Reid Barton]

To be clear, I think the documentation requirements are actively bad because they encourage poor documentation which tends to displace good documentation

[Mario Carneiro]

I don't think that not having doc requirements would somehow cause good docs to be written

[Mario Carneiro]

who's going to write those?

[Mario Carneiro]

Replacing bad docs with good are of course something we will accept

[Mario Carneiro]

so I don't think anyone's hand is being forced here

[Reid Barton]

If there is something nonobvious about a structure definition for example, it should usually be documented at the scope of the structure as a whole

[Mario Carneiro]

Okay, so do that

[Mario Carneiro]

the doc requirements on structure fields doesn't prevent you from writing that comment

[Reid Barton]

but then if you also have to document the fields individually, it is just 2x the noise to wade through

[Reid Barton]

Conversely, not requiring documentation on each field doesn't prevent you from taking that approach when it is appropriate (which it surely is sometimes)

[Mario Carneiro]

you can give the fields minimal comments if the doc on the structure is expansive, I think

[Mario Carneiro]

but this is not at all the problem we have in the library currently

[Mario Carneiro]

too much docs is a problem I wish we had

[Mario Carneiro]

but we are battling "way too few docs" here

[Reid Barton]

I would just use @[nolint docBlame], anything else is too much fuss.

[Mario Carneiro]

I think nolint docBlame is basically never appropriate, at least in the situation you have outlined

[Reid Barton]

In that case, I would never add a structure to mathlib.

[Mario Carneiro]

a nolint in the nolints file is fine, that's basically saying "someone else do it, I can't be bothered"

[Mario Carneiro]

but nolint docBlame means "this field should not be documented" and that's just a bizarre thing to say

[Mario Carneiro]

if you find yourself in this situation I would encourage you to use nolints.json instead of @[nolint]

[Eric Wieser]

Only data fields need documentation, right?

[Yaël Dillies]

Not currently, because all fields are defs.

[Yaël Dillies]

Mario Carneiro said:

who's going to write those?

I do bust doc blame nolints from time to time.

[Eric Wieser]

but nolint docBlame means "this field should not be documented" and that's just a bizarre thing to say

I take it to mean "a conscious choice was made not to document it"

[Eric Wieser]

To me, the nolints file is for new linters that were added without fixing all their findings, as this means we can start stopping new mistakes in PRs without fixing them everywhere else in HEAD first

[Mario Carneiro]

Eric Wieser said:

To me, the nolints file is for new linters that were added without fixing all their findings

In a sense, the new doc requirement on structure fields is that, since it immediately creates a huge number of violations in mathlib that will take time to work off

[Mario Carneiro]

it's making an existing lint stricter rather than adding a new lint but it works out basically the same

[Eric Wieser]

but nolint docBlame means "this field should not be documented" and that's just a bizarre thing to say

I think then we agree on the first half of this sentence modulo phrasing but disagree on the second

[Mario Carneiro]

To put it another way, a nolints.json entry is a TODO, while a @[nolint] attribute is a not-a-bug/wont-fix annotation

[Mario Carneiro]

if we want to use @[nolint] to mean "I decided not to do it but someone else might want to consider doing it" then we need another syntax to indicate "this is intentional, talk to someone before you try to 'fix' this"

[Eric Wieser]

"talk to someone before you try to 'fix' this" sounds the same as "won't-fix" to me

[Mario Carneiro]

that's what I mean

[Mario Carneiro]

to me @[nolint] means wontfix

[Mario Carneiro]

and using @[nolint docBlame] for something other than wontfix seems misleading

[Mario Carneiro]

and wontfix on documentation is nonsensical, hence why I say @[nolint docBlame] should never be used

[Johan Commelin]

The docBlame linter is complaining at

feat: port/RingTheory.Localization.Basic !4#2741

I thought we told it to not do that....

[Matthew Ballard]

It didn’t listen. I use inherit_doc for the fields now.

[Eric Wieser]

Yaël Dillies said:

Not currently, because all fields are defs.

I've filed std4#217 for ignoring defs that should be theorems. Is there a lean4 issue about the fact they are not theorems in the first place?

[Eric Wieser]

https://github.com/leanprover/std4/pull/269 tells Std not to lint proof fields of structures for docstrings