fix: silence the #-command linter on noisy commands (#20525)

Reported on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.23.20linter), the fix comes from [this update](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20status.20updates/near/486115503).

Mathlib/Tactic/Linter/HashCommandLinter.lean

@@ -67,7 +67,7 @@ logs a warning only for the `#`-commands that do not already emit a message. -/
 def hashCommandLinter : Linter where run := withSetOptionIn' fun stx => do
   let mod := (← getMainModule).components
   if Linter.getLinterValue linter.hashCommand (← getOptions) &&
-    ((← get).messages.toList.isEmpty || warningAsError.get (← getOptions)) &&
+    ((← get).messages.reportedPlusUnreported.isEmpty || warningAsError.get (← getOptions)) &&
     -- we check that the module is either not in `test` or, is `test.HashCommandLinter`
     (mod.getD 0 default != `test || (mod == [`test, `HashCommandLinter]))
     then

MathlibTest/HashCommandLinter.lean

@@ -2,12 +2,6 @@ import Lean.Elab.GuardMsgs
 import Mathlib.Tactic.AdaptationNote
 import Mathlib.Tactic.Linter.HashCommandLinter
 
-
--- #adaptation_note
--- The hashCommand linter started failing after https://github.com/leanprover/lean4/pull/6299
--- Disabling aync elaboration fixes it, but of course we're not going to do that globally.
-set_option Elab.async false
-
 set_option linter.hashCommand true
 
 section ignored_commands