Spurious docstring blame

Stream: CSLib

[Shreyas Srinivas]

I am getting a spurious docstring linter error in cslib#275

Automatically detecting modules to lint
Default modules: #[Cslib]
-- Found 1 error in 2303 declarations (plus 6406 automatically generated ones) in Cslib with 17 linters

/- The `docBlame` linter reports:
DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- Cslib.AlgorithmsTheory.QueryModel
.../cslib/Cslib/AlgorithmsTheory/QueryModel.lean:66:1: error: @Cslib.Algorithms.Model.timeQuery definition missing documentation string

[Shreyas Srinivas]

As you can see in the latest commit, the docstring is clearly available : https://github.com/leanprover/cslib/pull/275/changes/7e57d1548fcdc7b19e35894933bd6cf5c2559a5e

[Shreyas Srinivas]

This only happens locally apparently when I run lake lint

[Chris Henson]

Yes, environment linters are from lake lint, which just like Mathlib uses runLinter from batteries. It seems you resolved this already? I don't see any error locally or in CI.

[Shreyas Srinivas]

I still get it in my local folder

[Chris Henson]

Have you run lake build since adding the docstring? This is required for environment linters.

[Shreyas Srinivas]

I think so. I’ll try again

[Shreyas Srinivas]

Apparently it is fixed locally now

[Shreyas Srinivas]

Thanks

[Shreyas Srinivas]

I did need to run lake build again