From aa37b8130b84fe5850f4e0917307d50e6b40c5b4 Mon Sep 17 00:00:00 2001 From: damiano Date: Mon, 6 Jan 2025 20:17:04 +0000 Subject: [PATCH] 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 | 2 +- MathlibTest/HashCommandLinter.lean | 6 ------ 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index 1f01c9b69a412..e4bcb714f146f 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/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 diff --git a/MathlibTest/HashCommandLinter.lean b/MathlibTest/HashCommandLinter.lean index cf5304e11e734..4193342406c14 100644 --- a/MathlibTest/HashCommandLinter.lean +++ b/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