From fc4e2273f77a8cdaa61db349b331c6a6fc138e55 Mon Sep 17 00:00:00 2001
From: damiano <adomani@gmail.com>
Date: Tue, 29 Oct 2024 14:36:05 +0000
Subject: [PATCH] fix: silence `linter.minImports` tests (#18372)

Reported on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/.2318333.20adaptations.20for.20nightly-2024-10-28)
---
 Mathlib/Tactic/Linter/MinImports.lean | 17 ++++++++++++++++-
 test/MinImports.lean                  |  9 +++++----
 2 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
index c057808b885da..0aad206e77cf8 100644
--- a/Mathlib/Tactic/Linter/MinImports.lean
+++ b/Mathlib/Tactic/Linter/MinImports.lean
@@ -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
@@ -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"
 
diff --git a/test/MinImports.lean b/test/MinImports.lean
index 49f838a69d1af..dc2abd0c1421a 100644
--- a/test/MinImports.lean
+++ b/test/MinImports.lean
@@ -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]
@@ -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]
@@ -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]
@@ -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]