Documentation

Mathlib.Tactic.Linter.DirectoryDependency

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.

source
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.
Instances For
    source
    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.

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

    Runs the directoryDependency linter on the current module, assuming that it is called mainModule. Detects imports between directories that are supposed to be independent. If this is the case, it emits a warning.

    Note: we look in srcDir for scripts/forbiddenDirs.json and, if in mathlib, for Mathlib.Init. srcDir is thus typically expected to be the package directory (e.g. {path}/mathlib4).

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