The docPrime linter uses the file scripts/nolints_prime_decls.txt to keep track of which primed declarations already existed when the linter was created and should not be flagged by the linter.

This works well for mathlib, but downstream projects get flooded by warnings when they build mathlib from scratch, instead of downloading the cache via lake exe cache get.

The reason is that the linter looks for the file in scripts/nolints_prime_decls.txt, does not find it in the downstream project and therefore complains about all primed declarations. Once the cache has been saved with the linter warnings, lake then replays it every time.

For this reason, the docPrime linter is now disabled in mathlib.

See these previous Zulip discussions:

• https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/docPrime.20hell
• https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20import.20performance.20in.20neovim
• https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/suppressing.20set_option.20linter.2EdocPrime.20false.20warnings.3F
• https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/theorem.20names.20with.20primes.3F

#20559 is the PR where the linter was disabled.