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

@[instance_reducible]

instance ImportGraph.Shake.instReprIndirectModUse_importGraph : Repr Lean.IndirectModUse

@[instance_reducible]

instance ImportGraph.Shake.instHashableIndirectModUse_importGraph : Hashable Lean.IndirectModUse

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

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

@[instance_reducible]

instance ImportGraph.Shake.instOrdIndirectModUse_importGraph : Ord Lean.IndirectModUse

@[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.

@[inline]

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

@[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

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.

@[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.

@[inline]

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

@[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

@[inline]

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

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.

@[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.

@[inline]

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

Gets the state of the extraModUses extension.

@[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.

@[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.

@[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).

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.

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.

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.

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.

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.

@[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.

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.