Lean4
/-- Check the `Syntax` `imports` for broad imports:
`Mathlib.Tactic`, any import starting with `Lake`, or `Mathlib.Tactic.{Have,Replace}`. -/
def broadImportsCheck (imports : Array Syntax) (mainModule : Name) : CommandElabM Unit := do
for i in imports do
match i.getId with
| `Mathlib.Tactic =>
Linter.logLint linter.style.header i "Files in mathlib cannot import the whole tactic folder."
| `Mathlib.Tactic.Replace =>
if mainModule != `Mathlib.Tactic then
Linter.logLint linter.style.header i
"'Mathlib.Tactic.Replace' defines a deprecated form of the 'replace' tactic; \
please do not use it in mathlib."
| `Mathlib.Tactic.Have =>
if ![`Mathlib.Tactic, `Mathlib.Tactic.Replace].contains mainModule then
Linter.logLint linter.style.header i
"'Mathlib.Tactic.Have' defines a deprecated form of the 'have' tactic; \
please do not use it in mathlib."
| modName =>
if modName.getRoot == `Lake then
Linter.logLint linter.style.header i
"In the past, importing 'Lake' in mathlib has led to dramatic slow-downs of the linter \
(see e.g. https://github.com/leanprover-community/mathlib4/pull/13779). Please consider carefully if this import is useful and \
make sure to benchmark it. If this is fine, feel free to silence this linter."
