Shake extension API

This module provides basic API wrappers and boilerplate for shake extensions. This is mainly for readability, to ensure that the correct aspects of the state are being managed: different extensions use different parts of the state for specific purposes.

In particular, it provides withFreshShakeRecords for running an action after resetting the shake extension state, allowing for capture of what mod uses that action produced.

def ImportGraph.Shake.instReprIndirectModUse_importGraph.repr : Lean.IndirectModUse → Nat → Std.Format

Equations

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

@[instance_reducible]

instance ImportGraph.Shake.instReprIndirectModUse_importGraph : Repr Lean.IndirectModUse

Equations

• ImportGraph.Shake.instReprIndirectModUse_importGraph = { reprPrec := ImportGraph.Shake.instReprIndirectModUse_importGraph.repr }

@[instance_reducible]

instance ImportGraph.Shake.instHashableIndirectModUse_importGraph : Hashable Lean.IndirectModUse

Equations

• ImportGraph.Shake.instHashableIndirectModUse_importGraph = { hash := ImportGraph.Shake.instHashableIndirectModUse_importGraph.hash }

def ImportGraph.Shake.instHashableIndirectModUse_importGraph.hash : Lean.IndirectModUse → UInt64

Equations

• ImportGraph.Shake.instHashableIndirectModUse_importGraph.hash { kind := a, declName := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

def ImportGraph.Shake.instOrdIndirectModUse_importGraph.ord : Lean.IndirectModUse → Lean.IndirectModUse → Ordering

Equations

• ImportGraph.Shake.instOrdIndirectModUse_importGraph.ord { kind := a, declName := a_1 } { kind := b, declName := b_1 } = (compare a b).then ((compare a_1 b_1).then Ordering.eq)

@[instance_reducible]

instance ImportGraph.Shake.instOrdIndirectModUse_importGraph : Ord Lean.IndirectModUse

Equations

• ImportGraph.Shake.instOrdIndirectModUse_importGraph = { compare := ImportGraph.Shake.instOrdIndirectModUse_importGraph.ord }

@[inline]

def ImportGraph.Shake.resetNewIndirectModUses (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.indirectModUseExt.toEnvExtension.asyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Resets the new entries in the indirectModUse extension. Note that the state is never altered in the course of the file, as it only represents imported entries. Only the entries are gotten/ reset.

Equations

• ImportGraph.Shake.resetNewIndirectModUses env asyncMode asyncDecl = Lean.SimplePersistentEnvExtension.setEntries env Lean.indirectModUseExt [] asyncMode asyncDecl

@[inline]

def ImportGraph.Shake.getNewIndirectModUses (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.indirectModUseExt.toEnvExtension.asyncMode) : List Lean.IndirectModUse

Equations

• ImportGraph.Shake.getNewIndirectModUses env asyncMode = Lean.indirectModUseExt.getEntries env asyncMode

@[inline]

def ImportGraph.Shake.setNewIndirectModUses (env : Lean.Environment) (entries : List Lean.IndirectModUse) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.indirectModUseExt.toEnvExtension.asyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Equations

• ImportGraph.Shake.setNewIndirectModUses env entries asyncMode asyncDecl = Lean.SimplePersistentEnvExtension.setEntries env Lean.indirectModUseExt entries asyncMode asyncDecl

def ImportGraph.Shake.getResetNewIndirectModUses (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.indirectModUseExt.toEnvExtension.asyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : List Lean.IndirectModUse × Lean.Environment

Gets and resets the new indirect mod uses recorded in the indirectModUse extension. Note that the state per se is never altered in the course of the file, as it only represents imported entries. Only the entries list is gotten/reset.

Equations

• ImportGraph.Shake.getResetNewIndirectModUses env asyncMode asyncDecl = (Lean.indirectModUseExt.getEntries env asyncMode, ImportGraph.Shake.resetNewIndirectModUses env asyncMode asyncDecl)

@[inline]

def ImportGraph.Shake.extraModUsesAsyncMode : Lean.EnvExtension.AsyncMode

A wrapper for extraModUses.toEnvExtension.asyncMode to allow it to appear as an optParam in a public-facing type.

Equations

• ImportGraph.Shake.extraModUsesAsyncMode = Lean.extraModUses✝.toEnvExtension.asyncMode

@[inline]

def ImportGraph.Shake.resetNewExtraModUses (env : Lean.Environment) : Lean.Environment

Equations

• ImportGraph.Shake.resetNewExtraModUses env = Lean.PersistentEnvExtension.setState Lean.extraModUses✝ env ([], ∅)

@[inline]

def ImportGraph.Shake.getNewExtraModUses (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := extraModUsesAsyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : List Lean.ExtraModUse × Lean.PHashSet Lean.ExtraModUse

Equations

• ImportGraph.Shake.getNewExtraModUses env asyncMode asyncDecl = Lean.PersistentEnvExtension.getState Lean.extraModUses✝ env asyncMode asyncDecl

@[inline]

def ImportGraph.Shake.setNewExtraModUses (env : Lean.Environment) (entries : List Lean.ExtraModUse) (state : Lean.PHashSet Lean.ExtraModUse) : Lean.Environment

Equations

• ImportGraph.Shake.setNewExtraModUses env entries state = Lean.PersistentEnvExtension.setState Lean.extraModUses✝ env (entries, state)

def ImportGraph.Shake.getResetExtraModUses (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := extraModUsesAsyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : (List Lean.ExtraModUse × Lean.PHashSet Lean.ExtraModUse) × Lean.Environment

Gets and resets the new extra mod uses in the extraModUses extension. Note that the state does not include imported entries.

Equations

• ImportGraph.Shake.getResetExtraModUses env asyncMode asyncDecl = (ImportGraph.Shake.getNewExtraModUses env asyncMode asyncDecl, ImportGraph.Shake.resetNewExtraModUses env)

@[inline]

def ImportGraph.Shake.isExtraRevModUseExtAsyncMode : Lean.EnvExtension.AsyncMode

A wrapper for isExtraRevModUseExt.toEnvExtension.asyncMode to allow it to appear as an optParam in a public-facing type.

Equations

• ImportGraph.Shake.isExtraRevModUseExtAsyncMode = Lean.isExtraRevModUseExt✝.toEnvExtension.asyncMode

@[inline]

def ImportGraph.Shake.getNewExtraRevModUse (env : Lean.Environment) : Bool

Gets the state of the extraModUses extension.

Equations

• ImportGraph.Shake.getNewExtraRevModUse env = !(Lean.isExtraRevModUseExt✝.getEntries env).isEmpty

@[inline]

def ImportGraph.Shake.resetNewExtraRevModUse (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := isExtraRevModUseExtAsyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Resets the state of the extraModUses extension.

Equations

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

@[inline]

def ImportGraph.Shake.setNewExtraRevModUse (env : Lean.Environment) (isRev : Bool) (asyncMode : Lean.EnvExtension.AsyncMode := isExtraRevModUseExtAsyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Resets the state of the extraModUses extension.

Equations

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

@[inline]

def ImportGraph.Shake.mergeNewExtraRevModUse (env : Lean.Environment) (old : Bool) (asyncMode : Lean.EnvExtension.AsyncMode := isExtraRevModUseExtAsyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Merges the state of the extraModUses extension (using "or" semantics).

Equations

• ImportGraph.Shake.mergeNewExtraRevModUse env old asyncMode asyncDecl = if old = true then ImportGraph.Shake.setNewExtraRevModUse env old asyncMode asyncDecl else env

def ImportGraph.Shake.getResetNewExtraRevModUse (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := isExtraRevModUseExtAsyncMode) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Bool × Lean.Environment

Gets and resets the state of the extraModUses extension.

Equations

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

def ImportGraph.Shake.resetShakeRecords (env : Lean.Environment) (asyncMode : Lean.EnvExtension.AsyncMode := Lean.EnvExtension.AsyncMode.sync) (asyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Erases any new shake records from the current module.

Equations

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

def ImportGraph.Shake.copyExtraModUses (src dest : Lean.Environment) (srcAsyncMode destAsyncMode : Lean.EnvExtension.AsyncMode := extraModUsesAsyncMode) (destAsyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Copies new extra mod uses from src and adds them to dest. Does not erase extra mod uses already in dest. The same as Lean.copyExtraModUses, but passes async modes.

Equations

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

def ImportGraph.Shake.copyIndirectModUses (src dest : Lean.Environment) (srcAsyncMode destAsyncMode : Lean.EnvExtension.AsyncMode := Lean.indirectModUseExt.toEnvExtension.asyncMode) (destAsyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Copies new indirect mod uses from src and adds them to dest. Does not erase extra mod uses already in dest.

Equations

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

def ImportGraph.Shake.copyExtraRevModUse (src dest : Lean.Environment) (srcAsyncMode destAsyncMode : Lean.EnvExtension.AsyncMode := isExtraRevModUseExtAsyncMode) (destAsyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Copies a new rev mod use from src to dest, preserving the one in dest if present.

Equations

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

@[inline]

def ImportGraph.Shake.copyShakeRecords (src dest : Lean.Environment) (srcAsyncMode destAsyncMode : Lean.EnvExtension.AsyncMode := Lean.EnvExtension.AsyncMode.sync) (destAsyncDecl : Lean.Name := Lean.Name.anonymous) : Lean.Environment

Copies all new shake records from src to dest. Does not erase the entries in dest.

Equations

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

def ImportGraph.Shake.withFreshShakeRecords {m : Type → Type} [Monad m] [Lean.MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α

Resets the shake extension entries (the records from the current module), then restores them after running the given action, merging any new records into the new ones.

Equations

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