Skip to content

Commit

Permalink
fix: silence linter.minImports tests (#18372)
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Oct 29, 2024
1 parent 33d49bb commit fc4e227
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 5 deletions.
17 changes: 16 additions & 1 deletion Mathlib/Tactic/Linter/MinImports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,15 @@ register_option linter.minImports : Bool := {
descr := "enable the minImports linter"
}

/-- The `linter.minImports.increases` regulates whether the `minImports` linter reports the
change in number of imports, when it reports import changes.
Setting this option to `false` helps with test stability.
-/
register_option linter.minImports.increases : Bool := {
defValue := true
descr := "enable reporting increase-size change in the minImports linter"
}

namespace MinImports

open Mathlib.Command.MinImports
Expand Down Expand Up @@ -128,8 +137,14 @@ def minImportsLinter : Linter where run := withSetOptionIn fun stx ↦ do
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 Linter.getLinterValue linter.minImports.increases (← getOptions) then
m!"by {newCumulImps - oldCumulImps} "
else
m!""
Linter.logLint linter.minImports stx <|
m!"Imports increased by {newCumulImps - oldCumulImps} to\n{currImpArray}\n\n\
m!"Imports increased {byCount}to\n{currImpArray}\n\n\
New imports: {new}\n" ++
if redundant.isEmpty then m!"" else m!"\nNow redundant: {redundant}\n"

Expand Down
9 changes: 5 additions & 4 deletions test/MinImports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -74,8 +74,9 @@ import Mathlib.Data.Nat.Notation
#min_imports in
lemma hi (n : ℕ) : n = n := by extract_goal; rfl

set_option linter.minImports.increases false
/--
warning: Imports increased by 398 to
warning: Imports increased to
[Init.Guard, Mathlib.Data.Int.Notation]
New imports: [Init.Guard, Mathlib.Data.Int.Notation]
Expand All @@ -95,7 +96,7 @@ set_option linter.minImports false in
#reset_min_imports

/--
warning: Imports increased by 398 to
warning: Imports increased to
[Init.Guard, Mathlib.Data.Int.Notation]
New imports: [Init.Guard, Mathlib.Data.Int.Notation]
Expand All @@ -113,7 +114,7 @@ set_option linter.minImports true in
set_option linter.minImports true

/--
warning: Imports increased by 967 to
warning: Imports increased to
[Mathlib.Tactic.Linter.MinImports]
New imports: [Mathlib.Tactic.Linter.MinImports]
Expand All @@ -124,7 +125,7 @@ note: this linter can be disabled with `set_option linter.minImports false`
#reset_min_imports

/--
warning: Imports increased by 424 to
warning: Imports increased to
[Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic]
New imports: [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic]
Expand Down

0 comments on commit fc4e227

Please sign in to comment.