`#grind_lint` does not recognize grind sets

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

If I have a custom grind set:

module

public import Lean.Meta.Tactic.Grind.RegisterCommand

register_grind_attr foo

it is not recognized by #grind_lint

module

public import Foo.Basic

@[foo =]
public theorem bar : 1 = 1 := rfl

/--error: `bar` is not marked with the `@[grind]` attribute for theorem instantiation -/
#guard_msgs in
#grind_lint skip bar

Context

Discussed with Kim in office hours, this thread contains Mathlib PRs proposing their usage.

Steps to Reproduce

Create the modules listed above.

Expected behavior:

Allow #grind_lint reporting of theorems from custom grind sets, possibly with some options to control what sets are reported.

Actual behavior:

The error shown above.

Versions

Lean 4.29.1 Target: x86_64-unknown-linux-gnu

Additional Information

N/A

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the example with Lean.Meta.Tactic.Grind.RegisterCommand, Foo.Basic, and #grind_lint, then inspect the implementation and registration path used by #grind_lint. Done means a theorem marked with a custom grind set is recognized without the reported error, while the existing guard-message reproduction passes.