From dd5ea9368cd7f0c205558d02f59fdf9c89018fdf Mon Sep 17 00:00:00 2001 From: damiano Date: Tue, 7 Jan 2025 14:23:23 +0000 Subject: [PATCH] fix(HashCommandLinter): remove unnecessary, broken workaround for tests (#20529) The old workaround for `test` is wrong on two accounts. 1. The test directory is now called `MathlibTest`, not `test`. 2. With the weak-option settings that mathlib uses, the test files are all already opt-in for the linters anyways. --- Mathlib/Tactic/Linter/HashCommandLinter.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Mathlib/Tactic/Linter/HashCommandLinter.lean b/Mathlib/Tactic/Linter/HashCommandLinter.lean index e4bcb714f146f..41832c0f4570b 100644 --- a/Mathlib/Tactic/Linter/HashCommandLinter.lean +++ b/Mathlib/Tactic/Linter/HashCommandLinter.lean @@ -65,12 +65,9 @@ This means that CI will eventually fail on `#`-commands, but does not stop it fr However, in order to avoid local clutter, when `warningAsError` is `false`, the linter 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.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 + ((← get).messages.reportedPlusUnreported.isEmpty || warningAsError.get (← getOptions)) + then if let some sa := stx.getHead? then let a := sa.getAtomVal if (a.get ⟨0⟩ == '#' && ! allowed_commands.contains a) then