The directoryDependency linter

The directoryDependency linter detects imports between directories that are supposed to be independent. By specifying that one directory does not import from another, we can improve the modularity of Mathlib.

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

Parse all imports in a text file at path and return just their names: this is just a thin wrapper around Lean.parseImports'. Omit Init (which is part of the prelude).

Equations

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

def Lean.Environment.importPath (env : Environment) (imported : Name) : Array Name

Find the dependency chain, starting at a module that imports imported, and ends with the current module.

The path only contains the intermediate steps: it excludes imported and the current module.

Equations

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

opaque Mathlib.Linter.linter.directoryDependency : Lean.Option Bool

The directoryDependency linter detects imports between directories that are supposed to be independent. If this is the case, it emits a warning.

def Mathlib.Linter.directoryDependencyCheck (mainModule : Lean.Name) : Lean.Elab.Command.CommandElabM (Array Lean.MessageData)

The directoryDependency linter detects imports between directories that are supposed to be independent. If this is the case, it emits a warning.

Equations

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