fix: fix #lint by marking tacticDocs as public (leanprover-community#33322)

This PR fixes `#lint`, which had been reporting

> Unknown constant `_private.Mathlib.Tactic.Linter.TacticDocumentation.0.tacticDocs`

by marking `tacticDocs` as `public`.

See [#mathlib4 > #lint is broken @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23lint.20is.20broken/near/565443234).

Author: thorimur

Mathlib/Tactic/Linter/TacticDocumentation.lean

@@ -5,9 +5,9 @@ Authors: Anne Baanen
 -/
 module
 
-meta import Batteries.Tactic.Lint.Basic
-meta import Lean.Elab.Tactic.Doc
-import Lean.Parser.Tactic.Doc
+public meta import Batteries.Tactic.Lint.Basic
+public meta import Lean.Elab.Tactic.Doc
+public meta import Lean.Parser.Tactic.Doc
 import Mathlib.Tactic.Linter.Header
 
 /-! # The `tacticDocs` linter
@@ -25,7 +25,7 @@ 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
+@[env_linter] public meta def tacticDocs : Batteries.Tactic.Lint.Linter where
   noErrorsFound := "No tactics are missing documentation."
   errorsFound := "TACTICS ARE MISSING DOCUMENTATION STRINGS:"
   test tac := do

MathlibTest/HashLint.lean

@@ -0,0 +1,14 @@
+module
+
+import Mathlib.Init
+
+/-! Checks that a basic `#lint` works. -/
+
+/--
+info: -- Found 0 errors in 0 declarations (plus 0 automatically generated ones) in the current file with 16 linters
+
+
+-- All linting checks passed!
+-/
+#guard_msgs in
+#lint