Commit 2025-12-18 04:36 dfccc70a

fix(Linter): deprecated module linter now fires for public/meta imports (#32422) This PR fixes the deprecated module linter to recognize all import variants from the new module system (public import, meta import, import all, etc.). Previously, getImportIds used a syntax pattern that only matched plain import $n, missing the optional modifiers. Additionally:

• The duplicate import linter now considers modifiers, so public import Foo and import all Foo are correctly treated as distinct imports
• Added exemptions for Mathlib.lean (auto-generated) and Mathlib/Tactic (may need deprecated imports for tactics to work)
• Fixed deprecated imports in Mathlib.Geometry.Euclidean.Angle.Unoriented files (Mathlib.Analysis.NormedSpace.Normalize → Mathlib.Analysis.Normed.Module.Normalize) Reported on Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.20has.20moved.20to.20the.20new.20module.20system/near/561825752 🤖 Prepared with Claude Code