missing docs

Stream: mathlib4

[Damiano Testa]

I have a vague idea that doc-string for declarations can now only be added in the module where the declaration is defined.

[Damiano Testa]

If that is so, a syntax linter could warn about missing docs reliably: would that be desirable?

[Michael Rothgang]

I would find that valuable, but perhaps I'm biased :-)

[Damiano Testa]

It is still good to hear the opinion of one of the house linters... :smile:

[Kim Morrison]

It think it's important not to make it too annoying -- lots of people like to write their module docs as a final step.

[Damiano Testa]

Right and, if you have to trigger it manually, you might as well use #lint. So, not a clear win for the syntax linter...

[Damiano Testa]

There might still be value in getting a CI warning early, rather than having to wait for everything until the lint step to find out that you missed a doc-string.

[Damiano Testa]

So maybe just adding it to CI as an earlier step, since CI is going to fail anyway if you do not have docs, but at least you know earlier.

[Eric Wieser]

Damiano Testa said:

There might still be value in getting a CI warning early, rather than having to wait for everything until the lint step to find out that you missed a doc-string.

I'm not so sure, I think being encouraged to write the docstring sometime after getting everything building is a feature

[Eric Wieser]

In that you end up coming back in a separate session, perhaps with a clearer big picture

[Damiano Testa]

Ok, I was just in the situation where I had written the docs to a structure, explaining also what the fields meant and I got a lint error for not writing the docs of each field separately. I realize that this is a fairly special case! :smile:

[Michael Rothgang]

I have had several occasions where I thought my PR was all set, to have CI fail linting with a missing docs warning on some side definition. I found that disruptive and not particularly helpful. Returning to a PR with a fresh set of eyes is useful - but do we need to impose it in this way?

[Kim Morrison]

Yes, I agree there's tension here!

[Eric Wieser]

My comment above was primarily about module docstrings, where the fresh set of eyes is probably more valuable than on individual definitions

[Eric Wieser]

Damiano Testa said:

If that is so, a syntax linter could warn about missing docs reliably: would that be desirable?

Doesn't this already exist as linter.missingDocs, and Batteries uses it?

[Damiano Testa]

Oh, for module-docs, that linter is already in mathlib...

[Damiano Testa]

About #lint: I was exactly wondering if adding something that would be automatically on, rather than calling it explicitly was useful. I know of #lint and I only sometimes remember about it before sending a PR to CI.

[Damiano Testa]

It is a rather niche use, I am not too invested in it and am happy to leave things the way they are now.

[Damiano Testa]

Besides, I think that linters should have as close to unanimous support as possible, since they can be very intrusive: they should only flag issues that everyone feels strongly in favour of!

[Eric Wieser]

So this thread is really asking "Should we add (`linter.missingDocs, true) to the mathlib lakefile?"?

[Damiano Testa]

Yes, it looks like it! :smile: I also think that the discussion answered that question.

[Eric Wieser]

One downside in such a strategy is that I think linter.missingDocs does not permit nolints

[Eric Wieser]

So I doubt you can just turn it on and have the build succeed