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).

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.