feat: the docPrime linter (#16694)

This syntax linter emits a warning on declarations whose name ends with a `'` and that have no doc-string.

By default, the linter is
* `on` on `mathlib` and
* `off` on projects depending on mathlib.

The file `scripts/no_lints_prime_decls.txt` contains the current exceptions.

The exceptions need to be managed manually by design: the expectation is that, once the linter starts, the nolints file should only decrease and never increase.  In particular, after the linter flags a declaration, simply adding manually an exception is *not enough* for CI to be successful.  There needs to be a change in the file with the exception (or upstream from it), since otherwise `lake` will replay the `olean`s and keep emitting the initial warning.  The expectation is that the change will be the addition of a doc-string.



Co-authored-by: Michael Rothgang <[email protected]>

Mathlib.lean

@@ -4272,6 +4272,7 @@ import Mathlib.Tactic.LinearCombination'
 import Mathlib.Tactic.LinearCombination.Lemmas
 import Mathlib.Tactic.Linter
 import Mathlib.Tactic.Linter.AdmitLinter
+import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.FlexibleLinter
 import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.HashCommandLinter

Mathlib/Init.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.HashCommandLinter
 import Mathlib.Tactic.Linter.GlobalAttributeIn
 -- This file imports Batteries.Tactic.Lint, where the `env_linter` attribute is defined.

Mathlib/Tactic.lean

@@ -134,6 +134,7 @@ import Mathlib.Tactic.LinearCombination'
 import Mathlib.Tactic.LinearCombination.Lemmas
 import Mathlib.Tactic.Linter
 import Mathlib.Tactic.Linter.AdmitLinter
+import Mathlib.Tactic.Linter.DocPrime
 import Mathlib.Tactic.Linter.FlexibleLinter
 import Mathlib.Tactic.Linter.GlobalAttributeIn
 import Mathlib.Tactic.Linter.HashCommandLinter

Mathlib/Tactic/Linter/DocPrime.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2024 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import Lean.Elab.Command
+
+/-!
+# The "docPrime" linter
+
+The "docPrime" linter emits a warning on declarations that have no doc-string and whose
+name ends with a `'`. Such declarations are expected to have a documented explanation
+for the presence of a `'` in their name. This may consist of discussion of the difference relative
+to an unprimed version of that declaration, or an explanation as to why no better naming scheme
+is possible.
+-/
+
+open Lean Elab
+
+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.
+This list should not be appended to, and become emptied over time.
+-/
+register_option linter.docPrime : Bool := {
+  defValue := false
+  descr := "enable the docPrime linter"
+}
+
+namespace DocPrime
+
+@[inherit_doc Mathlib.Linter.linter.docPrime]
+def docPrimeLinter : Linter where run := withSetOptionIn fun stx ↦ do
+  unless Linter.getLinterValue linter.docPrime (← getOptions) do
+    return
+  if (← get).messages.hasErrors then
+    return
+  unless [``Lean.Parser.Command.declaration, `lemma].contains stx.getKind do return
+  let docstring := stx[0][0]
+  -- The current declaration's id, possibly followed by a list of universe names.
+  let declId :=
+    if stx[1].isOfKind ``Lean.Parser.Command.instance then
+      stx[1][3][0]
+    else
+      stx[1][1]
+  -- The name of the current declaration, with namespaces resolved.
+  let declName :=
+    if let `_root_ :: rest := declId[0].getId.components then
+      rest.foldl (· ++ ·) default
+    else (← getCurrNamespace) ++ declId[0].getId
+  let msg := m!"`{declName}` is missing a doc-string, please add one.\n\
+      Declarations whose name ends with a `'` are expected to contain an explanation for the \
+      presence of a `'` in their doc-string. This may consist of discussion of the difference \
+      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
+        return
+      else
+        Linter.logLint linter.docPrime declId msg
+    else
+      Linter.logLint linter.docPrime declId msg
+
+initialize addLinter docPrimeLinter
+
+end DocPrime
+
+end Mathlib.Linter

lakefile.lean

@@ -25,6 +25,7 @@ require "leanprover-community" / "LeanSearchClient" @ git "main"
   (as well as `Archive`, `Counterexamples` and `test`).
 -/
 abbrev mathlibOnlyLinters : Array LeanOption := #[
+  ⟨`linter.docPrime, true⟩,
   ⟨`linter.hashCommand, true⟩,
   ⟨`linter.oldObtain, true,⟩,
   ⟨`linter.refine, true⟩,