Documentation

Mathlib.Tactic.Cache

Once-per-file cache for tactics #

This file defines cache data structures for tactics that are initialized the first time they are accessed. Since Lean 4 starts one process per file, these caches are once-per-file and can for example be used to cache information about the imported modules.

The Cache α data structure is the most generic version we define. It is created using Cache.mk f where f : MetaM α performs the initialization of the cache:

initialize numberOfImports : Cache NatCache.mk do
  (← getEnv).imports.size

-- (does not work in the same module where the cache is defined)
#eval show MetaM Nat from numberOfImports.get

The DeclCache α data structure computes a fold over the environment's constants: DeclCache.mk empty f constructs such a cache where empty : α and f : Name → ConstantInfo → α → MetaM α. The result of the constants in the imports is cached between tactic invocations, while for constants defined in the same file f is evaluated again every time. This kind of cache can be used e.g. to populate discrimination trees.

Creates a cache with an initialization function.

Equations
def Mathlib.Tactic.Cache.get {m : TypeType} {α : Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadLog m] [inst : Lean.MonadOptions m] [inst : MonadLiftT BaseIO m] [inst : MonadExcept Lean.Exception m] (cache : Mathlib.Tactic.Cache α) :
m α

Access the cache. Calling this function for the first time will initialize the cache with the function provided in the constructor.

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

Cached fold over the environment's declarations, where a given function is applied to α for every constant.

Equations
def Mathlib.Tactic.DeclCache.mk {α : Type} (profilingName : String) (empty : α) (addDecl : Lean.NameLean.ConstantInfoαLean.MetaM α) :

Creates a DeclCache. The cached structure α is initialized with empty, and then addDecl is called for every constant in the environment. Calls to addDecl for imported constants are cached.

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

Access the cache. Calling this function for the first time will initialize the cache with the function provided in the constructor.

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