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

Equations

• Lean.instBEqIndirectModUse.beq { kind := a, declName := a_1 } { kind := b, declName := b_1 } = (a == b && a_1 == b_1)
• Lean.instBEqIndirectModUse.beq x✝¹ x✝ = false

instance Lean.instBEqIndirectModUse : BEq IndirectModUse

Equations

• Lean.instBEqIndirectModUse = { beq := Lean.instBEqIndirectModUse.beq }

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

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

Equations

• Lean.getIndirectModUses env modIdx = Lean.PersistentEnvExtension.getModuleEntries Lean.indirectModUseExt env modIdx

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.

Equations

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

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

Equations

• Lean.instBEqExtraModUse.beq { module := a, isExported := a_1, isMeta := a_2 } { module := b, isExported := b_1, isMeta := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.instBEqExtraModUse.beq x✝¹ x✝ = false

instance Lean.instBEqExtraModUse : BEq ExtraModUse

Equations

• Lean.instBEqExtraModUse = { beq := Lean.instBEqExtraModUse.beq }

def Lean.instHashableExtraModUse.hash : ExtraModUse → UInt64

Equations

• Lean.instHashableExtraModUse.hash { module := a, isExported := a_1, isMeta := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

instance Lean.instHashableExtraModUse : Hashable ExtraModUse

Equations

• Lean.instHashableExtraModUse = { hash := Lean.instHashableExtraModUse.hash }

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

Equations

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

instance Lean.instReprExtraModUse : Repr ExtraModUse

Equations

• Lean.instReprExtraModUse = { reprPrec := Lean.instReprExtraModUse.repr }

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

Returns additional recorded import dependencies of the given module.

Equations

• Lean.getExtraModUses env modIdx = Lean.PersistentEnvExtension.getModuleEntries Lean.extraModUses✝ env modIdx

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

Copies additional recorded import dependencies from one environment to another.

Equations

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

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.

Equations

• Lean.recordExtraModUse modName isMeta = do let __do_lift ← Lean.getEnv if (modName != __do_lift.mainModule) = true then Lean.recordExtraModUseCore✝ modName isMeta else pure PUnit.unit

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.

Equations

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

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

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

Equations

• Lean.isExtraRevModUse env modIdx = !(Lean.PersistentEnvExtension.getModuleEntries Lean.isExtraRevModUseExt✝ env modIdx).isEmpty

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.

Equations

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