refactor(Tactic/Linter/MinImports): make the minImports linter stateful

[marcelolynch]

This PR rewrites the minImports linter as a stateful linter (leanprover/lean4#14357). The linter behavior does not change. The existing tests in MathlibTest/MinImports.lean pass without changes. The PR adds one test section that sets Elab.async true explicitly: it checks that the linter accumulates imports correctly under parallel elaboration, and that #import_bumps keeps parallel elaboration on.

The old implementation kept the cumulative imports in a global IO.Ref. The ref is not safe under parallel elaboration. For this reason, #import_bumps set Elab.async false for the rest of the file. The new implementation keeps the same data in the linter state. The elaborator threads the state through the commands of the file, and the data stays correct under parallel elaboration. #import_bumps does not disable Elab.async anymore.

Implementation notes:

• The #reset_min_imports elaborator does nothing. The linter detects the command syntax and clears its own state. The reset works also when the linter option is off, as before.
• The post phase removes set_option ... in prefixes with withSetOptionIn from core. feat: generalize withSetOptionIn to arbitrary result types leanprover/lean4#14581 generalizes the result type of that function, so it accepts the phase of a stateful linter and not only a CommandElab. The generalization ships in v4.34.0-rc1.
• The state type ImportState and the linter handle are public. A follow-up can pass the computed import set to the upstreamableDecl linter, which computes the same data a second time today.

Measurements on synthetic files (Apple Silicon, 18 cores, medians of 3 runs):

• Proof-heavy file (150 commands, about 120 ms each), linter on: 20.0 s before, 8.8 s after. The old version serialized elaboration of the whole file. The new version keeps elaboration parallel and runs the lint chain next to it.
• The old version with Elab.async true emits 123 warning lines instead of the correct 11, because parallel lint tasks race on the ref. The new version emits the correct 11 lines.
• Linter off (2000 trivial commands): the added cost is about 45 microseconds per command.

registerStatefulLinter shipped in v4.34.0-rc1

🤖 Generated with Claude Code

[github-actions]

PR summary 94ebd2a757

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ async_uses_norm_num
+ minImportsPost
- 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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 94ebd2a).

• +18 new declarations
• −1 removed declarations

+Mathlib.Linter.ImportState
+Mathlib.Linter.ImportState.casesOn
+Mathlib.Linter.ImportState.ctorIdx
+Mathlib.Linter.ImportState.importSize
+Mathlib.Linter.ImportState.minImports
+Mathlib.Linter.ImportState.mk
+Mathlib.Linter.ImportState.mk.inj
+Mathlib.Linter.ImportState.mk.injEq
+Mathlib.Linter.ImportState.mk.noConfusion
+Mathlib.Linter.ImportState.mk.sizeOf_spec
+Mathlib.Linter.ImportState.noConfusion
+Mathlib.Linter.ImportState.noConfusionType
+Mathlib.Linter.ImportState.rec
+Mathlib.Linter.ImportState.recOn
+Mathlib.Linter.ImportState.transClosure
+Mathlib.Linter.MinImports.minImportsLinter
+Mathlib.Linter.instInhabitedImportState
+Mathlib.Linter.resetMinImports
-Mathlib.Linter.«command#reset_min_imports»

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 94ebd2a757
Reference commit 37252fbc4b

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.py 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).

[JovanGerb]

I never know what to think of linter that are implemented in mathlib but are not actually active in mathlib. I would think that they (or at least some of them) are used so rarely that they might as well be deprecated.

@thorimur, since you are working on the #min_imports command, what do you think is the role of the minImports linter?

[thorimur]

I think the minImports linter is soon to be revamped to use the new infrastructure! 😁 Therefore I think it makes sense to hold off on statefulifying it for now. (I'm also a little reluctant to put any stateful linters in mathlib just yet in case they become more featureful in the near future and the API changes.)

I should mention the #min_imports command revamp in leanprover-community/import-graph#168 for completeness, which will then hopefully enable a revamp of the linter. :) (Actually, it's possible we might be able to revamp it before that lands, but it's a careful revamp either way.)