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

def Lean.Name.findPrefix {α : Type u_1} (f : Name → Option α) (n : Name) : Option α

Find the longest prefix of n such that f returns some (or return none otherwise).

def Lean.Name.prefixes (n : Name) : NameSet

Make a NameSet containing all prefixes of n.

def Lean.Name.prefix? (n : Name) : Option Name

Return the immediate prefix of n (if any).

def Lean.Name.collectPrefixes (ns : Array Name) : NameSet

Collect all prefixes of names in ns into a single NameSet.

def Lean.Name.prefixToName (p : Name) (ns : Array Name) : Option Name

Find a name in ns that starts with prefix p.

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.

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

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

def Mathlib.Linter.DirectoryDependency.NamePrefixRel : Type

NamePrefixRel is a datatype for storing relations between name prefixes.

That is, R : NamePrefixRel is supposed to answer given names (n₁, n₂) whether there are any prefixes n₁' of n₁ and n₂' of n₂ such that n₁' R n₂'.

The current implementation is a NameMap of NameSets, testing each prefix of n₁ and n₂ in turn. This can probably be optimized.

instance Mathlib.Linter.DirectoryDependency.NamePrefixRel.instEmptyCollection : EmptyCollection NamePrefixRel

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.insert (r : NamePrefixRel) (n₁ n₂ : Lean.Name) : NamePrefixRel

Make all names with prefix n₁ related to names with prefix n₂.

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.ofArray (xs : Array (Lean.Name × Lean.Name)) : NamePrefixRel

Convert an array of prefix pairs to a NamePrefixRel.

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.find (r : NamePrefixRel) (n₁ n₂ : Lean.Name) : Option (Lean.Name × Lean.Name)

Get a prefix of n₁ that is related to a prefix of n₂.

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.findAny (r : NamePrefixRel) (n₁ : Lean.Name) (ns : Array Lean.Name) : Option (Lean.Name × Lean.Name)

Get a prefix of n₁ that is related to any prefix of the names in ns; return the prefixes.

This should be more efficient than iterating over all names in ns and calling find, since it doesn't need to worry about overlapping prefixes.

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.containsKey (r : NamePrefixRel) (n : Lean.Name) : Bool

Does r contain any entries with key n?

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.contains (r : NamePrefixRel) (n₁ n₂ : Lean.Name) : Bool

Is a prefix of n₁ related to a prefix of n₂?

def Mathlib.Linter.DirectoryDependency.NamePrefixRel.getAllLeft (r : NamePrefixRel) (n : Lean.Name) : Lean.NameSet

Look up all names m which are values of some prefix of n under this relation.

def Mathlib.Linter.DirectoryDependency.allowedImportDirs : NamePrefixRel

allowedImportDirs relates module prefixes, specifying that modules with the first prefix are only allowed to import modules in the second directory. For directories which are low in the import hierarchy, this opt-out approach is both more ergonomic (fewer updates needed) and needs less configuration.

We always allow imports of Init, Lean, Std, Qq and Mathlib.Init (as well as their transitive dependencies.)

def Mathlib.Linter.DirectoryDependency.forbiddenImportDirs : NamePrefixRel

forbiddenImportDirs relates module prefixes, specifying that modules with the first prefix should not import modules with the second prefix (except if specifically allowed in overrideAllowedImportDirs).

For example, (`Mathlib.Algebra.Notation, `Mathlib.Algebra) is in forbiddenImportDirs and (`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation) is in overrideAllowedImportDirs because modules in Mathlib/Algebra/Notation.lean cannot import modules in Mathlib.Algebra that are outside Mathlib/Algebra/Notation.lean.

def Mathlib.Linter.DirectoryDependency.overrideAllowedImportDirs : NamePrefixRel

overrideAllowedImportDirs relates module prefixes, specifying that modules with the first prefix are allowed to import modules with the second prefix, even if disallowed in forbiddenImportDirs.

For example, (`Mathlib.Algebra.Notation, `Mathlib.Algebra) is in forbiddenImportDirs and (`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation) is in overrideAllowedImportDirs because modules in Mathlib/Algebra/Notation.lean cannot import modules in Mathlib.Algebra that are outside Mathlib/Algebra/Notation.lean.

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

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