From 37280a98387504d7adf48c85a756ba68a85f347a Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 10:41:17 -0300
Subject: [PATCH 01/13] refactor(Tactic/Linter/MinImports): make the minImports
 linter stateful

Rewrite the minImports linter with the stateful linter API
(leanprover/lean4#14357). The cumulative import data moves from a global
IO.Ref into the linter state, which the elaborator threads through the
commands of the file. The IO.Ref was unsafe under parallel elaboration,
so `#import_bumps` had to set `Elab.async false`; the stateful state is
safe and the option stays on.

Linter behavior is unchanged: MathlibTest/MinImports.lean passes as is
(validated on a nightly-2026-07-27 toolchain).

NOTE: CI stays red until the toolchain bump to v4.34.0-rc1, which first
provides `registerStatefulLinter`.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/MinImports.lean | 187 +++++++++++++++-----------
 1 file changed, 109 insertions(+), 78 deletions(-)

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index 01648ac8527692..e123d23b0cc6d6 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -19,6 +19,10 @@ Unlike the related `#min_imports` command, the linter takes into account notatio
 information.
 It also works incrementally, accumulating increasing import information.
 This is better suited, for instance, to split files.
+
+The linter is a stateful linter (`Lean.Elab.Command.registerStatefulLinter`). It stores the
+cumulative import information in its linter state, and the elaborator threads the state
+through the commands of the file.
 -/
 
 meta section
@@ -34,14 +38,15 @@ The "minImports" linter tracks information about minimal imports over several co
 namespace Mathlib.Linter
 
 /--
-`ImportState` is the structure keeping track of the data that the `minImports` linter uses.
+`ImportState` is the persistent state of the `minImports` linter.
 * `transClosure` is the import graph of the current file.
 * `minImports` is the `NameSet` of minimal imports to build the file up to the current command.
 * `importSize` is the number of transitive imports to build the file up to the current command.
 -/
-structure ImportState where
-  /-- The transitive closure of the import graph of the current file.  The value is `none` only at
-  initialization time, as the linter immediately sets it to its value for the current file. -/
+public structure ImportState where
+  /-- The transitive closure of the import graph of the current file. The value is `none` only
+  before the linter processes the first command. The linter then sets it to the value for the
+  current file. -/
   transClosure : Option (NameMap NameSet) := none
   /-- The minimal imports needed to build the file up to the current command. -/
   minImports   : NameSet := {}
@@ -49,13 +54,11 @@ structure ImportState where
   importSize   : Nat := 0
   deriving Inhabited
 
-/--
-`minImportsRef` keeps track of cumulative imports across multiple commands, using `ImportState`.
--/
-initialize minImportsRef : IO.Ref ImportState ← IO.mkRef {}
-
-/-- `#reset_min_imports` sets to empty the current list of cumulative imports. -/
-elab "#reset_min_imports" : command => minImportsRef.set {}
+/-- `#reset_min_imports` makes the `minImports` linter start again from empty cumulative
+imports. -/
+-- Only the linter can write the linter state. The elaborator does nothing: the `minImports`
+-- linter detects the `resetMinImports` syntax kind and clears its state.
+elab (name := resetMinImports) "#reset_min_imports" : command => pure ()
 
 /--
 The `minImports` linter incrementally computes the minimal imports needed for each file to build.
@@ -100,76 +103,104 @@ def importsBelow (tc : NameMap NameSet) (ms : NameSet) : NameSet :=
 macro "#import_bumps" : command => `(
   -- We emit a message to prevent the `#`-command linter from flagging `#import_bumps`.
   run_cmd logInfo "Counting imports from here."
-  set_option Elab.async false
   set_option linter.minImports true)
 
+/--
+`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
+option values to the current scope. Then it runs `k` on the innermost command.
+The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
+stateful linter.
+-/
+private partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
+    Syntax → CommandElabM α :=
+  fun stx => do
+    if stx.getKind == ``Lean.Parser.Command.in &&
+       stx[0].getKind == ``Lean.Parser.Command.set_option then
+      -- Do not modify the infotrees when elaborating, and silently ignore errors.
+      let opts ← withEnableInfoTree false try
+          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
+        catch _ => getOptions
+      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
+    else
+      k stx
+
 @[inherit_doc Mathlib.Linter.linter.minImports]
-def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do
-    unless getLinterValue linter.minImports (← getLinterOptions) do
-      return
-    if (← get).messages.hasErrors then
-      return
-    if stx == (← `(command| #import_bumps)) then return
-    if stx == (← `(command| set_option $(mkIdent `linter.minImports) true)) then
-      logInfo "Try using '#import_bumps', instead of manually setting the linter option: \
-              the linter works best with linear parsing of the file and '#import_bumps' \
-              also sets the `Elab.async` option to `false`."
-      return
-    let env ← getEnv
-    -- the first time `minImportsRef` is read, it has `transClosure = none`;
-    -- in this case, we set it to be the `transClosure` for the file.
-    if (← minImportsRef.get).transClosure.isNone then
-      minImportsRef.modify ({· with transClosure := env.importGraph.transitiveClosure})
-    let impState ← minImportsRef.get
-    let (importsSoFar, oldCumulImps) := (impState.minImports, impState.importSize)
-    -- when the linter reaches the end of the file or `#exit`, it gives a report
-    if #[``Parser.Command.eoi, ``Lean.Parser.Command.exit].contains stx.getKind then
-      let explicitImportsInFile : NameSet :=
-        .ofArray ((env.imports.map (·.module)).filter (!isInitImport ·))
-      let newImps := importsSoFar \ explicitImportsInFile
-      let currentlyUnneededImports := explicitImportsInFile \ importsSoFar
-      -- we read the current file, to do a custom parsing of the imports:
-      -- this is a hack to obtain some `Syntax` information for the `import X` commands
-      let fname ← getFileName
-      let contents ← IO.FS.readFile fname
-      -- `impMods` is the syntax for the modules imported in the current file
-      let (impMods, _) ← Parser.parseHeader (Parser.mkInputContext contents fname)
-      for i in currentlyUnneededImports do
-        match impMods.raw.find? (·.getId == i) with
-          | some impPos => logWarningAt impPos m!"unneeded import '{i}'"
-          | _ => dbg_trace f!"'{i}' not found"  -- this should be unreachable
-      -- if the linter found new imports that should be added (likely to *reduce* the dependencies)
-      if !newImps.isEmpty then
-        -- format the imports prepending `import ` to each module name
-        let withImport := (newImps.toArray.qsort Name.lt).map (s!"import {·}")
-        -- log a warning at the first `import`, if there is one.
-        logWarningAt ((impMods.raw.find? (·.isOfKind `import)).getD default)
-          m!"-- missing imports\n{"\n".intercalate withImport.toList}"
-    let id ← getId stx
-    let newImports := (getIrredundantImports env (← getAllImports stx id)).filter (!isInitImport ·)
-    let tot := (newImports.append importsSoFar)
-    let redundant := env.findRedundantImports tot.toArray
-    let currImports := tot \ redundant
-    let currImpArray := currImports.toArray.qsort Name.lt
-    if currImpArray != #[] &&
-       currImpArray ≠ importsSoFar.toArray.qsort Name.lt then
-      let newCumulImps := -- We should always be in the situation where `getD` finds something
-        (importsBelow (impState.transClosure.getD env.importGraph.transitiveClosure) tot).size
-      minImportsRef.modify ({· with minImports := currImports, importSize := newCumulImps})
-      let new := currImpArray.filter (!importsSoFar.contains ·)
-      let redundant := importsSoFar.toArray.filter (!currImports.contains ·)
-      -- to make `test` files more stable, we suppress the exact count of import changes if
-      -- the `linter.minImports.increases` option is `false`
-      let byCount :=  if getLinterValue linter.minImports.increases (← getLinterOptions) then
-                      m!"by {newCumulImps - oldCumulImps} "
-                    else
-                      m!""
-      Linter.logLint linter.minImports stx <|
-        m!"Imports increased {byCount}to\n{currImpArray}\n\n\
-          New imports: {new}\n" ++
-            if redundant.isEmpty then m!"" else m!"\nNow redundant: {redundant}\n"
-
-initialize addLinter minImportsLinter
+def minImportsPost (stx : Syntax) (self : ImportState) : CommandElabM ImportState := do
+  -- The reset applies also when the linter option is off. The linter then lints the
+  -- `#reset_min_imports` command itself, against the empty state.
+  let self := if stx.isOfKind ``resetMinImports then {} else self
+  unless getLinterValue linter.minImports (← getLinterOptions) do
+    return self
+  if (← get).messages.hasErrors then
+    return self
+  if stx == (← `(command| #import_bumps)) then return self
+  if stx == (← `(command| set_option $(mkIdent `linter.minImports) true)) then
+    logInfo "Consider using '#import_bumps' instead of setting the linter option: \
+            it also logs the position where the import count starts."
+    return self
+  let env ← getEnv
+  -- On the first command that the linter processes, it computes the transitive closure of the
+  -- imports of the file.
+  let self := if self.transClosure.isNone then
+      { self with transClosure := env.importGraph.transitiveClosure }
+    else self
+  let (importsSoFar, oldCumulImps) := (self.minImports, self.importSize)
+  -- when the linter reaches the end of the file or `#exit`, it gives a report
+  if #[``Parser.Command.eoi, ``Lean.Parser.Command.exit].contains stx.getKind then
+    let explicitImportsInFile : NameSet :=
+      .ofArray ((env.imports.map (·.module)).filter (!isInitImport ·))
+    let newImps := importsSoFar \ explicitImportsInFile
+    let currentlyUnneededImports := explicitImportsInFile \ importsSoFar
+    -- we read the current file, to do a custom parsing of the imports:
+    -- this is a hack to obtain some `Syntax` information for the `import X` commands
+    let fname ← getFileName
+    let contents ← IO.FS.readFile fname
+    -- `impMods` is the syntax for the modules imported in the current file
+    let (impMods, _) ← Parser.parseHeader (Parser.mkInputContext contents fname)
+    for i in currentlyUnneededImports do
+      match impMods.raw.find? (·.getId == i) with
+        | some impPos => logWarningAt impPos m!"unneeded import '{i}'"
+        | _ => dbg_trace f!"'{i}' not found"  -- this should be unreachable
+    -- if the linter found new imports that should be added (likely to *reduce* the dependencies)
+    if !newImps.isEmpty then
+      -- format the imports prepending `import ` to each module name
+      let withImport := (newImps.toArray.qsort Name.lt).map (s!"import {·}")
+      -- log a warning at the first `import`, if there is one.
+      logWarningAt ((impMods.raw.find? (·.isOfKind `import)).getD default)
+        m!"-- missing imports\n{"\n".intercalate withImport.toList}"
+    return self
+  let id ← getId stx
+  let newImports := (getIrredundantImports env (← getAllImports stx id)).filter (!isInitImport ·)
+  let tot := (newImports.append importsSoFar)
+  let redundant := env.findRedundantImports tot.toArray
+  let currImports := tot \ redundant
+  let currImpArray := currImports.toArray.qsort Name.lt
+  if currImpArray != #[] &&
+     currImpArray ≠ importsSoFar.toArray.qsort Name.lt then
+    let newCumulImps := -- We should always be in the situation where `getD` finds something
+      (importsBelow (self.transClosure.getD env.importGraph.transitiveClosure) tot).size
+    let new := currImpArray.filter (!importsSoFar.contains ·)
+    let redundant := importsSoFar.toArray.filter (!currImports.contains ·)
+    -- to make `test` files more stable, we suppress the exact count of import changes if
+    -- the `linter.minImports.increases` option is `false`
+    let byCount :=  if getLinterValue linter.minImports.increases (← getLinterOptions) then
+                    m!"by {newCumulImps - oldCumulImps} "
+                  else
+                    m!""
+    Linter.logLint linter.minImports stx <|
+      m!"Imports increased {byCount}to\n{currImpArray}\n\n\
+        New imports: {new}\n" ++
+          if redundant.isEmpty then m!"" else m!"\nNow redundant: {redundant}\n"
+    return { self with minImports := currImports, importSize := newCumulImps }
+  return self
+
+/--
+The typed handle of the `minImports` linter. Other stateful linters can read the previous
+`ImportState` of the linter through this handle.
+-/
+public initialize minImportsLinter : StatefulLinter ImportState Unit ←
+  registerStatefulLinter {}
+    (post := fun stx self _ _ _ => withSetOptionIn' (minImportsPost · self) stx)
 
 end MinImports
 

From fec2cfa3474362bcf5a8e71f09fd30eb3b7a430a Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 11:07:59 -0300
Subject: [PATCH 02/13] test(MinImports): pin linter behavior under parallel
 elaboration

The new section runs with Elab.async explicitly on: the linter state
accumulates correctly across commands, and #import_bumps keeps parallel
elaboration enabled.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 MathlibTest/MinImports.lean | 58 +++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)

diff --git a/MathlibTest/MinImports.lean b/MathlibTest/MinImports.lean
index 5d1ce54b16f228..5a2b5fcddf4783 100644
--- a/MathlibTest/MinImports.lean
+++ b/MathlibTest/MinImports.lean
@@ -277,3 +277,61 @@ inductive ProposeToMoveThisInductive where
 theorem theorem_with_local_inductive : Nonempty ProposeToMoveThisInductive := ⟨.foo 0⟩
 
 end Linter.UpstreamableDecl
+
+section Linter.MinImports.Async
+
+/-!
+The `minImports` linter is a stateful linter: the elaborator threads the linter state through
+the commands of the file, so the accumulated imports are correct under parallel elaboration.
+The tests below run with `Elab.async` explicitly on, and check that `#import_bumps` keeps
+parallel elaboration enabled.
+-/
+
+set_option Elab.async true
+set_option linter.minImports.increases false
+
+-- Earlier sections of this file leave imports in the linter state: start from a clean state.
+set_option linter.minImports false in
+#reset_min_imports
+
+/-- info: Counting imports from here. -/
+#guard_msgs in
+#import_bumps
+
+-- `#import_bumps` must keep parallel elaboration on.
+set_option linter.minImports false in
+run_cmd do
+  unless Lean.Elab.async.get (← Lean.getOptions) do
+    throwError "`#import_bumps` must keep `Elab.async` on"
+
+/--
+warning: Imports increased to
+[Mathlib.Data.Int.Notation]
+
+New imports: [Mathlib.Data.Int.Notation]
+
+
+Note: This linter can be disabled with `set_option linter.minImports false`
+-/
+#guard_msgs in
+#guard (0 : ℤ) = 0
+
+#guard_msgs in
+-- no new imports needed here, so no message
+#guard (0 : ℤ) = 0
+
+/--
+warning: Imports increased to
+[Mathlib.Tactic.NormNum.Basic]
+
+New imports: [Mathlib.Tactic.NormNum.Basic]
+
+Now redundant: [Mathlib.Data.Int.Notation]
+
+
+Note: This linter can be disabled with `set_option linter.minImports false`
+-/
+#guard_msgs in
+lemma async_uses_norm_num : (0 + 1 : ℕ) = 1 := by norm_num
+
+end Linter.MinImports.Async

From c1dbc650843555174d1cd5a41af2f3b9785b30d6 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 11:11:17 -0300
Subject: [PATCH 03/13] doc(Tactic/Linter/MinImports): link the upstreaming PR
 for withSetOptionIn'

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/MinImports.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index e123d23b0cc6d6..03eddc8c4b70ac 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -105,6 +105,7 @@ macro "#import_bumps" : command => `(
   run_cmd logInfo "Counting imports from here."
   set_option linter.minImports true)
 
+-- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
 /--
 `withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
 option values to the current scope. Then it runs `k` on the innermost command.

From e8cad372b0713f9b6d48ad9873a2e2d9645abe64 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 11:41:18 -0300
Subject: [PATCH 04/13] doc(Tactic/Linter/MinImports): note possible reset
 semantics for #import_bumps

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/MinImports.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index 03eddc8c4b70ac..18a715a90521b8 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -54,6 +54,7 @@ public structure ImportState where
   importSize   : Nat := 0
   deriving Inhabited
 
+-- TODO: we could give `#import_bumps` reset semantics and deprecate `#reset_min_imports`.
 /-- `#reset_min_imports` makes the `minImports` linter start again from empty cumulative
 imports. -/
 -- Only the linter can write the linter state. The elaborator does nothing: the `minImports`

From de8260678eb89313b0f7ff124a72b59a380cdfe5 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 16:55:45 -0300
Subject: [PATCH 05/13] refactor(Tactic/Linter/Header): make the header linter
 stateful

Rewrite the header linter with the stateful linter API
(leanprover/lean4#14357). The linter state caches the library-root
check, which replaces the Std.Mutex that guarded the cache against
concurrent async linter runs, and records that the checks ran, so the
linter checks the header of each module exactly once. A file without a
module doc-string gets one set of warnings at its first command; the
IO.Ref-era behavior repeated the full header parse and its warnings on
every command of such a file.

Linter behavior on well-formed files is unchanged; the header linter
tests pass as is (validated on a nightly-2026-07-27 toolchain).

NOTE: CI stays red until the toolchain bump to v4.34.0-rc1, which first
provides `registerStatefulLinter`.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/Header.lean | 138 +++++++++++++++++++-----------
 1 file changed, 88 insertions(+), 50 deletions(-)

diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index 40b79e7b281843..fb57668e5a246e 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -7,7 +7,6 @@ module
 
 public meta import Lean.Elab.Command
 public meta import Lean.Elab.ParseImportsFast
-public meta import Std.Sync.Mutex
 public import Lean.Parser.Module
 public import Mathlib.Tactic.Linter.DirectoryDependency
 
@@ -52,6 +51,10 @@ after it.
 This makes it possible for the linter to check the entire header of the file, emit warnings that
 could arise from this part and also flag that the file should contain a module doc-string after
 the `import` statements.
+
+The linter is a stateful linter (`Lean.Elab.Command.registerStatefulLinter`). Its state caches
+the result of the library-root check, and it records that the checks ran: the linter checks the
+header of each module once.
 -/
 
 meta section
@@ -263,15 +266,16 @@ def isInLibraryRoot (modName : Name) : IO Bool := do
     return res.imports.any (·.module == modName)
   else return false
 
-/-- `inLibraryRootMutex` caches whether the current file is imported in the library root file
-(e.g. `Mathlib.lean`), as computed by `isInLibraryRoot`. It is
-* `none` at initialization time;
-* `some true` if the `header` linter has already discovered that the current file
-  is imported in the library root file;
-* `some false` if the `header` linter has already discovered that the current file
-  is *not* imported in the library root file.
--/
-initialize inLibraryRootMutex : Std.Mutex (Option Bool) ← Std.Mutex.new none
+/-- `HeaderState` is the persistent state of the `header` linter. -/
+public structure HeaderState where
+  /-- Whether the current module is imported in the library root file (e.g. `Mathlib.lean`),
+  as computed by `isInLibraryRoot`. The value is `none` before the linter computes it.
+  The state caches the answer, because `isInLibraryRoot` reads the library root file from
+  disk. -/
+  inLibraryRoot? : Option Bool := none
+  /-- `true` after the header checks ran. The linter checks the header of each module once. -/
+  ran : Bool := false
+  deriving Inhabited
 
 /--
 The "header" style linter checks that a file starts with
@@ -369,51 +373,41 @@ def headerTestFiles : NameSet := .ofList
   [`MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, `MathlibTest.Linter.Header.Verso,
   `MathlibTest.DirectoryDependencyLinter.Test]
 
-@[inherit_doc Mathlib.Linter.linter.style.header]
-def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
-  let mainModule ← getMainModule
-  unless getLinterValue linter.style.header (← getLinterOptions) do
-    return
-  if (← get).messages.hasErrors then
-    return
-  let inLibraryRoot? ← inLibraryRootMutex.atomically do
-    match ← get with
-    | some d => return d
-    | none =>
-      let val ← isInLibraryRoot mainModule
-      -- We cache the answer to avoid recomputing it on every command. The fill runs under the mutex
-      -- so that concurrent (async) linter runs don't all miss the cache and each redundantly parse
-      -- the library root file; `mainModule` is fixed for the duration of the elaboration.
-      set (some val)
-      return val
-  -- The linter skips files not imported in their library root (e.g. `Mathlib.lean`), to avoid
-  -- linting "scratch files". It is however active in the test files for the linter itself.
-  unless inLibraryRoot? || headerTestFiles.contains mainModule do return
-  -- Skip linting the library root file itself.
-  -- In practice, the `inLibraryRoot?` check above already covers this (a well-formed `<root>.lean`
-  -- does not import itself), but a root module could appear in `headerTestFiles`.
-  if mainModule == mainModule.getRoot then return
-  let fm ← getFileMap
-  let mdDocs := (getMainModuleDoc (← getEnv)).toArray
-  let versoDocs := (getMainVersoModuleDocs (← getEnv)).snippets
-  -- The end of the first module doc-string, or the end of the file if there is none.
-  -- For robustness, we assume Markdown and Verso docstrings can be arbitrarily mixed,
-  -- so we get the end pos for both types of docstrings and take their minimum as the first.
-  let firstMDDocModPos := match mdDocs[0]? with
-  | none     => fm.positions.back!
-  | some doc => fm.ofPosition doc.declarationRange.endPos
-  let firstVersoDocModPos := match versoDocs[0]? with
-  | none     => fm.positions.back!
-  | some doc => fm.ofPosition doc.declarationRange.endPos
-  let firstDocModPos := min firstMDDocModPos firstVersoDocModPos
-  unless stx.getTailPos?.getD default ≤ firstDocModPos do
-    return
+/--
+`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
+option values to the current scope. Then it runs `k` on the innermost command.
+The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
+stateful linter.
+-/
+private partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
+    Syntax → CommandElabM α :=
+  fun stx => do
+    if stx.getKind == ``Lean.Parser.Command.in &&
+       stx[0].getKind == ``Lean.Parser.Command.set_option then
+      -- Do not modify the infotrees when elaborating, and silently ignore errors.
+      let opts ← withEnableInfoTree false try
+          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
+        catch _ => getOptions
+      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
+    else
+      k stx
+
+/--
+`headerChecks stx mainModule firstDocModPos` runs the header checks for the current module:
+the copyright header, broad or duplicate imports, directory dependencies, and the position of
+the first module doc-string. `stx` is the command that triggers the checks, and
+`firstDocModPos` is the end position of the first module doc-string of the file, or the end of
+the file when there is none.
+-/
+def headerChecks (stx : Syntax) (mainModule : Name) (firstDocModPos : String.Pos.Raw) :
+    CommandElabM Unit := do
   -- We try to parse the file up to `firstDocModPos`.
   let upToStx ← parseUpToHere firstDocModPos <|> (do
     -- If parsing failed, there is some command which is not a module docstring.
     -- In that case, we parse until the end of the imports and add an extra `section` afterwards,
     -- so we trigger a "no module doc-string" warning.
     let fil ← getFileName
+    let fm ← getFileMap
     let (stx, _) ← Parser.parseHeader { inputString := fm.source, fileName := fil, fileMap := fm }
     parseUpToHere (stx.raw.getTailPos?.getD default) "\nsection")
   let importIds := getImportIds upToStx
@@ -449,7 +443,51 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
       m!"The module doc-string for a file should be the first command after the imports.\n\
        Please, add a module doc-string before `{stx}`."
 
-initialize addLinter headerLinter
+@[inherit_doc Mathlib.Linter.linter.style.header]
+def headerPost (stx : Syntax) (self : HeaderState) : CommandElabM HeaderState := do
+  let mainModule ← getMainModule
+  unless getLinterValue linter.style.header (← getLinterOptions) do
+    return self
+  if (← get).messages.hasErrors then
+    return self
+  let inLibraryRoot ← match self.inLibraryRoot? with
+    | some b => pure b
+    | none => isInLibraryRoot mainModule
+  let self := { self with inLibraryRoot? := some inLibraryRoot }
+  -- The linter skips files not imported in their library root (e.g. `Mathlib.lean`), to avoid
+  -- linting "scratch files". It is however active in the test files for the linter itself.
+  unless inLibraryRoot || headerTestFiles.contains mainModule do return self
+  -- Skip linting the library root file itself.
+  -- In practice, the `inLibraryRoot` check above already covers this (a well-formed `<root>.lean`
+  -- does not import itself), but a root module could appear in `headerTestFiles`.
+  if mainModule == mainModule.getRoot then return self
+  let fm ← getFileMap
+  let mdDocs := (getMainModuleDoc (← getEnv)).toArray
+  let versoDocs := (getMainVersoModuleDocs (← getEnv)).snippets
+  -- The end of the first module doc-string, or the end of the file if there is none.
+  -- For robustness, we assume Markdown and Verso docstrings can be arbitrarily mixed,
+  -- so we get the end pos for both types of docstrings and take their minimum as the first.
+  let firstMDDocModPos := match mdDocs[0]? with
+  | none     => fm.positions.back!
+  | some doc => fm.ofPosition doc.declarationRange.endPos
+  let firstVersoDocModPos := match versoDocs[0]? with
+  | none     => fm.positions.back!
+  | some doc => fm.ofPosition doc.declarationRange.endPos
+  let firstDocModPos := min firstMDDocModPos firstVersoDocModPos
+  unless stx.getTailPos?.getD default ≤ firstDocModPos do
+    return self
+  headerChecks stx mainModule firstDocModPos
+  return { self with ran := true }
+
+/--
+The typed handle of the `header` linter. Other stateful linters can read the previous
+`HeaderState` of the linter through this handle.
+-/
+public initialize headerLinter : StatefulLinter HeaderState Unit ←
+  registerStatefulLinter {}
+    (post := fun stx self _ _ _ => do
+      if self.ran then return self
+      withSetOptionIn' (headerPost · self) stx)
 
 end Style.header
 

From 3799adf31d594960e583ed0ab96fe38b7421dc46 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 17:18:58 -0300
Subject: [PATCH 06/13] doc(Tactic/Linter/Header): link the upstreaming PR for
 withSetOptionIn'

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/Header.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index fb57668e5a246e..1db78ef5856320 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -373,6 +373,7 @@ def headerTestFiles : NameSet := .ofList
   [`MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, `MathlibTest.Linter.Header.Verso,
   `MathlibTest.DirectoryDependencyLinter.Test]
 
+-- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
 /--
 `withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
 option values to the current scope. Then it runs `k` on the innermost command.

From d9be336ce1eadec31628e6da0170850ddf94a2d7 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 17:38:03 -0300
Subject: [PATCH 07/13] feat(Tactic/Linter/Header): store the parsed header in
 the linter state

The header linter state gains two things. The `headerSyntax` field
stores the parsed module header, so other linters can read it instead
of a re-parse of the file. The `settled` flag replaces `ran` and also
covers exempt modules, so every command of an exempt file takes the
same fast path as a checked file.

The `withSetOptionIn'` helper moves to the `Mathlib.Linter` namespace
and becomes public: the consumer linters share the single copy.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/Header.lean | 94 +++++++++++++++++--------------
 1 file changed, 51 insertions(+), 43 deletions(-)

diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index 1db78ef5856320..45f9c115c70df5 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -54,7 +54,9 @@ the `import` statements.
 
 The linter is a stateful linter (`Lean.Elab.Command.registerStatefulLinter`). Its state caches
 the result of the library-root check, and it records that the checks ran: the linter checks the
-header of each module once.
+header of each module once. The state also stores the parsed module header. Other linters, such
+as `minImports` and `longLine`, read the parsed header from the state instead of a re-parse of
+the file.
 -/
 
 meta section
@@ -273,10 +275,35 @@ public structure HeaderState where
   The state caches the answer, because `isInLibraryRoot` reads the library root file from
   disk. -/
   inLibraryRoot? : Option Bool := none
-  /-- `true` after the header checks ran. The linter checks the header of each module once. -/
-  ran : Bool := false
+  /-- `true` after the linter reaches a verdict for the module: the header checks ran, or the
+  module is exempt from the checks. Every later command takes a fast path. -/
+  settled : Bool := false
+  /-- The syntax of the module header: the copyright comment and the `import` commands, with
+  source positions in the current file. The value is `.missing` when the header checks did not
+  run. Other linters read this field to avoid a re-parse of the header. -/
+  headerSyntax : Syntax := .missing
   deriving Inhabited
 
+-- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
+/--
+`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
+option values to the current scope. Then it runs `k` on the innermost command.
+The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
+stateful linter.
+-/
+public partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
+    Syntax → CommandElabM α :=
+  fun stx => do
+    if stx.getKind == ``Lean.Parser.Command.in &&
+       stx[0].getKind == ``Lean.Parser.Command.set_option then
+      -- Do not modify the infotrees when elaborating, and silently ignore errors.
+      let opts ← withEnableInfoTree false try
+          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
+        catch _ => getOptions
+      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
+    else
+      k stx
+
 /--
 The "header" style linter checks that a file starts with
 ```
@@ -371,46 +398,16 @@ because they are files that test the linter.
 -/
 def headerTestFiles : NameSet := .ofList
   [`MathlibTest.Linter.Header.Basic, `MathlibTest.Linter.Header.Fail, `MathlibTest.Linter.Header.Verso,
-  `MathlibTest.DirectoryDependencyLinter.Test]
-
--- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
-/--
-`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
-option values to the current scope. Then it runs `k` on the innermost command.
-The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
-stateful linter.
--/
-private partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
-    Syntax → CommandElabM α :=
-  fun stx => do
-    if stx.getKind == ``Lean.Parser.Command.in &&
-       stx[0].getKind == ``Lean.Parser.Command.set_option then
-      -- Do not modify the infotrees when elaborating, and silently ignore errors.
-      let opts ← withEnableInfoTree false try
-          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
-        catch _ => getOptions
-      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
-    else
-      k stx
+  `MathlibTest.Linter.Header.MinImportsPayload, `MathlibTest.DirectoryDependencyLinter.Test]
 
 /--
-`headerChecks stx mainModule firstDocModPos` runs the header checks for the current module:
+`headerChecks stx mainModule upToStx` runs the header checks for the current module:
 the copyright header, broad or duplicate imports, directory dependencies, and the position of
-the first module doc-string. `stx` is the command that triggers the checks, and
-`firstDocModPos` is the end position of the first module doc-string of the file, or the end of
-the file when there is none.
+the first module doc-string. `stx` is the command that triggers the checks, and `upToStx` is
+the parse of the file up to the first module doc-string.
 -/
-def headerChecks (stx : Syntax) (mainModule : Name) (firstDocModPos : String.Pos.Raw) :
+def headerChecks (stx : Syntax) (mainModule : Name) (upToStx : Syntax) :
     CommandElabM Unit := do
-  -- We try to parse the file up to `firstDocModPos`.
-  let upToStx ← parseUpToHere firstDocModPos <|> (do
-    -- If parsing failed, there is some command which is not a module docstring.
-    -- In that case, we parse until the end of the imports and add an extra `section` afterwards,
-    -- so we trigger a "no module doc-string" warning.
-    let fil ← getFileName
-    let fm ← getFileMap
-    let (stx, _) ← Parser.parseHeader { inputString := fm.source, fileName := fil, fileMap := fm }
-    parseUpToHere (stx.raw.getTailPos?.getD default) "\nsection")
   let importIds := getImportIds upToStx
   let imports := getImports upToStx
   let afterImports := firstNonImport? upToStx
@@ -457,11 +454,13 @@ def headerPost (stx : Syntax) (self : HeaderState) : CommandElabM HeaderState :=
   let self := { self with inLibraryRoot? := some inLibraryRoot }
   -- The linter skips files not imported in their library root (e.g. `Mathlib.lean`), to avoid
   -- linting "scratch files". It is however active in the test files for the linter itself.
-  unless inLibraryRoot || headerTestFiles.contains mainModule do return self
+  -- Exemption is a per-module constant, so the verdict settles the state.
+  unless inLibraryRoot || headerTestFiles.contains mainModule do
+    return { self with settled := true }
   -- Skip linting the library root file itself.
   -- In practice, the `inLibraryRoot` check above already covers this (a well-formed `<root>.lean`
   -- does not import itself), but a root module could appear in `headerTestFiles`.
-  if mainModule == mainModule.getRoot then return self
+  if mainModule == mainModule.getRoot then return { self with settled := true }
   let fm ← getFileMap
   let mdDocs := (getMainModuleDoc (← getEnv)).toArray
   let versoDocs := (getMainVersoModuleDocs (← getEnv)).snippets
@@ -477,8 +476,17 @@ def headerPost (stx : Syntax) (self : HeaderState) : CommandElabM HeaderState :=
   let firstDocModPos := min firstMDDocModPos firstVersoDocModPos
   unless stx.getTailPos?.getD default ≤ firstDocModPos do
     return self
-  headerChecks stx mainModule firstDocModPos
-  return { self with ran := true }
+  -- We try to parse the file up to `firstDocModPos`.
+  let upToStx ← parseUpToHere firstDocModPos <|> (do
+    -- If parsing failed, there is some command which is not a module docstring.
+    -- In that case, we parse until the end of the imports and add an extra `section` afterwards,
+    -- so we trigger a "no module doc-string" warning.
+    let fil ← getFileName
+    let (stx, _) ← Parser.parseHeader { inputString := fm.source, fileName := fil, fileMap := fm }
+    parseUpToHere (stx.raw.getTailPos?.getD default) "\nsection")
+  headerChecks stx mainModule upToStx
+  -- `upToStx` is a `Lean.Parser.Module.module` node. Its first argument is the module header.
+  return { self with settled := true, headerSyntax := upToStx[0] }
 
 /--
 The typed handle of the `header` linter. Other stateful linters can read the previous
@@ -487,7 +495,7 @@ The typed handle of the `header` linter. Other stateful linters can read the pre
 public initialize headerLinter : StatefulLinter HeaderState Unit ←
   registerStatefulLinter {}
     (post := fun stx self _ _ _ => do
-      if self.ran then return self
+      if self.settled then return self
       withSetOptionIn' (headerPost · self) stx)
 
 end Style.header

From 6f2cb49e8b7bce758a7fccb9a1bb885ef96c8d78 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 17:38:03 -0300
Subject: [PATCH 08/13] refactor(Tactic/Linter/MinImports): read the parsed
 header from the header linter state

The end-of-file report positions its warnings with the parsed header
from the state of the header linter. When the header checks did not
run, the report falls back to the previous behavior: it reads the file
and parses the header again.

Two new tests pin both paths. MathlibTest/Linter/Header/MinImportsPayload.lean
exercises the payload path, and a new section in MathlibTest/MinImports.lean
exercises the fallback. A temporary throwError probe in the fallback
verified that each test takes its intended path.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/MinImports.lean         | 47 ++++++----------
 .../Linter/Header/MinImportsPayload.lean      | 56 +++++++++++++++++++
 MathlibTest/MinImports.lean                   | 16 ++++++
 3 files changed, 90 insertions(+), 29 deletions(-)
 create mode 100644 MathlibTest/Linter/Header/MinImportsPayload.lean

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index 18a715a90521b8..e75f20bbed1091 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -7,6 +7,7 @@ module
 
 public meta import ImportGraph.Imports.ImportGraph
 public meta import ImportGraph.Graph.TransitiveClosure
+public meta import Mathlib.Tactic.Linter.Header
 public import Mathlib.Tactic.MinImports
 
 /-! # The `minImports` linter
@@ -106,28 +107,10 @@ macro "#import_bumps" : command => `(
   run_cmd logInfo "Counting imports from here."
   set_option linter.minImports true)
 
--- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
-/--
-`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
-option values to the current scope. Then it runs `k` on the innermost command.
-The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
-stateful linter.
--/
-private partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
-    Syntax → CommandElabM α :=
-  fun stx => do
-    if stx.getKind == ``Lean.Parser.Command.in &&
-       stx[0].getKind == ``Lean.Parser.Command.set_option then
-      -- Do not modify the infotrees when elaborating, and silently ignore errors.
-      let opts ← withEnableInfoTree false try
-          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
-        catch _ => getOptions
-      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
-    else
-      k stx
 
 @[inherit_doc Mathlib.Linter.linter.minImports]
-def minImportsPost (stx : Syntax) (self : ImportState) : CommandElabM ImportState := do
+def minImportsPost (readPrev : PrevStateFn) (stx : Syntax) (self : ImportState) :
+    CommandElabM ImportState := do
   -- The reset applies also when the linter option is off. The linter then lints the
   -- `#reset_min_imports` command itself, against the empty state.
   let self := if stx.isOfKind ``resetMinImports then {} else self
@@ -153,14 +136,20 @@ def minImportsPost (stx : Syntax) (self : ImportState) : CommandElabM ImportStat
       .ofArray ((env.imports.map (·.module)).filter (!isInitImport ·))
     let newImps := importsSoFar \ explicitImportsInFile
     let currentlyUnneededImports := explicitImportsInFile \ importsSoFar
-    -- we read the current file, to do a custom parsing of the imports:
-    -- this is a hack to obtain some `Syntax` information for the `import X` commands
-    let fname ← getFileName
-    let contents ← IO.FS.readFile fname
-    -- `impMods` is the syntax for the modules imported in the current file
-    let (impMods, _) ← Parser.parseHeader (Parser.mkInputContext contents fname)
+    -- `impMods` is the syntax for the modules imported in the current file. The state of the
+    -- `header` linter provides it when the header checks ran. Otherwise, we read the current
+    -- file and do a custom parsing of the imports: this is a hack to obtain some `Syntax`
+    -- information for the `import X` commands.
+    let headerStx := (readPrev Style.header.headerLinter).headerSyntax
+    let impMods ← if headerStx.isMissing then do
+        let fname ← getFileName
+        let contents ← IO.FS.readFile fname
+        let (impMods, _) ← Parser.parseHeader (Parser.mkInputContext contents fname)
+        pure impMods.raw
+      else
+        pure headerStx
     for i in currentlyUnneededImports do
-      match impMods.raw.find? (·.getId == i) with
+      match impMods.find? (·.getId == i) with
         | some impPos => logWarningAt impPos m!"unneeded import '{i}'"
         | _ => dbg_trace f!"'{i}' not found"  -- this should be unreachable
     -- if the linter found new imports that should be added (likely to *reduce* the dependencies)
@@ -168,7 +157,7 @@ def minImportsPost (stx : Syntax) (self : ImportState) : CommandElabM ImportStat
       -- format the imports prepending `import ` to each module name
       let withImport := (newImps.toArray.qsort Name.lt).map (s!"import {·}")
       -- log a warning at the first `import`, if there is one.
-      logWarningAt ((impMods.raw.find? (·.isOfKind `import)).getD default)
+      logWarningAt ((impMods.find? (·.isOfKind `import)).getD default)
         m!"-- missing imports\n{"\n".intercalate withImport.toList}"
     return self
   let id ← getId stx
@@ -202,7 +191,7 @@ The typed handle of the `minImports` linter. Other stateful linters can read the
 -/
 public initialize minImportsLinter : StatefulLinter ImportState Unit ←
   registerStatefulLinter {}
-    (post := fun stx self _ _ _ => withSetOptionIn' (minImportsPost · self) stx)
+    (post := fun stx self _ readPrev _ => withSetOptionIn' (minImportsPost readPrev · self) stx)
 
 end MinImports
 
diff --git a/MathlibTest/Linter/Header/MinImportsPayload.lean b/MathlibTest/Linter/Header/MinImportsPayload.lean
new file mode 100644
index 00000000000000..e0b1288578b6be
--- /dev/null
+++ b/MathlibTest/Linter/Header/MinImportsPayload.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Marcelo Lynch. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcelo Lynch
+-/
+import Mathlib.Tactic.Linter.MinImports
+import Mathlib.Data.Int.Notation
+
+/--
+warning: The module doc-string for a file should be the first command after the imports.
+Please, add a module doc-string before `/-!# Tests for the header payload consumers
+-/
+`.
+
+Note: This linter can be disabled with `set_option linter.style.header false`
+-/
+#guard_msgs in
+set_option linter.style.header true in
+
+/-!
+# Tests for the header payload consumers
+-/
+
+/-! The `header` linter stores the parsed module header in its state. The `minImports` linter
+reads the parsed header for its end-of-file report. The command above enables the `header`
+linter on the module doc-string, so the linter runs its checks and stores the payload. The
+`#exit` command below then triggers the end-of-file report of the `minImports` linter, which
+positions the "unneeded import" warning with the payload. -/
+
+set_option linter.minImports.increases false
+
+/-- info: Counting imports from here. -/
+#guard_msgs in
+#import_bumps
+
+/--
+warning: Imports increased to
+[Mathlib.Data.Int.Notation]
+
+New imports: [Mathlib.Data.Int.Notation]
+
+
+Note: This linter can be disabled with `set_option linter.minImports false`
+-/
+#guard_msgs in
+#guard (0 : ℤ) = 0
+
+/--
+warning: using 'exit' to interrupt Lean
+---
+warning: unneeded import 'Mathlib.Tactic.Linter.MinImports'
+-/
+#guard_msgs in
+#exit
+
+set_option linter.minImports false
diff --git a/MathlibTest/MinImports.lean b/MathlibTest/MinImports.lean
index 5a2b5fcddf4783..482aef9880f07a 100644
--- a/MathlibTest/MinImports.lean
+++ b/MathlibTest/MinImports.lean
@@ -335,3 +335,19 @@ Note: This linter can be disabled with `set_option linter.minImports false`
 lemma async_uses_norm_num : (0 + 1 : ℕ) = 1 := by norm_num
 
 end Linter.MinImports.Async
+
+section Linter.MinImports.FallbackEoiReport
+
+/-! The `header` linter does not run in this file: the module is not in `headerTestFiles` and
+the file is not imported in a library root. The end-of-file report of the `minImports` linter
+then falls back to a re-parse of the file header. -/
+
+/--
+warning: using 'exit' to interrupt Lean
+---
+warning: unneeded import 'Mathlib.Tactic.FunProp.Attr'
+-/
+#guard_msgs in
+set_option linter.minImports true in #exit
+
+end Linter.MinImports.FallbackEoiReport

From a314edf96289433cc4e23a011d01efa26faf6937 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 28 Jul 2026 17:38:03 -0300
Subject: [PATCH 09/13] refactor(Tactic/Linter/Style): read the parsed header
 in the longLine linter

The longLine linter becomes a stateful linter with trivial state, so
its end-of-file check can read the parsed header from the state of the
header linter. When the header checks did not run, the check parses
the header itself, as before.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/Style.lean | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index 8e1d4af6bcdea4..17f6317e6ef96e 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -7,9 +7,7 @@ module
 
 public meta import Lean.Elab.Command
 public meta import Lean.Server.InfoUtils
--- Import this linter explicitly to ensure that
--- this file has a valid copyright header and module docstring.
-public meta import Mathlib.Tactic.Linter.Header  -- shake: keep
+public meta import Mathlib.Tactic.Linter.Header
 public import Lean.Parser.Command
 public import Mathlib.Tactic.DeclarationNames
 public import Batteries.Tactic.Lint.Basic
@@ -443,7 +441,7 @@ def isImport (s : String) : Bool :=
   s.startsWith "import all " || s.startsWith "meta import all "
 
 @[inherit_doc Mathlib.Linter.linter.style.longLine]
-def longLineLinter : Linter where run := withSetOptionIn fun stx ↦ do
+def longLinePost (readPrev : PrevStateFn) (stx : Syntax) : CommandElabM Unit := do
     unless getLinterValue linter.style.longLine (← getLinterOptions) do
       return
     if (← MonadState.get).messages.hasErrors then
@@ -456,11 +454,16 @@ def longLineLinter : Linter where run := withSetOptionIn fun stx ↦ do
     -- if the linter reached the end of the file, then we scan the `import` syntax instead
     let stx ← do
       if stx.isOfKind ``Lean.Parser.Command.eoi then
-        let fileMap ← getFileMap
-        -- `impMods` is the syntax for the modules imported in the current file
-        let (impMods, _) ← Parser.parseHeader
-          { inputString := fileMap.source, fileName := ← getFileName, fileMap := fileMap }
-        pure impMods.raw
+        -- `impMods` is the syntax for the modules imported in the current file. The state of
+        -- the `header` linter provides it when the header checks ran. Otherwise, we parse the
+        -- header of the file.
+        let headerStx := (readPrev Style.header.headerLinter).headerSyntax
+        if headerStx.isMissing then
+          let fileMap ← getFileMap
+          let (impMods, _) ← Parser.parseHeader
+            { inputString := fileMap.source, fileName := ← getFileName, fileMap := fileMap }
+          pure impMods.raw
+        else pure headerStx
       else pure stx
     let sstr := stx.getSubstring?
     let fm ← getFileMap
@@ -478,7 +481,13 @@ def longLineLinter : Linter where run := withSetOptionIn fun stx ↦ do
           (.ofRange ⟨(line.drop maxLineLength).startPos, line.stopPos⟩)
           m!"This line exceeds the {maxLineLength} character limit, please shorten it!{stringMsg}"
 
-initialize addLinter longLineLinter
+/--
+The typed handle of the `longLine` linter. The linter is stateful in order to read the state of
+the `header` linter; its own state is trivial.
+-/
+public initialize longLineLinter : StatefulLinter Unit Unit ←
+  registerStatefulLinter ()
+    (post := fun stx _ _ readPrev _ => withSetOptionIn' (longLinePost readPrev) stx)
 
 end Style.longLine
 

From a2fe02186deb5ae53207ae318b8611b1fdc448cb Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 11 Aug 2026 14:27:52 -0700
Subject: [PATCH 10/13] refactor(Tactic/Linter/MinImports): use
 `withSetOptionIn` from core

Core's `withSetOptionIn` now has an arbitrary result type
(leanprover/lean4#14581, in v4.34.0-rc1), so it fits the post phase of a
stateful linter. The private polymorphic copy goes away.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/MinImports.lean | 22 +---------------------
 1 file changed, 1 insertion(+), 21 deletions(-)

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index 18a715a90521b8..c12c4c9dc88844 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -106,26 +106,6 @@ macro "#import_bumps" : command => `(
   run_cmd logInfo "Counting imports from here."
   set_option linter.minImports true)
 
--- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
-/--
-`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
-option values to the current scope. Then it runs `k` on the innermost command.
-The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
-stateful linter.
--/
-private partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
-    Syntax → CommandElabM α :=
-  fun stx => do
-    if stx.getKind == ``Lean.Parser.Command.in &&
-       stx[0].getKind == ``Lean.Parser.Command.set_option then
-      -- Do not modify the infotrees when elaborating, and silently ignore errors.
-      let opts ← withEnableInfoTree false try
-          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
-        catch _ => getOptions
-      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
-    else
-      k stx
-
 @[inherit_doc Mathlib.Linter.linter.minImports]
 def minImportsPost (stx : Syntax) (self : ImportState) : CommandElabM ImportState := do
   -- The reset applies also when the linter option is off. The linter then lints the
@@ -202,7 +182,7 @@ The typed handle of the `minImports` linter. Other stateful linters can read the
 -/
 public initialize minImportsLinter : StatefulLinter ImportState Unit ←
   registerStatefulLinter {}
-    (post := fun stx self _ _ _ => withSetOptionIn' (minImportsPost · self) stx)
+    (post := fun stx self _ _ _ => withSetOptionIn (minImportsPost · self) stx)
 
 end MinImports
 

From e84aa33d80ae7060544bbd1ff1b3471586aa0f7c Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 11 Aug 2026 14:45:57 -0700
Subject: [PATCH 11/13] refactor(Tactic/Linter): use `withSetOptionIn` from
 core

Core's `withSetOptionIn` now has an arbitrary result type
(leanprover/lean4#14581, in v4.34.0-rc1), so it fits the phases of a
stateful linter. The shared polymorphic copy goes away, and the `header`
and `longLine` linters call the core function.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/Header.lean | 22 +---------------------
 Mathlib/Tactic/Linter/Style.lean  |  2 +-
 2 files changed, 2 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index 0a6bb75ef9ac5a..8cc0de3ae61083 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -285,26 +285,6 @@ public structure HeaderState where
   headerSyntax : Syntax := .missing
   deriving Inhabited
 
--- TODO: Upstream? https://github.com/leanprover/lean4/pull/14581
-/--
-`withSetOptionIn' k stx` peels off the `set_option ... in` prefixes of `stx` and applies the
-option values to the current scope. Then it runs `k` on the innermost command.
-The function is a variant of `withSetOptionIn`, with a result type that fits the phases of a
-stateful linter.
--/
-public partial def withSetOptionIn' {α : Type} (k : Syntax → CommandElabM α) :
-    Syntax → CommandElabM α :=
-  fun stx => do
-    if stx.getKind == ``Lean.Parser.Command.in &&
-       stx[0].getKind == ``Lean.Parser.Command.set_option then
-      -- Do not modify the infotrees when elaborating, and silently ignore errors.
-      let opts ← withEnableInfoTree false try
-          (·.1) <$> elabSetOption stx[0][1] stx[0][3]
-        catch _ => getOptions
-      withScope ({ · with opts }) do withSetOptionIn' k stx[2]
-    else
-      k stx
-
 /--
 The "header" style linter checks that a file starts with
 ```
@@ -504,7 +484,7 @@ public initialize headerLinter : StatefulLinter HeaderState Unit ←
   registerStatefulLinter {}
     (post := fun stx self _ _ _ => do
       if self.settled then return self
-      withSetOptionIn' (headerPost · self) stx)
+      withSetOptionIn (headerPost · self) stx)
 
 end Style.header
 
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index 02fbfe3a9fccb6..c0e879471d5a96 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -487,7 +487,7 @@ the `header` linter; its own state is trivial.
 -/
 public initialize longLineLinter : StatefulLinter Unit Unit ←
   registerStatefulLinter ()
-    (post := fun stx _ _ readPrev _ => withSetOptionIn' (longLinePost readPrev) stx)
+    (post := fun stx _ _ readPrev _ => withSetOptionIn (longLinePost readPrev) stx)
 
 end Style.longLine
 

From aa0366f7c09e17adc864f454b8bed1ff518eb683 Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 11 Aug 2026 16:31:24 -0700
Subject: [PATCH 12/13] fix(Tactic/Linter/MinImports): import `Mathlib.Init`
 for the header state

`linter.checkInitImports` requires that a module outside the import closure
of `Mathlib.Init` reaches the `header` linter through `Mathlib.Init`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/MinImports.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index 1f828524a98f38..0c1382e1708f40 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -7,7 +7,9 @@ module
 
 public meta import ImportGraph.Imports.ImportGraph
 public meta import ImportGraph.Graph.TransitiveClosure
-public meta import Mathlib.Tactic.Linter.Header
+-- The `headerLinter` handle comes from `Mathlib.Tactic.Linter.Header`, which `Mathlib.Init`
+-- imports: `linter.checkInitImports` requires the import of `Mathlib.Init` here.
+public meta import Mathlib.Init
 public import Mathlib.Tactic.MinImports
 
 /-! # The `minImports` linter

From 48540ad78d76e6c0ed9350264bc728774354f68a Mon Sep 17 00:00:00 2001
From: Marcelo Lynch <marcelomlynch@gmail.com>
Date: Tue, 1 Sep 2026 21:15:02 -0700
Subject: [PATCH 13/13] refactor(Tactic/Linter/Header): make the new header
 linter implementation stateful

The header linter on master changed with #40347: it now detects the first
command with a fast parse of the imports on every command. This commit
re-applies the stateful refactor on top of that implementation. The state
records the verdict for the module, so every later command skips the
per-command parse. The state replaces the library-root mutex and stores the
parsed header for the minImports and longLine consumers.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 Mathlib/Tactic/Linter/Header.lean             | 70 +++++++++++--------
 Mathlib/Tactic/Linter/MinImports.lean         |  2 +-
 Mathlib/Tactic/Linter/Style.lean              |  2 +-
 .../Linter/Header/MinImportsPayload.lean      | 13 +---
 4 files changed, 44 insertions(+), 43 deletions(-)

diff --git a/Mathlib/Tactic/Linter/Header.lean b/Mathlib/Tactic/Linter/Header.lean
index abd960abeda600..bdd004810816d5 100644
--- a/Mathlib/Tactic/Linter/Header.lean
+++ b/Mathlib/Tactic/Linter/Header.lean
@@ -6,11 +6,9 @@ Authors: Michael Rothgang, Damiano Testa, Thomas R. Murrills
 module
 
 public meta import Lean.Elab.Command
-public meta import Std.Sync.Mutex
 public import Lean.Parser.Module
 public import Mathlib.Tactic.Linter.DirectoryDependency
 public meta import Lean.Linter.Basic
-public import Std.Sync.Mutex
 
 /-!
 # The "header" linter
@@ -43,6 +41,12 @@ The linter checks if it is linting the first command or not by (quickly) parsing
 checking whether the end position of the header is the same as the start position of the current
 command. If so, it re-parses the header more slowly and checks that the current (first) command is
 a module doc-string (unless the command is exempted for some reason).
+
+The linter is a stateful linter (`Lean.Elab.Command.registerStatefulLinter`). Its state records
+a verdict for the module: the header checks ran, or the module is exempt. Every later command
+takes a fast path that does no parsing at all. The state also stores the parsed module header.
+Other linters, such as `minImports` and `longLine`, read the parsed header from the state
+instead of a re-parse of the file.
 -/
 
 meta section
@@ -191,15 +195,16 @@ def isInLibraryRoot (modName : Name) : IO Bool := do
     return res.imports.any (·.module == modName)
   else return false
 
-/-- `inLibraryRootMutex` caches whether the current file is imported in the library root file
-(e.g. `Mathlib.lean`), as computed by `isInLibraryRoot`. It is
-* `none` at initialization time;
-* `some true` if the `header` linter has already discovered that the current file
-  is imported in the library root file;
-* `some false` if the `header` linter has already discovered that the current file
-  is *not* imported in the library root file.
--/
-initialize inLibraryRootMutex : Std.Mutex (Option Bool) ← Std.Mutex.new none
+/-- `HeaderState` is the persistent state of the `header` linter. -/
+public structure HeaderState where
+  /-- `true` after the linter reaches a verdict for the module: the header checks ran, or the
+  module is exempt from the checks. Every later command takes a fast path. -/
+  settled : Bool := false
+  /-- The syntax of the module header: the copyright comment and the `import` commands, with
+  source positions in the current file. The value is `.missing` when the header checks did not
+  run. Other linters read this field to avoid a re-parse of the header. -/
+  headerSyntax : Syntax := .missing
+  deriving Inhabited
 
 /--
 The "header" style linter checks that a file starts with
@@ -284,6 +289,7 @@ def headerTestFiles : NameSet := .ofList [
   `MathlibTest.Linter.Header.Basic,
   `MathlibTest.Linter.Header.Fail,
   `MathlibTest.Linter.Header.Verso,
+  `MathlibTest.Linter.Header.MinImportsPayload,
   `MathlibTest.DirectoryDependencyLinter.Test]
 
 /-- Check the `Syntax` `imports` for broad imports:
@@ -332,47 +338,40 @@ def duplicateImportsCheck (imports : Array ImportRef) : CommandElabM Unit := do
       importsSoFar := importsSoFar.insert imp.toImport
 
 @[inherit_doc Mathlib.Linter.linter.style.header]
-def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
+def headerPost (stx : Syntax) (self : HeaderState) : CommandElabM HeaderState := do
   unless getLinterValue linter.style.header (← getLinterOptions) do
-    return
+    return self
   if (← get).messages.hasErrors then
-    return
+    return self
   let map ← getFileMap
   -- This is essentially the same as calling `parseImports'`, but we need access to `s.pos`.
   let s := ParseImports.main map.source (ParseImports.whitespace map.source {})
   unless (← read).cmdPos == s.pos do
-    return
+    -- Only a command that starts at the end of the header can be the first command of the
+    -- module. Later commands start further down, so the linter has no work left in this module.
+    return { self with settled := true }
   let mainModule ← getMainModule
   if Parser.isTerminalCommand stx ||
     -- Deprecated module files are exempt from all header style checks (copyright, doc-string,
     -- directory dependency, etc.) since they are just import-redirect stubs.
     stx.isOfKind ``Parser.Command.deprecated_module ||
     -- Skip linting the library root file itself.
-    -- In practice, the `inLibraryRoot?` check above already covers this (a well-formed
+    -- In practice, the `isInLibraryRoot` check below already covers this (a well-formed
     -- `<root>.lean` does not import itself), but a root module could appear in `headerTestFiles`.
     mainModule matches .str .anonymous _libroot
-  then return
+  then return { self with settled := true }
   unless stx.isOfKind ``Parser.Command.moduleDoc do
     Linter.logLint linter.style.header stx
       m!"The module doc-string for a file should be the first command after the imports.\n\
         Please, add a module doc-string (`/-! ... -/`) before `{stx}`.\
         {.hint' m!"Type `m(odule docstring) + [tab]` to insert a template via snippet."}"
-  let inLibraryRoot? ← inLibraryRootMutex.atomically do
-    match ← get with
-    | some d => return d
-    | none =>
-      let val ← isInLibraryRoot mainModule
-      -- We cache the answer to avoid recomputing it on every command. The fill runs under the mutex
-      -- so that concurrent (async) linter runs don't all miss the cache and each redundantly parse
-      -- the library root file; `mainModule` is fixed for the duration of the elaboration.
-      set (some val)
-      return val
   -- The linter skips files not imported in their library root (e.g. `Mathlib.lean`), to avoid
   -- linting "scratch files". It is however active in the test files for the linter itself.
-  unless inLibraryRoot? || headerTestFiles.contains mainModule do return
+  unless (← isInLibraryRoot mainModule) || headerTestFiles.contains mainModule do
+    return { self with settled := true }
   -- Re-parse the header slowly, to get the leading whitespace and nice source locations for imports
-  let (headerStx, s, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName))
-  if log.hasErrors then return
+  let (headerStx, _, log) ← Parser.parseHeader (Parser.mkInputContext map.source (← getFileName))
+  if log.hasErrors then return { self with settled := true }
   let importRefs := headerToImportRefs headerStx
   -- Report on broad or duplicate imports.
   broadImportsCheck importRefs mainModule
@@ -389,8 +388,17 @@ def headerLinter : Linter where run := withSetOptionIn fun stx ↦ do
       | _ => ""
     for (stx, m) in copyrightHeaderChecks copyright expectedLicense do
       Linter.logLint linter.style.header stx m!"* `{stx.getAtomVal}`:\n{m}\n"
+  return { self with settled := true, headerSyntax := headerStx.raw }
 
-initialize addLinter headerLinter
+/--
+The typed handle of the `header` linter. Other stateful linters can read the previous
+`HeaderState` of the linter through this handle.
+-/
+public initialize headerLinter : StatefulLinter HeaderState Unit ←
+  registerStatefulLinter {}
+    (post := fun stx self _ _ _ => do
+      if self.settled then return self
+      withSetOptionIn (headerPost · self) stx)
 
 end Style.Header
 
diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index 0c1382e1708f40..e8de7a0cb73434 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -141,7 +141,7 @@ def minImportsPost (readPrev : PrevStateFn) (stx : Syntax) (self : ImportState)
     -- `header` linter provides it when the header checks ran. Otherwise, we read the current
     -- file and do a custom parsing of the imports: this is a hack to obtain some `Syntax`
     -- information for the `import X` commands.
-    let headerStx := (readPrev Style.header.headerLinter).headerSyntax
+    let headerStx := (readPrev Style.Header.headerLinter).headerSyntax
     let impMods ← if headerStx.isMissing then do
         let fname ← getFileName
         let contents ← IO.FS.readFile fname
diff --git a/Mathlib/Tactic/Linter/Style.lean b/Mathlib/Tactic/Linter/Style.lean
index 89975e086d2af4..3b4cf3f9b03a3c 100644
--- a/Mathlib/Tactic/Linter/Style.lean
+++ b/Mathlib/Tactic/Linter/Style.lean
@@ -457,7 +457,7 @@ def longLinePost (readPrev : PrevStateFn) (stx : Syntax) : CommandElabM Unit :=
         -- `impMods` is the syntax for the modules imported in the current file. The state of
         -- the `header` linter provides it when the header checks ran. Otherwise, we parse the
         -- header of the file.
-        let headerStx := (readPrev Style.header.headerLinter).headerSyntax
+        let headerStx := (readPrev Style.Header.headerLinter).headerSyntax
         if headerStx.isMissing then
           let fileMap ← getFileMap
           let (impMods, _) ← Parser.parseHeader
diff --git a/MathlibTest/Linter/Header/MinImportsPayload.lean b/MathlibTest/Linter/Header/MinImportsPayload.lean
index e0b1288578b6be..cfa4d4f4539110 100644
--- a/MathlibTest/Linter/Header/MinImportsPayload.lean
+++ b/MathlibTest/Linter/Header/MinImportsPayload.lean
@@ -6,14 +6,6 @@ Authors: Marcelo Lynch
 import Mathlib.Tactic.Linter.MinImports
 import Mathlib.Data.Int.Notation
 
-/--
-warning: The module doc-string for a file should be the first command after the imports.
-Please, add a module doc-string before `/-!# Tests for the header payload consumers
--/
-`.
-
-Note: This linter can be disabled with `set_option linter.style.header false`
--/
 #guard_msgs in
 set_option linter.style.header true in
 
@@ -24,8 +16,9 @@ set_option linter.style.header true in
 /-! The `header` linter stores the parsed module header in its state. The `minImports` linter
 reads the parsed header for its end-of-file report. The command above enables the `header`
 linter on the module doc-string, so the linter runs its checks and stores the payload. The
-`#exit` command below then triggers the end-of-file report of the `minImports` linter, which
-positions the "unneeded import" warning with the payload. -/
+checks accept this file, so the `#guard_msgs` above expects no message. The `#exit` command
+below then triggers the end-of-file report of the `minImports` linter, which positions the
+"unneeded import" warning with the payload. -/
 
 set_option linter.minImports.increases false