[Merged by Bors] - chore: update Mathlib dependencies 2026-09-13

lake-manifest.json

@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1681d78dd6e65e38b143f9740d829c826673807c",
+   "rev": "14f0afd1c8448a1159d7b02e1c6b6db3787c62c8",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

scripts/lint-style.lean

@@ -11,6 +11,8 @@ import Mathlib.Tactic.Linter.TextBased
 import ImportGraph.Imports.FromSource
 import Cli.Basic
 
+open ImportGraph
+
 /-!
 # Text-based style linters
 
@@ -105,12 +107,13 @@ 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 (← findImportsFromSource "Mathlib.lean")
+  let mathlibHeader ← ("Mathlib.lean" : System.FilePath).parseImports'
+  let allModuleNames := eraseExplicitImports (mathlibHeader.filterInit.imports.map (·.module))
   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 ← findImportsFromSource path
+    let imports := (← path.parseImports').filterInit.imports.map (·.module)
     let hasNoMathlibImport := imports.all fun name ↦ name.getRoot != `Mathlib
     if hasNoMathlibImport then
       modulesWithoutMathlibImports := modulesWithoutMathlibImports.push module
@@ -248,9 +251,9 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
   Lean.initSearchPath (← Lean.findSysroot)
   let searchPath ← Lean.getSrcSearchPath
   let allModuleNames ← originModules.flatMapM fun mod => do
-    let imports ← match ← searchPath.findWithExt "lean" mod with
-    | some file => findImportsFromSource file
-    | none => throw <| IO.userError s!"could not find module with name {mod}"
+    let some file ← searchPath.findWithExt "lean" mod
+      | throw <| IO.userError s!"could not find module with name {mod}"
+    let imports := (← file.parseImports').filterInit.imports.map (·.module)
     pure <| imports.filter (·.components.head! ∈ pkgs)
 
   -- Read the `nolints` file, with manual exceptions for the linter.