Source-File-Based Import Analysis

This module provides functions for analyzing imports by parsing source files directly, as an alternative to Environment-based analysis (e.g. in ImportGraph.Imports). Specifically:

• parseImports?, System.FilePath.parseImports': Parse direct imports from a single string or file
• Lean.ModuleHeader.filterInit: Remove Init imports from a parsed header
• parseCurrentHeader: parse the imports of the current file from the FileMap
• modToRelFilePath: like modToFilePath, but does not insert a leading file separator
• findTransitiveImportsFromSource: Compute a nameset of the transitive closure of imports from source files. Note, however, that this does not respect the module system.

def ImportGraph.parseImports? (input : String) : Except (Lean.FileMap × Lean.Position × String) Lean.ModuleHeader

Like parseImports', but pure. Instead of returning the fileName:pos <msg> error of parseImports' of parseImports', returns (fileMap, pos, <msg>).

Equations

• One or more equations did not get rendered due to their size.

def ImportGraph.System.FilePath.parseImports' (path : System.FilePath) : IO Lean.ModuleHeader

Parse the header of the source file at path, returning its ModuleHeader.

This is a thin wrapper around Lean.parseImports' which:

• Reads the file from disk
• Parses the import statements

Note that it does not filter out Init modules. See ModuleHeader.filterInit.

Equations

• ImportGraph.System.FilePath.parseImports' path = do let __do_lift ← IO.FS.readFile path Lean.parseImports' __do_lift path.toString

def ImportGraph.Lean.ModuleHeader.filterInit (m : Lean.ModuleHeader) : Lean.ModuleHeader

Removes every import in the Init namespace (Init itself and Init.*) from a ModuleHeader.

Equations

• ImportGraph.Lean.ModuleHeader.filterInit m = { imports := Array.filter (fun (imp : Lean.Import) => !`Init.isPrefixOf imp.module) m.imports, isModule := m.isModule }

def ImportGraph.parseCurrentHeader {m : Type → Type} [Monad m] [Lean.MonadLog m] [MonadLiftT IO m] : m (Lean.TSyntax `Lean.Parser.Module.header × Lean.Parser.ModuleParserState × Lean.MessageLog)

Parses the header of the current file via the source string present in the ambient FileMap.

Equations

• One or more equations did not get rendered due to their size.

@[deprecated "Use `ImportGraph.System.FilePath.parseImports'` and `ImportGraph.Lean.ModuleHeader.filterInit` instead" (since := "2026-09-13")]

def ImportGraph.findImportsFromSource (path : System.FilePath) : IO (Array Lean.Name)

Parse all imports in a source file at path and return their module names.

This is a thin wrapper around Lean.parseImports' that:

• Reads the file from disk
• Parses the import statements
• Filters out Init (part of the prelude)

Note: This only sees syntactic imports in the source file. It does not account for what declarations are actually used.

Equations

• One or more equations did not get rendered due to their size.

def ImportGraph.modToRelFilePath (mod : Lean.Name) (ext : String) : System.FilePath

Like modToFilePath, but does not demand base. Example: modToRelFilePath A.B.C "lean" results in A/B/C.lean. (Note that modToFilePath "" mod ext inserts a leading file separator, and would result in /A/B/C.lean.)

Equations

• ImportGraph.modToRelFilePath mod ext = (ImportGraph.modToRelFilePath.go✝ mod).addExtension ext

def ImportGraph.findTransitiveImportsFromSource (startPath : System.FilePath) (rootFilter : Option Lean.Name := none) : IO Lean.NameSet

Compute the transitive closure of imports starting from a source file.

Returns a NameSet of all modules that are transitively imported by the given file, by recursively parsing source files.

Example:

-- Get all transitive Mathlib imports
let imports ← findTransitiveImportsFromSource "Mathlib/Algebra/Ring/Basic.lean" (some `Mathlib)

-- Get all transitive imports regardless of namespace
let allImports ← findTransitiveImportsFromSource "MyFile.lean"

Equations

• One or more equations did not get rendered due to their size.