Caching of lints

Stream: mathlib4

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It looks like in #17341 I ran into an instance of missing cache invalidation. In the first commit, one file failed due to a linter warning. I modified one of the nolint files (no_lints_prime_decls.txt) to fix this, but it seems not to be included in Lake's list of build inputs. Thus, even after the change the file is replayed from cache and the build continues to fail. What should I do to fix this?

[Kim Morrison]

@Mac Malone, could you advise here?

[Mac Malone]

My suggestion would be to add the no lint files as a target (via inputTextFile) and an extraDepTargets of the relevant libaries (or the whole package). For example, something like this:

target no_lints pkg : Unit := do
  let noLintFiles := #[
    pkg.dir / "scripts" / "no_lints_prime_decls.txt",
    pkg.dir / "scripts" / "nolints-style.txt",
    pkg.dir / "scripts" / "nolints.json"
  ]
  BuildJob.mixArray (← noLintFiles.mapM (inputTextFile ·))

package mathlib where
  extraDepTargets := #{`no_lints]

[Yury G. Kudryashov]

Why not add a docstring instead?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

@Yury G. Kudryashov as in, obey the lint? The lemma in question is

@[simp]
lemma coe_mk' (carrier : Set R) (h₁ h₂ h₃ h₄ h₅) :
    (mk' carrier h₁ h₂ h₃ h₄ h₅ : Set R) = carrier

which I feel doesn't really deserve a docstring. Also, even though this particular issue can be fixed this way, the issue of overzealous caching would remain.