feat(scripts): count the number of tactics without a docstring (leanprover-community#32131)

We want to make sure every tactic is well documented. Right now, I count 33 tactics in Mathlib without any docstring at all. Add this number to the weekly technical debt metrics bot so we can track it and fix any regressions.

Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

Author: Vierkantor

Mathlib.lean

@@ -6637,6 +6637,7 @@ public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PPRoundtrip
 public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
+public import Mathlib.Tactic.Linter.TacticDocumentation
 public import Mathlib.Tactic.Linter.TextBased
 public import Mathlib.Tactic.Linter.UnusedInstancesInType
 public import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/Init.lean

@@ -17,6 +17,7 @@ public import Mathlib.Tactic.Linter.Lint
 public import Mathlib.Tactic.Linter.Multigoal
 public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PrivateModule
+public import Mathlib.Tactic.Linter.TacticDocumentation
 -- The following import contains the environment extension for the unused tactic linter.
 public import Mathlib.Tactic.Linter.UnusedTacticExtension
 public import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/Tactic.lean

@@ -176,6 +176,7 @@ public import Mathlib.Tactic.Linter.OldObtain
 public import Mathlib.Tactic.Linter.PPRoundtrip
 public import Mathlib.Tactic.Linter.PrivateModule
 public import Mathlib.Tactic.Linter.Style
+public import Mathlib.Tactic.Linter.TacticDocumentation
 public import Mathlib.Tactic.Linter.TextBased
 public import Mathlib.Tactic.Linter.UnusedInstancesInType
 public import Mathlib.Tactic.Linter.UnusedTactic

Mathlib/Tactic/Linter/TacticDocumentation.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+module
+
+meta import Batteries.Tactic.Lint.Basic
+meta import Lean.Elab.Tactic.Doc
+import Lean.Parser.Tactic.Doc
+import Mathlib.Tactic.Linter.Header
+
+/-! # The `tacticDocs` linter
+
+The `tacticDocs` environment linter checks that all tactics defined in a module come with
+a (nonempty) docstring.
+-/
+
+open Lean Parser Elab Command
+
+open Tactic.Doc
+
+/-- Does this tactic have a docstring, or an `extensionDoc` defined later? -/
+meta def isNonemptyDoc (doc : TacticDoc) : Bool :=
+  doc.docString.isSome || doc.extensionDocs.any (! ·.isEmpty)
+
+/-- Check that all tactics available in Mathlib have a docstring. -/
+@[env_linter] meta def tacticDocs : Batteries.Tactic.Lint.Linter where
+  noErrorsFound := "No tactics are missing documentation."
+  errorsFound := "TACTICS ARE MISSING DOCUMENTATION STRINGS:"
+  test tac := do
+    let env ← getEnv
+
+    -- Only run on unique tactics (where tactics are defined as parsers in the tactic kind).
+    if !isTactic env tac || (alternativeOfTactic env tac).isSome then
+      return none
+
+    -- Find the associated documentation.
+    let docs ← Tactic.Doc.allTacticDocs
+    let docMap : NameMap _ := docs.foldl (init := {}) fun m doc =>
+      m.insert doc.internalName doc
+    -- This `get?` should not return `none` for normally declared tactics,
+    -- but if we do environment manipulation it might give us weird results.
+    -- So we should allow the case of `none`.
+    let doc := docMap.get? tac
+    let name := (doc.map (·.userName)).getD tac.toString
+
+    if let some doc := doc then
+      if isNonemptyDoc doc then
+        return none
+
+    return m!"tactic `{name}` missing documentation string"

scripts/nolints.json

@@ -260,4 +260,15 @@
  ["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"],
  ["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
  ["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
- ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"]]
+ ["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
+ ["tacticDocs", "Mathlib.Tactic.tacticMatch_target_"],
+ ["tacticDocs", "Tactic.Elementwise.tacticElementwise!___"],
+ ["tacticDocs", "Tactic.Elementwise.tacticElementwise___"],
+ ["tacticDocs",
+  "AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac"],
+ ["tacticDocs",
+  "AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.tacticMem_tac_aux"],
+ ["tacticDocs", "Mathlib.Tactic.Conv.convLHS"],
+ ["tacticDocs", "Mathlib.Tactic.Conv.convRHS"],
+ ["tacticDocs", "Mathlib.Tactic.Find.«tactic#find_»"],
+ ["tacticDocs", "Mathlib.Tactic.GCongr.tacticGcongr_discharger"]]

scripts/technical-debt-metrics.sh

@@ -118,6 +118,7 @@ doubleDeprecs="$(git grep -A2 -- "set_option linter.deprecated false" -- ":^Math
 printf '%s|disabled deprecation lints\n' "$(( deprecs - doubleDeprecs ))"
 
 printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nolint entries"
+printf '%s|%s\n' "$(grep -c 'tacticDocs' scripts/nolints.json)" "undocumented tactics"
 # We count the number of large files, making sure to avoid counting the test file `MathlibTest/Lint.lean`.
 printf '%s|%s\n' "$(git grep '^set_option linter.style.longFile [0-9]*' Mathlib | wc -l)" "large files"