allowedImportDirs

Stream: mathlib4

[Kim Morrison]

@Anne Baanen, could you give me a quick tutorial sometime on how to use the DirectoryDependency linter?

On my hammer branch on my kim-em fork, I'm getting messages:

warning: Mathlib/Logic/Encodable/Pi.lean:9:0: Module Mathlib.Logic.Encodable.Pi depends on Hammer,
but is only allowed to import modules starting with one of [Batteries,
 Mathlib.Algebra,
 Mathlib.Algebra.NeZero,
 Mathlib.Algebra.Notation,
 Mathlib.Control,
 Mathlib.Data,
 Mathlib.Lean,
 Mathlib.Order,
 Mathlib.Tactic,
 Mathlib.Util].
Note: module Hammer is imported by Mathlib.Tactic.Common,
which is imported by Mathlib.Data.Vector.Defs,
which is imported by Mathlib.Data.Vector.Basic,
which is imported by this module.(Exceptions can be added to `allowedImportDirs`.)
note: this linter can be disabled with `set_option linter.directoryDependency false`

but looking at the definition of allowedImportDirs I'm not sure what change I should make to achieve the desired effect (everything is allowed to import Hammer!).

[Anne Baanen]

If you want to disable all checks involving imports of Hammer, you can add it to the let exclude list in directoryDependencyCheck:

    let exclude := [
      `Init, `Std, `Lean,
      `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient, `Hammer,
    ]

To be more specific and allow importing Hammer from Mathlib.Logic (but not necessarily elsewhere), you can add Mathlib.Logic paired with Hammer to the allowedImportDirs:

def allowedImportDirs : NamePrefixRel := .ofArray #[
  -- Any file in the directory `Mathlib.Logic` is allowed to import `Hammer`.
  (`Mathlib.Logic, `Hammer),
  ...,
]