Commit 2026-10-21 00:36 10156080

feat(Tactic/Linter/Header): access library root without cwd (#45061) This PR modifies the way the header linter finds the library root from the current module. Instead of assuming that the current working directory contains the root, we peel off components from the current filename and match them against the current module name until we reach the root. We also adjust the directory dependency linter to take in a srcDir when locating Mathlib.Init and scripts/forbiddenDirs.json, which we provide as the parent of this filepath. This is both more principled and enables us to apply header linter suggestions from skimmer, which is started from scripts/. It also has the effect of (correctly) running these linters when building mathlib as an upstream dependency, just as we run mathlib's other linters in the same circumstance. Note that the scripts/ folder is distributed along with the source files, so we are still able to locate scripts/forbiddenDirs.json successfully. (This was tested locally with a minimal downstream project.) This was used in conjunction with #44507 to create #45071. (This PR also adjusts the style of some nearby but unrelated MessageData handling.)