feat: tag linter warnings for recordLints

[wkrozowski]

This PR makes Lean.Linter.logLint attach an internal tag to every
linter warning so that Lean.Linter.recordLints can reliably distinguish
linter-produced messages from other tagged messages (named errors,
unknown-identifier messages, hasSorry markers, etc.). Previously,
recordLints captured every message whose top-level kind was non-anonymous,
which over-recorded non-linter diagnostics into the persistent lint log.

The change preserves the existing MessageData.kind of linter warnings (it
still returns the linter option name) by nesting the sentinel tag inside the
kind tag. A new helper MessageData.isLinterMessage is exposed alongside the
existing isDeprecationWarning / isUnusedVariableWarning predicates.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for 6ce247a against 55cf1d7 are in. No significant results found. @wkrozowski

• 🟥 build//instructions: +741.3M (+0.01%)

Small changes (3✅, 2🟥)

• 🟥 build/module/Lean.Linter.Init//instructions: +15.9M (+1.68%)
• 🟥 build/module/Lean.Linter.PersistentLintLog//instructions: +20.1M (+2.84%)
• ✅ compiled/parser//task-clock: -188ms (-8.22%)
• ✅ compiled/parser//wall-clock: -188ms (-8.21%)
• ✅ mvcgen/sym/PurePrecond/400/kernel//wall-clock: -9ms (-7.03%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 55cf1d71e8dc1217c559d6426571d237beb84e46 --onto 2cd98639c40d2d2a026dd599093b70f55f55ffaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-25 18:48:21)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 55cf1d71e8dc1217c559d6426571d237beb84e46 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-05-25 18:48:23)