Commit 2026-04-29 03:39 d543ec18

feat(Tactic/Linter/Header): make header linter work downstream (#38396) This PR makes linter.style.header usable in projects downstream of Mathlib. Previously isInMathlib hardcoded a lookup of Mathlib.lean, so the linter silently exited early in (e.g.) CSLib even when enabled via linter.mathlibStandardSet. The fix uses the root of the current mainModule to find the aggregator file, so Cslib.Foo.Bar now checks Cslib.lean, matching the standard Lean convention that a library named Foo has its root file at Foo.lean. The "skip the aggregator itself" check is generalised from mainModule == \MathlibtomainModule == mainModule.getRoot`. Reported by Chris Henson on Zulip; cc @chenson2018 @grunweg. 🤖 Prepared with Claude Code