From b0890aa4ad52262811ba72d7f467848c16b5a497 Mon Sep 17 00:00:00 2001
From: grunweg <rothgang@math.uni-bonn.de>
Date: Fri, 22 Nov 2024 22:03:26 +0000
Subject: [PATCH] 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                         | 6 +++---
 scripts/README.md                                           | 3 +--
 .../{no_lints_prime_decls.txt => nolints_prime_decls.txt}   | 0
 scripts/technical-debt-metrics.sh                           | 2 +-
 4 files changed, 5 insertions(+), 6 deletions(-)
 rename scripts/{no_lints_prime_decls.txt => nolints_prime_decls.txt} (100%)

diff --git a/Mathlib/Tactic/Linter/DocPrime.lean b/Mathlib/Tactic/Linter/DocPrime.lean
index 7221a12e1ad7f..c2a8a38fbcdcf 100644
--- a/Mathlib/Tactic/Linter/DocPrime.lean
+++ b/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
diff --git a/scripts/README.md b/scripts/README.md
index 8f55ce30822bb..44156380d5e62 100644
--- a/scripts/README.md
+++ b/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.
diff --git a/scripts/no_lints_prime_decls.txt b/scripts/nolints_prime_decls.txt
similarity index 100%
rename from scripts/no_lints_prime_decls.txt
rename to scripts/nolints_prime_decls.txt
diff --git a/scripts/technical-debt-metrics.sh b/scripts/technical-debt-metrics.sh
index eb24ded1ce153..b3f3df14ec9aa 100755
--- a/scripts/technical-debt-metrics.sh
+++ b/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=^ *==')"