chore: rename no_lints_prime_decls.txt to nolints_... (#19383)

For consistency with the other nolints files. Suggested in #19275.

Mathlib/Tactic/Linter/DocPrime.lean

@@ -26,7 +26,7 @@ namespace Mathlib.Linter
 The "docPrime" linter emits a warning on declarations that have no doc-string and whose
 name ends with a `'`.
 
-The file `scripts/no_lints_prime_decls.txt` contains a list of temporary exceptions to this linter.
+The file `scripts/nolints_prime_decls.txt` contains a list of temporary exceptions to this linter.
 This list should not be appended to, and become emptied over time.
 -/
 register_option linter.docPrime : Bool := {
@@ -63,8 +63,8 @@ def docPrimeLinter : Linter where run := withSetOptionIn fun stx ↦ do
       relative to the unprimed version, or an explanation as to why no better naming scheme \
       is possible."
   if docstring[0][1].getAtomVal.isEmpty && declName.toString.back == '\'' then
-    if ← System.FilePath.pathExists "scripts/no_lints_prime_decls.txt" then
-      if (← IO.FS.lines "scripts/no_lints_prime_decls.txt").contains declName.toString then
+    if ← System.FilePath.pathExists "scripts/nolints_prime_decls.txt" then
+      if (← IO.FS.lines "scripts/nolints_prime_decls.txt").contains declName.toString then
         return
       else
         Linter.logLint linter.docPrime declId msg

scripts/README.md

@@ -80,8 +80,7 @@ to learn about it as well!
 **Data files with linter exceptions**
 - `nolints.json` contains exceptions for all `env_linter`s in mathlib.
   For permanent and deliberate exceptions, add a `@[nolint lintername]` in the .lean file instead.
-- `no_lints_prime_decls.txt`
-  contains temporary exceptions for the `docPrime` linter
+- `nolints_prime_decls.txt` contains temporary exceptions for the `docPrime` linter
 
 Both of these files should tend to zero over time;
 please do not add new entries to these files. PRs removing (the need for) entries are welcome.

scripts/technical-debt-metrics.sh

@@ -113,7 +113,7 @@ printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nol
 printf '%s|%s\n' "$(git grep '^set_option linter.style.longFile [0-9]*' Mathlib | wc -l)" "large files"
 printf '%s|%s\n' "$(git grep "^open .*Classical" | grep -v " in$" -c)" "bare open (scoped) Classical"
 
-printf '%s|%s\n' "$(wc -l < scripts/no_lints_prime_decls.txt)" "exceptions for the docPrime linter"
+printf '%s|%s\n' "$(wc -l < scripts/nolints_prime_decls.txt)" "exceptions for the docPrime linter"
 
 deprecatedFiles="$(git ls-files '**/Deprecated/*.lean' | xargs wc -l | sed 's=^ *==')"