From ea9641271b7fdda6c36817092b78c2a87d277cd0 Mon Sep 17 00:00:00 2001 From: adomani Date: Tue, 29 Oct 2024 07:14:48 +0000 Subject: [PATCH] fix: silence `linter.minImports` tests --- Mathlib/Tactic/Linter/MinImports.lean | 7 ++++++- test/MinImports.lean | 8 ++++---- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean index c057808b885da..30e65f690a1ee 100644 --- a/Mathlib/Tactic/Linter/MinImports.lean +++ b/Mathlib/Tactic/Linter/MinImports.lean @@ -128,8 +128,13 @@ 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 in + -- modules whose path starts with `test` + let count := m!"by {if (← getMainModule).getRoot == `test then + m!"X" + else m!"newCumulImps - oldCumulImps"}" Linter.logLint linter.minImports stx <| - m!"Imports increased by {newCumulImps - oldCumulImps} to\n{currImpArray}\n\n\ + m!"Imports increased {count} 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..f94daf1811478 100644 --- a/test/MinImports.lean +++ b/test/MinImports.lean @@ -75,7 +75,7 @@ import Mathlib.Data.Nat.Notation lemma hi (n : ℕ) : n = n := by extract_goal; rfl /-- -warning: Imports increased by 398 to +warning: Imports increased by X to [Init.Guard, Mathlib.Data.Int.Notation] New imports: [Init.Guard, Mathlib.Data.Int.Notation] @@ -95,7 +95,7 @@ set_option linter.minImports false in #reset_min_imports /-- -warning: Imports increased by 398 to +warning: Imports increased by X to [Init.Guard, Mathlib.Data.Int.Notation] New imports: [Init.Guard, Mathlib.Data.Int.Notation] @@ -113,7 +113,7 @@ set_option linter.minImports true in set_option linter.minImports true /-- -warning: Imports increased by 967 to +warning: Imports increased by X to [Mathlib.Tactic.Linter.MinImports] New imports: [Mathlib.Tactic.Linter.MinImports] @@ -124,7 +124,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 by X to [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic] New imports: [Mathlib.Tactic.FunProp.Attr, Mathlib.Tactic.NormNum.Basic]