Endless docstring warnings after updating to mathlib >4.12.0

Stream: mathlib4

[Geoffrey Irving]

I've updated some repos to recent mathlib and lean, and now I get a ton of warnings about missing docstrings in mathlib when building my repo. How can I fix this? For example, here's the output of lake build if nothing needs to be built at all, in either mathlib or my own code, for https://github.com/girving/interval:

julia:interval% lake build 2>&1 | wc
    8639  182020 1376992

julia:interval% lake build 2>&1 | tail -n 30
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean:66:8: `Real.deriv_log'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [1827/1850] Replayed Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean:82:8: `Complex.deriv_cos'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean:512:8: `Real.deriv_cos'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [1830/1850] Replayed Mathlib.Analysis.Convex.SpecificFunctions.Deriv
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean:123:8: `deriv_sqrt_mul_log'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [1832/1850] Replayed Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean:130:8: `Complex.tan_add'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean:231:8: `Real.tan_eq_zero_iff'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [1833/1850] Replayed Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean:38:8: `Real.tan_add'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [1835/1850] Replayed Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
warning: ././.lake/packages/mathlib/././Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean:78:8: `Real.hasDerivAt_arctan'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
Build completed successfully.

[Damiano Testa]

Did you use lake exe cache get to download mathlib's cache?

[Geoffrey Irving]

No, I haven't been able to do that for months because there is an ABI bug which causes lean to crash unless I build mathlib myself.

[Geoffrey Irving]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Crashing.20bug.2C.20possibly.20related.20to.20UInt64.20arithmetic/near/474354843

[Damiano Testa]

I think that you would not see the warnings if you had mathlib's cache. If you are building mathlib anyway, you can then make the linter silent, by building with the docPrime linter option false.

[Damiano Testa]

I'm not at a computer, though, and I don't remember what it is exactly.

[Geoffrey Irving]

To clarify, do I need to modify .lake/packages/mathlib to do that? I'd prefer to avoid having to set options inside the .lake directory.

[Geoffrey Irving]

If there's a way to do it that modifies only my own lakefile.lean that would be excellent; I've tried to set the mentioned option but am unsure how.

[Eric Wieser]

I would guess this relates to the nolints file, and this not being accessible except when building the initial cache?

[Eric Wieser]

(which is to say, this sounds like a bug)

[Ruben Van de Velde]

By the way, if you go-to-definition into mathlib from a dependent project, vs code also flags those as warnings

[Eric Wieser]

Maybe the actual issue here is that lake build should not show warnings from dependent projects unless you ask it to, cc @Mac Malone

[Eric Wieser]

It's great to see all the warnigns in dependent files, but if it's someone else's project they're just noise that drowns out the local issues in your own project

[Damiano Testa]

Eric Wieser said:

I would guess this relates to the nolints file, and this not being accessible except when building the initial cache?

Ah, I did make the linter look for exceptions assuming that the file would be in scripts/... and did not think of pre-pending the appropriate path!

[Eric Wieser]

I think you should probably be using the mechanism that proofwidgets uses to load javascript files

[Eric Wieser]

Though I guess the downside is that adding a nolint causes all of mathlib to rebuild

[Damiano Testa]

So, maybe another solution would be to copy the nolint file into the location expected by the linter.

[Damiano Testa]

(Until I fix this.)

[Eric Wieser]

Eric Wieser said:

Though I guess the downside is that adding a nolint causes all of mathlib to rebuild

But this should never happen, right? We should only be removing things from here, probably in bulk

[Mario Carneiro]

Geoffrey Irving said:

No, I haven't been able to do that for months because there is an ABI bug which causes lean to crash unless I build mathlib myself.

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Crashing.20bug.2C.20possibly.20related.20to.20UInt64.20arithmetic/near/474354843

By the way, you should be able to work around this issue by using the leantar patch in that thread, although you will have to build it yourself

[Mario Carneiro]

(I have just updated the branch to include all versions up to v4.13.0-rc1)

[Damiano Testa]

Is this, (batteries#980), already a fix for the issue reported here?

[Julian Berman]

Eric Wieser said:

Maybe the actual issue here is that lake build should not show warnings from dependent projects unless you ask it to, cc Mac Malone

I'm finding this thread after noticing the same thing happen (to a repository I updated) -- I'm guessing because I see it them that no behavior changed here -- not sure if there was any follow-up discussion but just putting in a vote of support for this kind of solution, to me it seems like the right direction as well; I don't think downstream projects of a dependency should see many warnings coming from the dependency by default. In Python this was botched ~10-15 years ago to the point where things were silenced too much such that nearly no useful warnings are seen by default (with this reasoning being given that it was too noisy for downstream projects), but as long as there's some decent way of indicating which warnings are of what category I think it's possible to improve upon.