Commit 2024-07-23 04:33 b8215992

feat: the minImports linter (#14840) Introducing the "linter form" of #min_imports in. The linter is called linter.minImports and flags every command that increases the imports-so-far in the file. When it reaches the end of the file, it also reports which current imports are unneeded and which imports are missing to minimize the current imports. Here is an example.

import Mathlib.Tactic.Linter.MinImports
-- `import Mathlib.Data.Int.Notation` flagged as missing
import Mathlib.Data.Nat.Notation   -- flagged as unneeded
import Mathlib.Data.Int.Defs       -- flagged as unneeded
-- Imports increased to [Lean.Parser.Command]
set_option linter.minImports true
-- Imports increased to [Mathlib.Tactic.Linter.MinImports]
#reset_min_imports
-- Imports increased to [Mathlib.Data.Int.Notation, Mathlib.Tactic.Linter.MinImports]
#guard (0 : ℤ) = 0

Test PR at #14839.