Lean4
/-- `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.)
-/
def allowedImportDirs : NamePrefixRel :=
.ofArray
#[
-- This is used to test the linter.
(`MathlibTest.DirectoryDependencyLinter, `Mathlib.Lean),
-- Mathlib.Tactic has large transitive imports: just allow all of mathlib,
-- as we don't care about the details a lot.
(`MathlibTest.Header, `Mathlib), (`MathlibTest.Header, `Aesop), (`MathlibTest.Header, `ImportGraph),
(`MathlibTest.Header, `LeanSearchClient), (`MathlibTest.Header, `Plausible), (`MathlibTest.Header, `ProofWidgets),
(`MathlibTest.Header, `Qq),
-- (`MathlibTest.Header, `Mathlib.Tactic),
-- (`MathlibTest.Header, `Mathlib.Deprecated),
(`MathlibTest.Header, `Batteries), (`MathlibTest.Header, `Lake), (`Mathlib.Util, `Batteries),
(`Mathlib.Util, `Mathlib.Lean), (`Mathlib.Util, `Mathlib.Tactic),
-- TODO: reduce this dependency by upstreaming `Data.String.Defs to batteries
(`Mathlib.Util.FormatTable, `Mathlib.Data.String.Defs), (`Mathlib.Lean, `Batteries.Tactic.Lint),
(`Mathlib.Lean, `Batteries.CodeAction),
-- TODO: should this be minimised further?
(`Mathlib.Lean.Meta.CongrTheorems, `Batteries),
-- These modules are transitively imported by `Batteries.CodeAction.
(`Mathlib.Lean, `Batteries.Classes.SatisfiesM), (`Mathlib.Lean, `Batteries.Data.Array.Match),
(`Mathlib.Lean, `Batteries.Data.Fin), (`Mathlib.Lean, `Batteries.Data.List), (`Mathlib.Lean, `Batteries.Lean),
(`Mathlib.Lean, `Batteries.Control.ForInStep), (`Mathlib.Lean, `Batteries.Tactic.Alias),
(`Mathlib.Lean, `Batteries.Util.ProofWanted), (`Mathlib.Lean.Expr, `Mathlib.Util),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Util),
-- Fine-grained exceptions: TODO decide if these are fine, or should be scoped more broadly.
(`Mathlib.Lean.CoreM, `Mathlib.Tactic.ToExpr), (`Mathlib.Lean.CoreM, `Mathlib.Util.WhatsNew),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic.Lemma),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic.TypeStar),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic.ToAdditive),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Tactic), -- split this up further?
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Data), -- split this up further?
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Algebra.Notation),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Data.Notation),
(`Mathlib.Lean.Meta.RefinedDiscrTree, `Mathlib.Data.Array), (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Data),
(`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Logic), (`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Order.Defs),
(`Mathlib.Lean.Meta.CongrTheorems, `Mathlib.Tactic),
(`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Util.ExtendedBinder),
(`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Logic),
(`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Tactic.Trans),
(`Mathlib.Lean.Expr.ExtraRecognizers, `Batteries.Tactic.Init),
(`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Data), (`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Order),
(`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Logic), (`Mathlib.Lean.Expr.ExtraRecognizers, `Mathlib.Tactic),
(`Mathlib.Tactic.Linter, `Batteries),
-- The Mathlib.Tactic.Linter *module* imports all linters, hence requires all the imports.
-- For more fine-grained exceptions of the next two imports, one needs to rename that file.
(`Mathlib.Tactic.Linter, `ImportGraph), (`Mathlib.Tactic.Linter, `Mathlib.Tactic.MinImports),
(`Mathlib.Tactic.Linter.TextBased, `Mathlib.Data.Nat.Notation), (`Mathlib.Logic, `Batteries),
-- TODO: should the next import direction be flipped?
(`Mathlib.Logic, `Mathlib.Control), (`Mathlib.Logic, `Mathlib.Lean), (`Mathlib.Logic, `Mathlib.Util),
(`Mathlib.Logic, `Mathlib.Tactic), (`Mathlib.Logic.Fin.Rotate, `Mathlib.Algebra.Group.Fin.Basic),
(`Mathlib.Logic, `Mathlib.Algebra.Notation), (`Mathlib.Logic, `Mathlib.Algebra.NeZero),
(`Mathlib.Logic, `Mathlib.Data),
-- TODO: this next dependency should be made more fine-grained.
(`Mathlib.Logic, `Mathlib.Order),
-- Particular modules with larger imports.
(`Mathlib.Logic.Hydra, `Mathlib.GroupTheory), (`Mathlib.Logic.Hydra, `Mathlib.Algebra),
(`Mathlib.Logic.Encodable.Pi, `Mathlib.Algebra), (`Mathlib.Logic.Equiv.Fin.Rotate, `Mathlib.Algebra.Group),
(`Mathlib.Logic.Equiv.Fin.Rotate, `Mathlib.Algebra.Regular), (`Mathlib.Logic.Equiv.Array, `Mathlib.Algebra),
(`Mathlib.Logic.Equiv.Finset, `Mathlib.Algebra), (`Mathlib.Logic.Godel.GodelBetaFunction, `Mathlib.Algebra),
(`Mathlib.Logic.Small.List, `Mathlib.Algebra), (`Mathlib.Testing, `Batteries),
-- TODO: this next import should be eliminated.
(`Mathlib.Testing, `Mathlib.GroupTheory), (`Mathlib.Testing, `Mathlib.Control),
(`Mathlib.Testing, `Mathlib.Algebra), (`Mathlib.Testing, `Mathlib.Data), (`Mathlib.Testing, `Mathlib.Logic),
(`Mathlib.Testing, `Mathlib.Order), (`Mathlib.Testing, `Mathlib.Lean), (`Mathlib.Testing, `Mathlib.Tactic),
(`Mathlib.Testing, `Mathlib.Util), ]
