diff --git a/lake-manifest.json b/lake-manifest.json index 4cc8c0454c82e0..c399190da20900 100644 --- a/lake-manifest.json +++ b/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", diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 693913299410b9..58e7111528be16 100644 --- a/scripts/lint-style.lean +++ b/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.