fix(scripts/lint-style): improve Mathlib.Init import error messages (leanprover-community#32419)

Improve the `checkInitImports` linter by:
1. Accepting transitive imports (not just direct) for the `Mathlib.Init` check
2. Removing hardcoded exceptions for transitively imported files
3. Making error messages actionable with specific advice

### Two cases with different advice

1. **Transitively imported by `Mathlib.Init`** → add `import Mathlib.Tactic.Linter.Header`
2. **NOT imported by `Mathlib.Init`** → add `import Mathlib.Init`

### Example output

**Case 1: Transitively imported by Init**
```
  • `Mathlib.Util.SomeFile` is transitively imported by `Mathlib.Init`.
    Please add `import Mathlib.Tactic.Linter.Header` to `Mathlib.Util.SomeFile`.
```

**Case 2: Not imported by Init**
```
  • `Mathlib.Util.TestFile` is NOT imported by `Mathlib.Init`.
    Please add `import Mathlib.Init` to `Mathlib.Util.TestFile`.
```

Prompted by confusion when working on leanprover-community#32416 - the old error message just said files didn't import `Mathlib.Init` without explaining what to do when adding that import would create a cycle.

Discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Mathlib.2EInit.20linter.20error

🤖 Prepared with Claude Code

Author: kim-em

scripts/lint-style.lean

@@ -8,6 +8,7 @@ import Lake.CLI.Main
 import Lean.Elab.ParseImportsFast
 import Batteries.Data.String.Basic
 import Mathlib.Tactic.Linter.TextBased
+import ImportGraph.FromSource
 import Cli.Basic
 
 /-!
@@ -104,38 +105,30 @@ def missingInitImports (opts : LinterOptions) : IO Nat := do
 
   -- Find any file in the Mathlib directory which does not contain any Mathlib import.
   -- We simply parse `Mathlib.lean`, as CI ensures this file is up to date.
-  let allModuleNames := eraseExplicitImports (← findImports "Mathlib.lean")
+  let allModuleNames := eraseExplicitImports (← findImportsFromSource "Mathlib.lean")
   let mut modulesWithoutMathlibImports := #[]
   let mut importsHeaderLinter := #[]
   for module in allModuleNames do
     let path := System.mkFilePath (module.components.map fun n ↦ n.toString)|>.addExtension "lean"
-    let imports ← findImports path
+    let imports ← findImportsFromSource path
     let hasNoMathlibImport := imports.all fun name ↦ name.getRoot != `Mathlib
     if hasNoMathlibImport then
       modulesWithoutMathlibImports := modulesWithoutMathlibImports.push module
     if imports.contains `Mathlib.Tactic.Linter.Header then
       importsHeaderLinter := importsHeaderLinter.push module
 
-  -- Every file importing the `header` linter should be imported in `Mathlib/Init.lean` itself.
+  -- Every file importing the `header` linter should be (transitively) imported by `Mathlib.Init`.
   -- (Downstream files should import `Mathlib.Init` and not the header linter.)
-  -- The only exception are auto-generated import-only files.
-  let initImports ← findImports ("Mathlib" / "Init.lean")
+  -- The only exceptions are auto-generated import-only files.
+  let initTransitiveImports ← findTransitiveImportsFromSource ("Mathlib" / "Init.lean") (some `Mathlib)
   let mismatch := importsHeaderLinter.filter (fun mod ↦
-    ![`Mathlib, `Mathlib.Tactic, `Mathlib.Init].contains mod && !initImports.contains mod)
-    -- These files are transitively imported by `Mathlib.Init`.
-    |>.erase `Mathlib.Tactic.DeclarationNames
-    |>.erase `Mathlib.Lean.Elab.Tactic.Meta
-    |>.erase `Mathlib.Lean.ContextInfo
-    |>.erase `Mathlib.Tactic.Lia
-    |>.erase `Mathlib.Tactic.Linter.DirectoryDependency
-    |>.erase `Mathlib.Lean.Elab.InfoTree
-    |>.erase `Mathlib.Lean.Environment
-    |>.erase `Mathlib.Lean.Expr.Basic
+    ![`Mathlib, `Mathlib.Tactic, `Mathlib.Init].contains mod && !initTransitiveImports.contains mod)
   if mismatch.size > 0 then
     IO.eprintln s!"error: the following {mismatch.size} module(s) import the `header` linter \
-      directly, but should import Mathlib.Init instead: {mismatch}\n\
-      The `header` linter is included in Mathlib.Init, and every file in Mathlib \
-      should import Mathlib.Init.\nPlease adjust the imports accordingly."
+      directly, but should import Mathlib.Init instead: {mismatch}\n"
+    for mod in mismatch do
+      IO.eprintln s!"  • `{mod}` is NOT imported by `Mathlib.Init`.\n    \
+        Please replace `import Mathlib.Tactic.Linter.Header` with `import Mathlib.Init`."
     return mismatch.size
 
   -- Now, it only remains to check that every module (except for the Header linter itself)
@@ -145,7 +138,15 @@ def missingInitImports (opts : LinterOptions) : IO Nat := do
     |>.erase `Mathlib.Tactic.Linter.DirectoryDependency
   if missing.size > 0 then
     IO.eprintln s!"error: the following {missing.size} module(s) do not import Mathlib.Init: \
-      {missing}"
+      {missing}\n"
+    for mod in missing do
+      if initTransitiveImports.contains mod then
+        -- Transitively imported by Init: just needs to import the Header linter
+        IO.eprintln s!"  • `{mod}` is transitively imported by `Mathlib.Init`.\n    \
+          Please add `import Mathlib.Tactic.Linter.Header` to `{mod}`."
+      else
+        IO.eprintln s!"  • `{mod}` is NOT imported by `Mathlib.Init`.\n    \
+          Please add `import Mathlib.Init` to `{mod}`."
     return missing.size
   return 0
 
@@ -240,7 +241,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   let searchPath ← Lean.getSrcSearchPath
   let allModuleNames ← originModules.flatMapM fun mod => do
     let imports ← match ← searchPath.findWithExt "lean" mod with
-    | some file => findImports file
+    | some file => findImportsFromSource file
     | none => throw <| IO.userError s!"could not find module with name {mod}"
     pure <| imports.filter (·.components.head! ∈ pkgs)