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

Equations

• Lean.Name.findPrefix f Lean.Name.anonymous = (f Lean.Name.anonymous <|> none)
• Lean.Name.findPrefix f (n'.str str) = (f (n'.str str) <|> Lean.Name.findPrefix f n')
• Lean.Name.findPrefix f (n'.num i) = (f (n'.num i) <|> Lean.Name.findPrefix f n')

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

Make a NameSet containing all prefixes of n.

Equations

• Lean.Name.anonymous.prefixes = ∅.insert Lean.Name.anonymous
• (n'.str str).prefixes = n'.prefixes.insert (n'.str str)
• (n'.num i).prefixes = n'.prefixes.insert (n'.num i)

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

Return the immediate prefix of n (if any).

Equations

• Lean.Name.anonymous.prefix? = none
• (n'.str str).prefix? = some n'
• (n'.num i).prefix? = some n'

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

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

Equations

• Lean.Name.collectPrefixes ns = Array.foldl (fun (ns : Lean.NameSet) (n : Lean.Name) => Lean.RBTree.union ns n.prefixes) ∅ ns

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

Find a name in ns that starts with prefix p.

Equations

• p.prefixToName ns = Array.find? p.isPrefixOf ns

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

Equations

• Mathlib.Linter.DirectoryDependency.NamePrefixRel = Lean.NameMap Lean.NameSet

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

Equations

• Mathlib.Linter.DirectoryDependency.NamePrefixRel.instEmptyCollection = inferInstanceAs (EmptyCollection (Lean.NameMap Lean.NameSet))

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

Equations

• r.insert n₁ n₂ = match Lean.NameMap.find? r n₁ with | some ns => Lean.NameMap.insert r n₁ (ns.insert n₂) | none => Lean.NameMap.insert r n₁ (∅.insert n₂)

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

Convert an array of prefix pairs to a NamePrefixRel.

Equations

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

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

Equations

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

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.

Equations

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

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

Does r contain any entries with key n?

Equations

• r.containsKey n = Lean.NameMap.contains r 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₂?

Equations

• r.contains n₁ n₂ = (r.find n₁ n₂).isSome

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.

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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