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.

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
    def Lean.Name.findPrefix {α : Type u_1} (f : NameOption α) (n : Name) :

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

    Equations
    Instances For

      Make a NameSet containing all prefixes of n.

      Equations
      Instances For

        Return the immediate prefix of n (if any).

        Equations
        Instances For

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

          Equations
          Instances For

            Find a name in ns that starts with prefix p.

            Equations
            Instances For

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

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

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

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

                  Equations
                  Instances For

                    Convert an array of prefix pairs to a NamePrefixRel.

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

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

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

                          Does r contain any entries with key n?

                          Equations
                          Instances For

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

                            Equations
                            Instances For

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

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

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

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

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