Lean4
@[inherit_doc Mathlib.Linter.linter.directoryDependency]
def directoryDependencyCheck (mainModule : Name) : CommandElabM (Array MessageData) := do
unless Linter.getLinterValue linter.directoryDependency (← getLinterOptions) do
return #[]
let env ← getEnv
let imports := env.allImportedModuleNames
let matchingPrefixes := mainModule.prefixes.filter (fun prf ↦ allowedImportDirs.containsKey prf)
if matchingPrefixes.isEmpty then
-- Otherwise, we fall back to the blocklist `forbiddenImportDirs`.
if let some msg := checkBlocklist env mainModule imports then
return #[msg]
else
return #[]
else
-- We always allow imports in the same directory (for each matching prefix),
-- from `Init`, `Lean` and `Std`, as well as imports in `Aesop`, `Qq`, `Plausible`,
-- `ImportGraph`, `ProofWidgets` or `LeanSearchClient` (as these are imported in Tactic.Common).
-- We also allow transitive imports of Mathlib.Init, as well as Mathlib.Init itself.
let initImports :=
(← findImports ("Mathlib" / "Init.lean")).append #[`Mathlib.Init, `Mathlib.Tactic.DeclarationNames]
let exclude := [`Init, `Std, `Lean, `Aesop, `Qq, `Plausible, `ImportGraph, `ProofWidgets, `LeanSearchClient]
let importsToCheck :=
imports.filter (fun imp ↦ !exclude.any (·.isPrefixOf imp)) |>.filter
(fun imp ↦ !matchingPrefixes.any (·.isPrefixOf imp)) |>.filter
(!initImports.contains ·)
-- Find all prefixes which are allowed for one of these directories.
let allRules := allowedImportDirs.getAllLeft mainModule
let mut messages := #[]
for imported in importsToCheck do
if !allowedImportDirs.contains mainModule imported then
let importPath := env.importPath imported
let mut msg :=
m! "Module {mainModule } depends on {imported},\n\
but is only allowed to import modules starting with one of \
{(allRules.toArray.qsort (·.toString < ·.toString))}.\n\
Note: module {imported}"
let mut superseded := false
match importPath.toList with
| [] =>
msg := msg ++ " is directly imported by this module"
| a :: rest =>
-- Only add messages about imports that aren't themselves transitive imports of
-- forbidden imports.
-- This should prevent redundant messages.
if !allowedImportDirs.contains mainModule a then
superseded := true
else
msg := msg ++ s! " is imported by {a},\n"
for dep in rest do
if !allowedImportDirs.contains mainModule dep then
superseded := true
break
msg := msg ++ m! "which is imported by {dep},\n"
msg := msg ++ m!"which is imported by this module."
msg := msg ++ "(Exceptions can be added to `allowedImportDirs`.)"
if !superseded then
messages := messages.push msg
return messages
