refactor(Tactic/Linter/Header): make the header linter stateful

[marcelolynch]

This PR rewrites the header linter as a stateful linter (leanprover/lean4#14357). Linter behavior on well-formed files does not change. All four header linter test files pass without changes.

The linter state replaces two pieces of ad-hoc machinery:

• The state caches the library-root check. This removes the Std.Mutex that guarded the cache against concurrent async linter runs.
• The state records a verdict for the module: the header checks ran, or the module is exempt. The linter checks the header of each module exactly once, and every later command takes a fast path.

One behavior improves on malformed files: a file without a module doc-string gets one set of warnings at its first command. The previous implementation repeated the full header parse and its warnings on every command of such a file. The repeated parse was the largest per-command cost of the linter, for example during edits of a new file that does not have its module doc-string yet.

Other performance effects are small. After the verdict, each command reads one state field, and the end-of-file checks of the consumer linters replace a header parse with a state read.

The state also stores the parsed module header, and the header linter becomes a producer. The minImports and longLine linters read the parsed header from the state for their end-of-file checks, instead of a re-parse of the file. When the header checks did not run, both linters fall back to the previous re-parse. Two new tests pin the payload path and the fallback path of the minImports report.

• depends on: refactor(Tactic/Linter/MinImports): make the minImports linter stateful #42186

🤖 Generated with Claude Code

[github-actions]

PR summary a314edf962

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ HeaderState
+ async_uses_norm_num
+ headerChecks
+ headerPost
+ longLinePost
+ minImportsPost
- headerLinter
- longLineLinter
- minImportsLinter

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a314edf962
Reference commit 3b6f23172a

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• refactor(Tactic/Linter/MinImports): make the minImports linter stateful #42186
  By Dependent Issues (🤖). Happy coding!