Properly silence the docPrime linter in downstream projects

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.

Start by reading the docPrime linter and its use of scripts/nolints_prime_decls.txt, then review the linked Zulip discussions and PR #20559. Reproduce a downstream build without the cache and compare the warnings with a cached build. Done means downstream projects no longer receive the flood of docPrime warnings when building mathlib from scratch.