Skip to content

Commit

Permalink
fix(HashCommandLinter): remove unnecessary, broken workaround for tes…
Browse files Browse the repository at this point in the history
…ts (#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.
  • Loading branch information
adomani committed Jan 7, 2025
1 parent 01b6f1b commit dd5ea93
Showing 1 changed file with 2 additions and 5 deletions.
7 changes: 2 additions & 5 deletions Mathlib/Tactic/Linter/HashCommandLinter.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit dd5ea93

Please sign in to comment.