Infrastructure for recording extra import dependencies not implied by the environment constants for the benefit of shake.

structure Lean.IndirectModUse : Type

• kind : String
• declName : Name

def Lean.instBEqIndirectModUse.beq : IndirectModUse → IndirectModUse → Bool

@[implicit_reducible]

instance Lean.instBEqIndirectModUse : BEq IndirectModUse

opaque Lean.indirectModUseExt : SimplePersistentEnvExtension IndirectModUse (Std.HashMap Name (Array ModuleIdx))

def Lean.getIndirectModUses (env : Environment) (modIdx : ModuleIdx) : Array IndirectModUse

def Lean.recordIndirectModUse {m : Type → Type} [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m] (kind : String) (declName : Name) : m Unit

Lets shake know that references to declName may also require importing the current module due to some additional metaprogramming dependency expressed by kind. Currently this is always the name of an attribute applied to declName, which is not from the current module, in the current module. kind is not currently used to further filter what references to declName require importing the current module but may in the future.

structure Lean.ExtraModUse : Type

Additional import dependency for elaboration.

• module : Name

  Dependency's module name.

• isExported : Bool

  Whether dependency must be imported as public.

• isMeta : Bool

  Whether dependency must be imported as meta.

def Lean.instBEqExtraModUse.beq : ExtraModUse → ExtraModUse → Bool

@[implicit_reducible]

instance Lean.instBEqExtraModUse : BEq ExtraModUse

def Lean.instHashableExtraModUse.hash : ExtraModUse → UInt64

@[implicit_reducible]

instance Lean.instHashableExtraModUse : Hashable ExtraModUse

def Lean.instReprExtraModUse.repr : ExtraModUse → Nat → Format

@[implicit_reducible]

instance Lean.instReprExtraModUse : Repr ExtraModUse

def Lean.getExtraModUses (env : Environment) (modIdx : ModuleIdx) : Array ExtraModUse

Returns additional recorded import dependencies of the given module.

def Lean.copyExtraModUses (src dest : Environment) : Environment

Copies additional recorded import dependencies from one environment to another.

def Lean.recordExtraModUse {m : Type → Type} [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m] (modName : Name) (isMeta : Bool) : m Unit

Records an additional import dependency for the current module, using Environment.isExporting as the visibility level.

NOTE: Directly recording a module name does not trigger including indirect dependencies recorded via recordIndirectModUse, prefer recordExtraModUseFromDecl instead.

def Lean.recordExtraModUseFromDecl {m : Type → Type} [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m] (declName : Name) (isMeta : Bool) : m Unit

Records the module of the given declaration as an additional import dependency for the current module, using Environment.isExporting as the visibility level. If the declaration itself is already meta, the module dependency is recorded as a non-meta dependency.

def Lean.isExtraRevModUse (env : Environment) (modIdx : ModuleIdx) : Bool

Checks whether this module should be preserved as an import by shake.

def Lean.recordExtraRevUseOfCurrentModule {m : Type → Type} [Monad m] [MonadEnv m] [MonadTrace m] [MonadOptions m] [MonadRef m] [AddMessageContext m] : m Unit

Records this module to be preserved as an import by shake.