From 37280a98387504d7adf48c85a756ba68a85f347a Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Tue, 28 Jul 2026 10:41:17 -0300 Subject: [PATCH 1/5] 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 --- 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 Date: Tue, 28 Jul 2026 11:07:59 -0300 Subject: [PATCH 2/5] 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 --- 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 Date: Tue, 28 Jul 2026 11:11:17 -0300 Subject: [PATCH 3/5] doc(Tactic/Linter/MinImports): link the upstreaming PR for withSetOptionIn' Co-Authored-By: Claude Fable 5 --- 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 Date: Tue, 28 Jul 2026 11:41:18 -0300 Subject: [PATCH 4/5] doc(Tactic/Linter/MinImports): note possible reset semantics for #import_bumps Co-Authored-By: Claude Fable 5 --- 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 a2fe02186deb5ae53207ae318b8611b1fdc448cb Mon Sep 17 00:00:00 2001 From: Marcelo Lynch Date: Tue, 11 Aug 2026 14:27:52 -0700 Subject: [PATCH 5/5] 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) --- 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