chore(Tactic/Linter/Style): check declIDs

Mathlib/ModelTheory/PartialEquiv.lean

@@ -236,11 +236,12 @@ def toEmbeddingOfEqTop {f : M ≃ₚ[L] N} (h : f.dom = ⊤) : M ↪[L] N :=
   (h ▸ f.toEmbedding).comp topEquiv.symm.toEmbedding
 
 @[simp]
-theorem toEmbeddingOfEqTop__apply {f : M ≃ₚ[L] N} (h : f.dom = ⊤) (m : M) :
+theorem toEmbeddingOfEqTop_apply {f : M ≃ₚ[L] N} (h : f.dom = ⊤) (m : M) :
     toEmbeddingOfEqTop h m = f.toEquiv ⟨m, h.symm ▸ mem_top m⟩ := by
   rcases f with ⟨dom, cod, g⟩
   cases h
   rfl
+@[deprecated (since := "2024-10-09")] alias toEmbeddingOfEqTop__apply := toEmbeddingOfEqTop_apply
 
 /-- Given a partial equivalence which has the whole structure as domain and
   as codomain, returns the corresponding equivalence. -/

Mathlib/Tactic/Linter/Style.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Michael Rothgang
 -/
 
+import Batteries.Data.String.Matcher
 import Lean.Elab.Command
 
 /-!
@@ -12,7 +13,7 @@ import Lean.Elab.Command
 This file contains (currently one, eventually more) linters about stylistic aspects:
 these are only about coding style, but do not affect correctness nor global coherence of mathlib.
 
-Historically, these were ported from the `lint-style.py` Python script.
+Historically, some of these were ported from the `lint-style.py` Python script.
 -/
 
 open Lean Elab Command
@@ -68,4 +69,53 @@ initialize addLinter setOptionLinter
 
 end Style.setOption
 
+/-- The `check_declID` linter: if it emits a warning, then a declID is considered
+non-standard style.  -/
+register_option linter.style.check_declID : Bool := {
+  defValue := false
+  descr := "enable the `setOption` linter"
+}
+
+
+namespace Style.checkDeclID
+
+/-- Checks whether a given identifier name contains "__". -/
+def contains_double_underscore (stx : Syntax) : Bool :=
+  (stx.getSubstring?.get!).containsSubstr "__"
+
+/-- `getNames stx` returns all `declId`s in the input syntax `stx`. -/
+partial
+def getNames : Syntax → Array Syntax
+  | stx@(.node _ kind args) =>
+    let rargs := (args.map getNames).flatten
+    if kind == ``Lean.Parser.Command.declId then rargs.push stx else rargs
+  | _ => default
+
+/-- The `checkDeclID` linter: if this linter emits a warning, then a declID is considered
+non-standard style. Currently we only check if it contains a double underscore ("__") as a
+substring.
+
+**Why is this bad?** Double underscores in theorem names can be considered non-standard style and
+probably have been introduced by accident
+**How to fix this?** Use single underscores to separate parts of a name, following standard naming
+conventions.
+-/
+def checkDeclIDLinter: Linter where
+  run := withSetOptionIn fun _stx => do
+    unless Linter.getLinterValue linter.style.check_declID (← getOptions) do
+      return
+    if (← MonadState.get).messages.hasErrors then
+      return
+    for stx in (getNames _stx) do
+      if (contains_double_underscore stx) then
+        Linter.logLint linter.style.check_declID stx
+          m!"The declID '{stx}' contains '__', which does not follow naming conventions. \
+              Consider using single underscores instead."
+      else
+        continue
+
+initialize addLinter checkDeclIDLinter
+
+end Style.checkDeclID
+
 end Mathlib.Linter

lakefile.lean

@@ -36,6 +36,7 @@ abbrev mathlibOnlyLinters : Array LeanOption := #[
   ⟨`linter.style.longFile, .ofNat 1500⟩,
   ⟨`linter.style.missingEnd, true⟩,
   ⟨`linter.style.setOption, true⟩,
+  ⟨`linter.style.check_declID, true⟩,
   ⟨`aesop.warn.applyIff, false⟩ -- This became a problem after https://github.com/leanprover-community/aesop/commit/29cf094e84ae9852f0011b47b6ddc684ffe4be5f
 ]
 

test/LintStyle.lean

@@ -134,4 +134,13 @@ lemma foo' : True := trivial
 
 -- TODO: add terms for the term form
 
+/--
+warning: The declID 'double__underscore' contains '__', which does not follow naming conventions.
+Consider using single underscores instead.
+note: this linter can be disabled with `set_option linter.style.check_declID false`
+-/
+#guard_msgs in
+set_option linter.style.check_declID true in
+theorem double__underscore : True := trivial
+
 end setOption