suppressing set_option linter.docPrime false warnings?

Stream: mathlib4

[Jason Gross]

This is probably a very basic lean question: I have a project that has mathlib as a dependency. Every time I run lake build, I get ~2k lines of warnings from mathlib saying things

warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/CauSeq/Basic.lean:475:8: `CauSeq.mul_equiv_zero'` 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`

How can I suppress these warnings so I only see the errors from my project?

[Jason Gross]

(If it's relevant, I set up my project with lake +leanprover-community/mathlib4:lean-toolchain new <NAME> math)

[Michael Rothgang]

You can disable the linter in the project lakefile. Example for a lakefile.toml.

[Michael Rothgang]

(Do you have a lakefile.lean? Then you need something like this.)

[Jason Gross]

I added linter.docPrime = false to the [leanOptions] section of lakefile.toml, but then I get

trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH= /Users/jason/.elan/toolchains/leanprover--lean4---v4.15.0-rc1/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -Dlinter.docPrime=false ././././Testing2/Basic.lean -R ./././. -o ././.lake/build/lib/Testing2/Basic.olean -i ././.lake/build/lib/Testing2/Basic.ilean -c ././.lake/build/ir/Testing2/Basic.c --json
error: <input>:1:0: invalid -D parameter, unknown configuration option 'linter.docPrime'

If the option is defined in this library, use '-Dweak.linter.docPrime' to set it conditionally

If instead I do weak.linter.docPrime = false, then I still see messages like:

⚠ [684/697] Replayed Mathlib.Algebra.Order.CauSeq.Basic
warning: ././.lake/packages/mathlib/././Mathlib/Algebra/Order/CauSeq/Basic.lean:121:6: `IsCauSeq.bounded'` 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/Algebra/Order/CauSeq/Basic.lean:199:8: `CauSeq.bounded'` 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/Algebra/Order/CauSeq/Basic.lean:475:8: `CauSeq.mul_equiv_zero'` 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`

on lake build.

[Eric Wieser]

@Michael Rothgang, note the linter message is coming from mathlib itself; this looks like a bug

[Ruben Van de Velde]

This should not happen. Can you share your lakefile?

[Ruben Van de Velde]

And lake manifest

[Damiano Testa]

I think that this may be happening because the cache for Mathlib is not the one downloaded via lake exe cache get.

[Damiano Testa]

If you can get the "correct" cache, then the warnings should not appear.

[Jason Gross]

Ah, indeed, I forgot to do lake exe cache get and instead just ran lake build.

[Damiano Testa]

So, this is expected, but undesired behaviour, unfortunately.

[Eric Wieser]

Can you elaborate on why this is expected, Damiano?

[Kim Morrison]

Yes, we really need to make this not happen!

[Kim Morrison]

We can't assume people will use the cache.

[Damiano Testa]

Sorry to be late here. I can't find the references, but I very vaguely remember two possible issues.

• The search path for the no-lints file is wrong for dependencies, since it is stored in .lake/..., instead of scripts/...: this could be fixed by using a better search path on the linter side, but I was under the impression that lake would handle the search-paths for dependencies by looking directly inside the dependencies folder.
• lake uses the value of the Mathlibs option, even when a dependency sets it to something different: I do not know if this is the case, but I have found it hard to figure out the correct way of setting the options. If this is the issue, maybe I can look again at whether there is an error there.

I really wish I could find the previous discussion for this, but I am failing...

[awalterschulze]

Just for reference
I also got these warnings when running lake build, even after running lake exe cache get.
But it was fixed after running lake clean and then lake exe cache get and now I only get the warnings from my project, which is what I want.
Thank you