Documentation

Lean.Environment

Note [Environment Branches] #

The kernel environment type Lean.Kernel.Environment enforces a linear order on the addition of declarations: addDeclCore takes an environment and returns a new one, assuming type checking succeeded. On the other hand, the metaprogramming-level Lean.Environment wrapper must allow for branching environment transformations so that multiple declarations can be elaborated concurrently while still being able to access information about preceding declarations that have also been branched out as soon as they are available.

The basic function to introduce such branches is addConstAsync, which takes an environment and returns a structure containing two environments: one for the "main" branch that can be used in further branching and eventually contains all the declarations of the file and one for the "async" branch that can be used concurrently to the main branch to elaborate and add the declaration for which the branch was introduced. Branches are "joined" back together implicitly via the kernel environment, which as mentioned cannot be changed concurrently: when the main branch first tries to access it, evaluation is blocked until the kernel environment on the async branch is complete. Thus adding two declarations A and B concurrently can be visualized like this:

o addConstAsync A
|\
| \
|  \
o addConstAsync B
|\   \
| \   o elaborate A
|  \  |
|   o elaborate B
|   | |
|   | o addDeclCore A
|   |/
|   o addDeclCore B
|  /
| /
|/
o .olean serialization calls Environment.toKernelEnv

While each edge represents a Lean.Environment that has its own view of the state of the module, the kernel environment really lives only in the right-most path, with all other paths merely holding an unfulfilled Task representing it and where forcing that task leads to the back-edges joining paths back together.

opaque Lean.debug.skipKernelTC :

Lean.Option Bool

opaque Lean.EnvExtensionStateSpec :

(α : Type) × Inhabited α

Opaque environment extension state.

def Lean.EnvExtensionState :

Equations

Lean.EnvExtensionState = Lean.EnvExtensionStateSpec.fst

Instances For

Lean.instInhabitedEnvExtensionState

instance Lean.instInhabitedEnvExtensionState :

Inhabited EnvExtensionState

Equations

Lean.instInhabitedEnvExtensionState = Lean.EnvExtensionStateSpec.snd

def Lean.ModuleIdx :

Equations

Lean.ModuleIdx = Nat

Instances For

instance Lean.instModuleIdxBEq :

Equations

Lean.instModuleIdxBEq = instBEqOfDecidableEq

instance Lean.instModuleIdxToString :

ToString ModuleIdx

Equations

Lean.instModuleIdxToString = instToStringNat

@[reducible, inline]

abbrev Lean.ModuleIdx.toNat (midx : ModuleIdx) :

Equations

midx.toNat = midx

instance Lean.instInhabitedModuleIdx :

Inhabited ModuleIdx

Equations

Lean.instInhabitedModuleIdx = { default := 0 }

instance Lean.instGetElemArrayModuleIdxLtNatToNatSize {α : Type u_1} :

GetElem (Array α) ModuleIdx α fun (a : Array α) (i : ModuleIdx) => i.toNat < a.size

Equations

Lean.instGetElemArrayModuleIdxLtNatToNatSize = { getElem := fun (a : Array α) (i : Lean.ModuleIdx) (h : i.toNat < a.size) => a[i.toNat] }

instance Lean.instGetElem?ArrayModuleIdxLtNatToNatSize {α : Type u_1} :

GetElem? (Array α) ModuleIdx α fun (a : Array α) (i : ModuleIdx) => i.toNat < a.size

Equations

Lean.instGetElem?ArrayModuleIdxLtNatToNatSize = GetElem?.mk (fun (a : Array α) (i : Lean.ModuleIdx) => a[i.toNat]?) fun [Inhabited α] (a : Array α) (i : Lean.ModuleIdx) => a[i.toNat]!

@[reducible, inline]

abbrev Lean.ConstMap :

Equations

Lean.ConstMap = Lean.SMap Lean.Name Lean.ConstantInfo

structure Lean.Import :

module : Name
runtimeOnly : Bool

Instances For

instance Lean.instReprImport :

Equations

Lean.instReprImport = { reprPrec := Lean.reprImport✝ }

instance Lean.instInhabitedImport :

Inhabited Import

Equations

Lean.instInhabitedImport = { default := { module := default, runtimeOnly := default } }

instance Lean.instCoeNameImport :

Coe Name Import

Equations

Lean.instCoeNameImport = { coe := fun (x : Lean.Name) => { module := x, runtimeOnly := false } }

instance Lean.instToStringImport :

ToString Import

Equations

Lean.instToStringImport = { toString := fun (imp : Lean.Import) => toString imp.module ++ if imp.runtimeOnly = true then " (runtime)" else "" }

def Lean.CompactedRegion :

A compacted region holds multiple Lean objects in a contiguous memory region, which can be read/written to/from disk. Objects inside the region do not have reference counters and cannot be freed individually. The contents of .olean files are compacted regions.

Equations

Lean.CompactedRegion = USize

@[extern lean_compacted_region_is_memory_mapped]

opaque Lean.CompactedRegion.isMemoryMapped :

CompactedRegion → Bool

@[extern lean_compacted_region_free]

unsafe opaque Lean.CompactedRegion.free :

CompactedRegion → IO Unit

Free a compacted region and its contents. No live references to the contents may exist at the time of invocation.

opaque Lean.EnvExtensionEntrySpec :

Opaque persistent environment extension entry.

def Lean.EnvExtensionEntry :

Equations

Lean.EnvExtensionEntry = Lean.EnvExtensionEntrySpec.type

Instances For

Lean.instNonemptyEnvExtensionEntry

instance Lean.instNonemptyEnvExtensionEntry :

Nonempty EnvExtensionEntry

structure Lean.ModuleData :

Content of a .olean file. We use compact.cpp to generate the image of this object in disk.

imports : Array Import
constNames : Array Name
constNames contains all constant names in constants. This information is redundant. It is equal to constants.map fun c => c.name, but it improves the performance of importModules. perf reports that 12% of the runtime was being spent on ConstantInfo.name when importing a file containing only import Lean
constants : Array ConstantInfo
extraConstNames : Array Name
Extra entries for the const2ModIdx map in the Environment object. The code generator creates auxiliary declarations that are not in the mapping constants, but we want to know in which module they were generated.
entries : Array (Name × Array EnvExtensionEntry)

Instances For

Lean.instInhabitedModuleData

instance Lean.instInhabitedModuleData :

Inhabited ModuleData

Equations

Lean.instInhabitedModuleData = { default := { imports := default, constNames := default, constants := default, extraConstNames := default, entries := default } }

structure Lean.EnvironmentHeader :

Environment fields that are not used often.

trustLevel : UInt32
The trust level used by the kernel. For example, the kernel assumes imported constants are type correct when the trust level is greater than zero.
mainModule : Name
Name of the module being compiled.
imports : Array Import
Direct imports
regions : Array CompactedRegion
Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management.
moduleNames : Array Name
Name of all imported modules (directly and indirectly). The index of a module name in the array equals the ModuleIdx for the same module.
moduleData : Array ModuleData
Module data for all imported modules.

Instances For

Lean.instNonemptyEnvironmentHeader

instance Lean.instNonemptyEnvironmentHeader :

Nonempty EnvironmentHeader

structure Lean.Kernel.Diagnostics :

unfoldCounter : PHashMap Name Nat
Number of times each declaration has been unfolded by the kernel.
enabled : Bool
If enabled = true, kernel records declarations that have been unfolded.

Instances For

Lean.Kernel.instInhabitedDiagnostics

instance Lean.Kernel.instInhabitedDiagnostics :

Inhabited Diagnostics

Equations

Lean.Kernel.instInhabitedDiagnostics = { default := { unfoldCounter := default, enabled := default } }

structure Lean.Kernel.Environment :

An environment stores declarations provided by the user. The kernel currently supports different kinds of declarations such as definitions, theorems, and inductive families. Each has a unique identifier (i.e., Name), and can be parameterized by a sequence of universe parameters. A constant in Lean is just a reference to a ConstantInfo object. The main task of the kernel is to type check these declarations and refuse type incorrect ones. The kernel does not allow declarations containing metavariables and/or free variables to be added to an environment. Environments are never destructively updated.

The environment also contains a collection of extensions. For example, the simp theorems declared by users are stored in an environment extension. Users can declare new extensions using meta-programming.

constants : ConstMap
Mapping from constant name to ConstantInfo. It contains all constants (definitions, theorems, axioms, etc) that have been already type checked by the kernel.
quotInit : Bool
quotInit = true if the command init_quot has already been executed for the environment, and Quot declarations have been added to the environment. When the flag is set, the type checker can assume that the Quot declarations in the environment have indeed been added by the kernel and not by the user.
diagnostics : Diagnostics
Diagnostic information collected during kernel execution.
Remark: We store kernel diagnostic information in an environment field to simplify the interface with the kernel implemented in C/C++. Thus, we can only track declarations in methods, such as addDecl, which return a new environment. Kernel.isDefEq and Kernel.whnf do not update the statistics. We claim this is ok since these methods are mainly used for debugging.
const2ModIdx : Std.HashMap Name ModuleIdx
Mapping from constant name to module (index) where constant has been declared. Recall that a Lean file has a header where previously compiled modules can be imported. Each imported module has a unique ModuleIdx. Many extensions use the ModuleIdx to efficiently retrieve information stored in imported modules.
Remark: this mapping also contains auxiliary constants, created by the code generator, that are not in the field constants. These auxiliary constants are invisible to the Lean kernel and elaborator. Only the code generator uses them.
extensions : Array Lean.EnvExtensionState
Environment extensions. It also includes user-defined extensions.
extraConstNames : Lean.NameSet
Constant names to be saved in the field extraConstNames at ModuleData. It contains auxiliary declaration names created by the code generator which are not in constants. When importing modules, we want to insert them at const2ModIdx.
header : EnvironmentHeader
The header contains additional information that is set at import time.

Instances For

Lean.Kernel.instNonemptyEnvironment

instance Lean.Kernel.instNonemptyEnvironment :

Nonempty Environment

inductive Lean.Kernel.Exception :

Exceptions that can be raised by the kernel when type checking new declarations.

unknownConstant (env : Environment) (name : Name) : Exception
alreadyDeclared (env : Environment) (name : Name) : Exception
declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr) : Exception
declHasMVars (env : Environment) (name : Name) (expr : Expr) : Exception
declHasFVars (env : Environment) (name : Name) (expr : Expr) : Exception
funExpected (env : Environment) (lctx : LocalContext) (expr : Expr) : Exception
typeExpected (env : Environment) (lctx : LocalContext) (expr : Expr) : Exception
letTypeMismatch (env : Environment) (lctx : LocalContext) (name : Name) (givenType expectedType : Expr) : Exception
exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr expectedType : Expr) : Exception
appTypeMismatch (env : Environment) (lctx : LocalContext) (app funType argType : Expr) : Exception
invalidProj (env : Environment) (lctx : LocalContext) (proj : Expr) : Exception
thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr) : Exception
other (msg : String) : Exception
deterministicTimeout : Exception
excessiveMemory : Exception
deepRecursion : Exception
interrupted : Exception

Instances For

Lean.Kernel.instNonemptyException

instance Lean.Kernel.instNonemptyException :

Nonempty Exception

@[export lean_environment_find]

def Lean.Kernel.Environment.find? (env : Environment) (n : Name) :

Option ConstantInfo

Equations

env.find? n = Lean.SMap.find?' env.constants n

@[extern lean_add_decl]

opaque Lean.Kernel.Environment.addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : Declaration) (cancelTk? : Option IO.CancelToken) :

Except Exception Environment

Type check given declaration and add it to the environment

@[extern lean_add_decl_without_checking]

opaque Lean.Kernel.Environment.addDeclWithoutChecking (env : Environment) (decl : Declaration) :

Except Exception Environment

Add declaration to kernel without type checking it.

WARNING This function is meant for temporarily working around kernel performance issues. It compromises soundness because, for example, a buggy tactic may produce an invalid proof, and the kernel will not catch it if the new option is set to true.

@[export lean_kernel_diag_is_enabled]

def Lean.Kernel.Environment.Diagnostics.isEnabled (d : Diagnostics) :

Equations

Lean.Kernel.Environment.Diagnostics.isEnabled d = d.enabled

def Lean.Kernel.Environment.enableDiag (env : Environment) (flag : Bool) :

Enables/disables kernel diagnostics.

Equations

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

def Lean.Kernel.Environment.isDiagnosticsEnabled (env : Environment) :

Equations

env.isDiagnosticsEnabled = env.diagnostics.enabled

def Lean.Kernel.Environment.resetDiag (env : Environment) :

Equations

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

@[export lean_kernel_record_unfold]

def Lean.Kernel.Environment.Diagnostics.recordUnfold (d : Diagnostics) (declName : Name) :

Equations

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

@[export lean_kernel_get_diag]

def Lean.Kernel.Environment.getDiagnostics (env : Environment) :

Equations

env.getDiagnostics = env.diagnostics

@[export lean_kernel_set_diag]

def Lean.Kernel.Environment.setDiagnostics (env : Environment) (diag : Diagnostics) :

Equations

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

@[reducible, inline, deprecated Lean.Kernel.Exception (since := "2024-12-12")]

abbrev Lean.KernelException :

Equations

Lean.KernelException = Lean.Kernel.Exception

inductive Lean.ConstantKind :

defn : ConstantKind
thm : ConstantKind
axiom : ConstantKind
opaque : ConstantKind
quot : ConstantKind
induct : ConstantKind
ctor : ConstantKind
recursor : ConstantKind

Instances For

instance Lean.instInhabitedConstantKind :

Inhabited ConstantKind

Equations

Lean.instInhabitedConstantKind = { default := Lean.ConstantKind.defn }

instance Lean.instBEqConstantKind :

BEq ConstantKind

Equations

Lean.instBEqConstantKind = { beq := Lean.beqConstantKind✝ }

instance Lean.instReprConstantKind :

Repr ConstantKind

Equations

Lean.instReprConstantKind = { reprPrec := Lean.reprConstantKind✝ }

structure Lean.AsyncConstantInfo :

ConstantInfo variant that allows for asynchronous filling of components via tasks.

name : Name
The declaration name, known immediately.
kind : ConstantKind
The kind of the constant, known immediately.
sig : Task ConstantVal
The "signature" including level params and type, potentially filled asynchronously.
constInfo : Task ConstantInfo
The final, complete constant info, potentially filled asynchronously.

Instances For

Lean.instInhabitedAsyncConstantInfo

instance Lean.instInhabitedAsyncConstantInfo :

Inhabited AsyncConstantInfo

Equations

Lean.instInhabitedAsyncConstantInfo = { default := { name := default, kind := default, sig := default, constInfo := default } }

def Lean.AsyncConstantInfo.toConstantVal (c : AsyncConstantInfo) :

Equations

c.toConstantVal = c.sig.get

def Lean.AsyncConstantInfo.toConstantInfo (c : AsyncConstantInfo) :

Equations

c.toConstantInfo = c.constInfo.get

def Lean.AsyncConstantInfo.ofConstantInfo (c : ConstantInfo) :

AsyncConstantInfo

Equations

Lean.AsyncConstantInfo.ofConstantInfo c = { name := c.name, kind := Lean.ConstantKind.ofConstantInfo c, sig := { get := c.toConstantVal }, constInfo := { get := c } }

instance Lean.instNonemptyAsyncContext :

Nonempty Lean.AsyncContext✝

structure Lean.AsyncConst :

Constant info and environment extension states eventually resulting from async elaboration.

constInfo : AsyncConstantInfo
exts? : Option (Task (Array EnvExtensionState))
Reported extension state eventually fulfilled by promise; may be missing for tasks (e.g. kernel checking) that can eagerly guarantee they will not report any state.

instance Lean.instInhabitedAsyncConsts :

Inhabited Lean.AsyncConsts✝

Equations

Lean.instInhabitedAsyncConsts = { default := { size := default, revList := default, map := default, normalizedTrie := default } }

structure Lean.Environment :

Elaboration-specific extension of Kernel.Environment that adds tracking of asynchronously elaborated declarations.

checkedWithoutAsync : Kernel.Environment
Kernel environment not containing any asynchronously elaborated declarations. Also stores environment extension state for the current branch of the environment.
Ignoring extension state, this is guaranteed to be some prior version of checked that is eagerly available. Thus we prefer taking information from it instead of checked whenever possible.
checked : Task Kernel.Environment
Kernel environment task that is fulfilled when all asynchronously elaborated declarations are finished, containing the resulting environment. Also collects the environment extension state of all environment branches that contributed contained declarations.
asyncConsts : Lean.AsyncConsts✝
Container of asynchronously elaborated declarations. For consistency, updateBaseAfterKernelAdd makes sure this contains constants added even synchronously, i.e. this is a superset of checkedWithoutAsync except for imported constants.
asyncCtx? : Option Lean.AsyncContext✝
Information about this asynchronous branch of the environment, if any.
realizedImportedConsts? : Option Lean.RealizationContext✝
Realized constants belonging to imported declarations. Must be initialized by calling enableRealizationsForImports.
realizedLocalConsts : Lean.NameMap Lean.RealizationContext✝
Realized constants belonging to local declarations. This is a map from local declarations, which need to be registered synchronously using enableRealizationsForConst, to their realization context incl. a ref of realized constants.

Instances For

Lean.instNonemptyEnvironment

instance Lean.instNonemptyEnvironment :

Nonempty Environment

@[export lean_elab_environment_of_kernel_env]

def Lean.Environment.ofKernelEnv (env : Kernel.Environment) :

Equations

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

@[export lean_elab_environment_to_kernel_env]

def Lean.Environment.toKernelEnv (env : Environment) :

Kernel.Environment

Equations

env.toKernelEnv = env.checked.get

def Lean.Environment.isRealizing (env : Environment) :

True while inside realizeConst's realize.

Equations

env.isRealizing = Option.any (fun (x : Lean.AsyncContext✝) => x.realizing) (Lean.Environment.asyncCtx?✝ env)

def Lean.Environment.asyncMayContain (env : Environment) (declName : Name) :

Checks whether the given declaration name may potentially added, or have been added, to the current environment branch, which is the case either if this is the main branch or if the declaration name is a suffix (modulo privacy and hygiene information) of the top-level declaration name for which this branch was created.

This function should always be checked before modifying an AsyncMode.async environment extension to ensure findStateAsync will be able to find the modification from other branches.

Equations

env.asyncMayContain declName = Option.all (fun (x : Lean.AsyncContext✝) => x.mayContain declName) (Lean.Environment.asyncCtx?✝ env)

def Lean.Environment.addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : Declaration) (cancelTk? : Option IO.CancelToken) (doCheck : Bool := true) :

Except Kernel.Exception Environment

Adds given declaration to the environment, type checking it unless doCheck is false.

This is a plumbing function for the implementation of Lean.addDecl, most users should use it instead.

Equations

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

def Lean.Environment.constants (env : Environment) :

Mapping from constant name to ConstantInfo. It contains all constants (definitions, theorems, axioms, etc) that have been already type checked by the kernel.

Equations

env.constants = env.toKernelEnv.constants

def Lean.Environment.const2ModIdx (env : Environment) :

Std.HashMap Name ModuleIdx

Mapping from constant name to module (index) where constant has been declared. Recall that a Lean file has a header where previously compiled modules can be imported. Each imported module has a unique ModuleIdx. Many extensions use the ModuleIdx to efficiently retrieve information stored in imported modules.

Remark: this mapping also contains auxiliary constants, created by the code generator, that are not in the field constants. These auxiliary constants are invisible to the Lean kernel and elaborator. Only the code generator uses them.

Equations

env.const2ModIdx = env.toKernelEnv.const2ModIdx

def Lean.Environment.addExtraName (env : Environment) (name : Name) :

Save an extra constant name that is used to populate const2ModIdx when we import .olean files. We use this feature to save in which module an auxiliary declaration created by the code generator has been created.

Equations

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

def Lean.Environment.findAsync? (env : Environment) (n : Name) :

Option AsyncConstantInfo

Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration tasks.

Equations

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

def Lean.Environment.findConstVal? (env : Environment) (n : Name) :

Option ConstantVal

Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration tasks for declaration bodies (which are not accessible from ConstantVal).

Equations

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

def Lean.Environment.enableRealizationsForImports (env : Environment) (opts : Options) :

BaseIO Environment

Allows realizeConst calls for imported declarations in all derived environment branches. Realizations will run using the given environment and options to ensure deterministic results. This function should be called directly after setMainModule to ensure that all realized constants use consistent private prefixes.

Equations

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

def Lean.Environment.enableRealizationsForConst (env : Environment) (opts : Options) (c : Name) :

BaseIO Environment

Allows realizeConst calls for the given declaration in all derived environment branches. Realizations will run using the given environment and options to ensure deterministic results. Note that while we check that the function isn't called too early, i.e. before the declaration is actually added to the environment, we cannot automatically check that it isn't called too late, i.e. before all environment extensions that may be relevant to realizations have been set. We do check that we are not calling it from a different branch than c was added on, which would be definitely too late.

Equations

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

def Lean.Environment.find? (env : Environment) (n : Name) :

Option ConstantInfo

Looks up the given declaration name in the environment, blocking on the corresponding elaboration task if not yet complete.

Equations

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

def Lean.Environment.dbgFormatAsyncState (env : Environment) :

Returns debug output about the asynchronous state of the environment.

Equations

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

def Lean.Environment.dbgFormatCheckedSyncState (env : Environment) :

Returns debug output about the synchronous state of the environment.

Equations

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

structure Lean.Environment.PromiseCheckedResult :

Result of Lean.Environment.promiseChecked.

mainEnv : Environment
Resulting "main branch" environment. Accessing the kernel environment will block until PromiseCheckedResult.commitChecked has been called.
asyncEnv : Environment
Resulting "async branch" environment which should be used in a new task and then to call PromiseCheckedResult.commitChecked to commit results back to the main environment. If it is not called and the PromiseCheckedResult object is dropped, the kernel environment will be left unchanged.
checkedEnvPromise : IO.Promise Lean.Kernel.Environment

def Lean.Environment.promiseChecked (env : Environment) :

BaseIO PromiseCheckedResult

Starts an asynchronous modification of the kernel environment. The environment is split into a "main" branch that will block on access to the kernel environment until PromiseCheckedResult.commitChecked has been called on the "async" environment branch.

Equations

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

def Lean.Environment.PromiseCheckedResult.commitChecked (res : PromiseCheckedResult) (env : Environment) :

Commits the kernel environment of the given environment back to the main branch.

Equations

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

structure Lean.Environment.AddConstAsyncResult :

Result of Lean.Environment.addConstAsync which is necessary to complete the asynchronous addition.

mainEnv : Environment
Resulting "main branch" environment which contains the declaration name as an asynchronous constant. Accessing the constant or kernel environment will block until the corresponding AddConstAsyncResult.commit* function has been called.
asyncEnv : Environment
Resulting "async branch" environment which should be used to add the desired declaration in a new task and then call AddConstAsyncResult.commit* to commit results back to the main environment. commitCheckEnv completes the addition; if it is not called and the AddConstAsyncResult object is dropped, sorryed default values will be reported instead and the kernel environment will be left unchanged.
constName : Lean.Name
kind : Lean.ConstantKind
sigPromise : IO.Promise Lean.ConstantVal
infoPromise : IO.Promise Lean.ConstantInfo
extensionsPromise : IO.Promise (Array Lean.EnvExtensionState)
checkedEnvPromise : IO.Promise Lean.Kernel.Environment

def Lean.Environment.addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (reportExts checkMayContain : Bool := true) :

IO AddConstAsyncResult

Starts the asynchronous addition of a constant to the environment. The environment is split into a "main" branch that holds a reference to the constant to be added but will block on access until the corresponding information has been added on the "async" environment branch and committed there; see the respective fields of AddConstAsyncResult as well as the [Environment Branches] note for more information.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitSignature (res : AddConstAsyncResult) (sig : ConstantVal) :

Commits the signature of the constant to the main environment branch. The declaration name must match the name originally given to addConstAsync. It is optional to call this function but can help in unblocking corresponding accesses to the constant on the main branch.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environment) (info? : Option ConstantInfo := none) :

Commits the full constant info to the main environment branch. If info? is none, it is taken from the given environment. The declaration name and kind must match the original values given to addConstAsync. The signature must match the previous commitSignature call, if any.

Equations

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

def Lean.Environment.AddConstAsyncResult.commitCheckEnv (res : AddConstAsyncResult) (env : Environment) :

Assuming Lean.addDecl has been run for the constant to be added on the async environment branch, commits the full constant info from that call to the main environment, waits for the final kernel environment resulting from the addDecl call, and commits it to the main branch as well, unblocking kernel additions there. All commitConst preconditions apply.

Equations

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

def Lean.Environment.contains (env : Environment) (n : Name) :

Equations

env.contains n = (env.findAsync? n).isSome

def Lean.Environment.imports (env : Environment) :

Equations

env.imports = env.header.imports

def Lean.Environment.allImportedModuleNames (env : Environment) :

Equations

env.allImportedModuleNames = env.header.moduleNames

def Lean.Environment.setMainModule (env : Environment) (m : Name) :

Equations

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

def Lean.Environment.mainModule (env : Environment) :

Equations

env.mainModule = env.header.mainModule

def Lean.Environment.getModuleIdxFor? (env : Environment) (declName : Name) :

Option ModuleIdx

Equations

env.getModuleIdxFor? declName = env.checkedWithoutAsync.const2ModIdx[declName]?

def Lean.Environment.isConstructor (env : Environment) (declName : Name) :

Equations

env.isConstructor declName = match env.find? declName with | some (Lean.ConstantInfo.ctorInfo val) => true | x => false

def Lean.Environment.isSafeDefinition (env : Environment) (declName : Name) :

Equations

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

def Lean.Environment.getModuleIdx? (env : Environment) (moduleName : Name) :

Option ModuleIdx

Equations

env.getModuleIdx? moduleName = Array.findIdx? (fun (x : Lean.Name) => x == moduleName) env.header.moduleNames

def Lean.ConstantInfo.instantiateTypeLevelParams (c : ConstantInfo) (ls : List Level) :

Equations

c.instantiateTypeLevelParams ls = c.type.instantiateLevelParams c.levelParams ls

def Lean.ConstantInfo.instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) :

Equations

c.instantiateValueLevelParams! ls = c.value!.instantiateLevelParams c.levelParams ls

inductive Lean.EnvExtension.AsyncMode :

Async access mode for environment extensions used in EnvironmentExtension.get/set/modifyState. Depending on their specific uses, extensions may opt out of the strict sync access mode in order to avoid blocking parallel elaboration and/or to optimize accesses. The access mode is set at environment extension registration time but can be overriden at EnvironmentExtension.getState in order to weaken it for specific accesses.

In all modes, the state stored into the .olean file for persistent environment extensions is the result of getState called on the main environment branch at the end of the file, i.e. it encompasses all modifications for all modes but local.

sync : AsyncMode
Default access mode, writing and reading the extension state to/from the full checked environment. This mode ensures the observed state is identical independently of whether or how parallel elaboration is used but getState will block on all prior environment branches by waiting for checked. setState and modifyState do not block.
While a safe default, any extension that reasonably could be used in parallel elaboration contexts should opt for a weaker mode to avoid blocking unless there is no way to access the correct state without waiting for all prior environment branches, in which case its data management should be restructured if at all possible.
local : AsyncMode
Accesses only the state of the current environment branch. Modifications on other branches are not visible and are ultimately discarded except for the main branch. Provides the fastest accessors, will never block.
This mode is particularly suitable for extensions where state does not escape from lexical scopes even without parallelism, e.g. ScopedEnvExtensions when setting local entries.
mainOnly : AsyncMode
Like local but panics when trying to modify the state on anything but the main environment branch. For extensions that fulfill this requirement, all modes functionally coincide but this is the safest and most efficient choice in that case, preventing accidental misuse.
This mode is suitable for extensions that are modified only at the command elaboration level before any environment forks in the command, and in particular for extensions that are modified only at the very beginning of the file.
async : AsyncMode
Accumulates modifications in the checked environment like sync, but getState will panic instead of blocking. Instead findStateAsync should be used, which will access the state of the environment branch corresponding to the passed declaration name, if any, or otherwise the state of the current branch. In other words, at most one environment branch will be blocked on instead of all prior branches. The local state can still be accessed by calling getState with mode local explicitly.
This mode is suitable for extensions with map-like state where the key uniquely identifies the top-level declaration where it could have been set, e.g. because the key on modification is always the surrounding declaration's name. Any calls to modifyState/setState should assert asyncMayContain with that key to ensure state is never accidentally stored in a branch where it cannot be found by findStateAsync. In particular, this mode is closest to how the environment's own constant map works which asserts the same predicate on modification and provides findAsync? for block-avoiding access.

Instances For

Lean.EnvExtension.instInhabitedAsyncMode

instance Lean.EnvExtension.instInhabitedAsyncMode :

Inhabited AsyncMode

Equations

Lean.EnvExtension.instInhabitedAsyncMode = { default := Lean.EnvExtension.AsyncMode.sync }

@[reducible, inline]

abbrev Lean.ReplayFn (σ : Type) :

Equations

Lean.ReplayFn σ = (σ → σ → List Lean.Name → σ → σ)

structure Lean.EnvExtension (σ : Type) :

Environment extension, can only be generated by registerEnvExtension that allocates a unique index for this extension into each environment's extension state's array.

idx : Nat
mkInitial : IO σ
asyncMode : AsyncMode
replay? : Option (ReplayFn σ)
Optional function that, given state before and after realization and newly added constants, replays this change onto a state from another (derived) environment. This function is used only when making changes to an extension inside a realizeConst call, in which case it must be present.

Instances For

Lean.instInhabitedEnvExtension

instance Lean.instInhabitedEnvExtension {a✝ : Type} :

Inhabited (EnvExtension a✝)

Equations

Lean.instInhabitedEnvExtension = { default := { idx := default, mkInitial := default, asyncMode := default, replay? := default } }

def Lean.EnvExtension.ensureExtensionsArraySize (exts : Array EnvExtensionState) :

IO (Array EnvExtensionState)

User-defined environment extensions are declared using the initialize command. This command is just syntax sugar for the init attribute. When we import lean modules, the vector stored at envExtensionsRef may increase in size because of user-defined environment extensions. When this happens, we must adjust the size of the env.extensions. This method is invoked when processing imports.

Equations

Lean.EnvExtension.ensureExtensionsArraySize exts = Lean.EnvExtension.ensureExtensionsArraySize.loop exts.size exts

partial def Lean.EnvExtension.ensureExtensionsArraySize.loop (i : Nat) (exts : Array EnvExtensionState) :

IO (Array EnvExtensionState)

def Lean.EnvExtension.mkInitialExtStates :

IO (Array EnvExtensionState)

Equations

Lean.EnvExtension.mkInitialExtStates = do let exts ← ST.Ref.get Lean.EnvExtension.envExtensionsRef✝ Array.mapM (fun (ext : Lean.EnvExtension Lean.EnvExtensionState) => ext.mkInitial) exts

def Lean.EnvExtension.modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) :

Applies the given function to the extension state. See AsyncMode for details on how modifications from different environment branches are reconciled.

Note that in modes sync and async, f will be called twice, on the local and on the checked state.

Equations

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

def Lean.EnvExtension.setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) :

Sets the extension state to the given value. See AsyncMode for details on how modifications from different environment branches are reconciled.

Equations

ext.setState env s = inline (ext.modifyState env fun (x : σ) => s)

@[implemented_by _private.Lean.Environment.0.Lean.EnvExtension.getStateUnsafe]

opaque Lean.EnvExtension.getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) (asyncMode : AsyncMode := ext.asyncMode) :

σ

Returns the current extension state. See AsyncMode for details on how modifications from different environment branches are reconciled. Panics if the extension is marked as async; see its documentation for more details. Overriding the extension's default AsyncMode is usually not recommended and should be considered only for important optimizations.

@[implemented_by _private.Lean.Environment.0.Lean.EnvExtension.findStateAsyncUnsafe]

opaque Lean.EnvExtension.findStateAsync {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) (declPrefix : Name) :

σ

Returns the final extension state on the environment branch corresponding to the passed declaration name, if any, or otherwise the state on the current branch. In other words, at most one environment branch will be blocked on.

def Lean.registerEnvExtension {σ : Type} (mkInitial : IO σ) (replay? : Option (ReplayFn σ) := none) (asyncMode : EnvExtension.AsyncMode := EnvExtension.AsyncMode.mainOnly) :

IO (EnvExtension σ)

Environment extensions can only be registered during initialization. Reasons: 1- Our implementation assumes the number of extensions does not change after an environment object is created. 2- We do not use any synchronization primitive to access envExtensionsRef.

Note that by default, extension state is not stored in .olean files and will not propagate across imports. For that, you need to register a persistent environment extension.

Equations

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

@[export lean_mk_empty_environment]

def Lean.mkEmptyEnvironment (trustLevel : UInt32 := 0) :

Equations

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

structure Lean.PersistentEnvExtensionState (α σ : Type) :

importedEntries : Array (Array α)
state : σ

Instances For

Lean.instInhabitedPersistentEnvExtensionState

structure Lean.ImportM.Context :

env : Environment
opts : Options

@[reducible, inline]

abbrev Lean.ImportM (α : Type) :

Equations

Lean.ImportM = ReaderT Lean.ImportM.Context IO

Instances For

Lean.instMonadLiftImportMAttrM

structure Lean.PersistentEnvExtension (α β σ : Type) :

An environment extension with support for storing/retrieving entries from a .olean file.

α is the type of the entries that are stored in .olean files.
β is the type of values used to update the state.
σ is the actual state.

For most extensions, α and β coincide. α and ‵β` do not coincide for extensions where the data used to update the state contains elements which cannot be stored in files (for example, closures).

During elaboration of a module, state of type σ can be both read and written. When elaboration is complete, the state of type σ is converted to serialized state of type Array α by exportEntriesFn. To read the current module's state, use PersistentEnvExtension.getState. To modify it, use PersistentEnvExtension.addEntry, with an addEntryFn that performs the appropriate modification.

When a module is loaded, the values saved by all of its dependencies for this PersistentEnvExtension are available as an Array (Array α) via the environment extension, with one array per transitively imported module. The state of type σ used in the current module can be initialized from these imports by specifying a suitable addImportedFn. The addImportedFn runs at the beginning of elaboration for every module, so it's usually better for performance to query the array of imported modules directly, because only a fraction of imported entries is usually queried during elaboration of a module.

The most typical pattern for using PersistentEnvExtension is to set σ to a datatype such as NameMap that efficiently tracks data for the current module. Then, in exportEntriesFn, this type is converted to an array of pairs, sorted by the key. Given ext : PersistentEnvExtension α β σ and env : Environment, the complete array of imported entries sorted by module index can be obtained using (ext.toEnvExtension.getState env).importedEntries. To query the extension for some constant name n, first use env.getModuleIdxFor? n. If it returns none, look up n in the current module's state (the NameMap). If it returns some idx, use ext.getModuleEntries env idx to get the array of entries for n's defining module, and query it using Array.binSearch. This pattern imposes a constraint that the extension can only track metadata that is declared in the same module as the definition to which it applies; relaxing this restriction can make queries slower due to needing to search all modules. If it is necessary to search all modules, it is usually better to initialize the state of type σ once from all imported entries and choose a more efficient search datastructure for it.

Note that addEntryFn is not in IO. This is intentional, and allows us to write simple functions such as

def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
aliasExtension.addEntry env (a, e)

without using IO. We have many functions like addAlias.

toEnvExtension : EnvExtension (PersistentEnvExtensionState α σ)
name : Name
addImportedFn : Array (Array α) → ImportM σ
addEntryFn : σ → β → σ
exportEntriesFn : σ → Array α
statsFn : σ → Format

Instances For

Lean.instInhabitedPersistentEnvExtension

instance Lean.instInhabitedPersistentEnvExtensionState {α σ : Type} [Inhabited σ] :

Inhabited (PersistentEnvExtensionState α σ)

Equations

Lean.instInhabitedPersistentEnvExtensionState = { default := { importedEntries := #[], state := default } }

instance Lean.instInhabitedPersistentEnvExtension {α β σ : Type} [Inhabited σ] :

Inhabited (PersistentEnvExtension α β σ)

Equations

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

def Lean.PersistentEnvExtension.getModuleEntries {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) (m : ModuleIdx) :

Equations

ext.getModuleEntries env m = (ext.toEnvExtension.getState env Lean.EnvExtension.AsyncMode.local).importedEntries[m]!

def Lean.PersistentEnvExtension.addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (b : β) :

Equations

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

def Lean.PersistentEnvExtension.getState {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) :

σ

Get the current state of the given extension in the given environment.

Equations

ext.getState env asyncMode = (ext.toEnvExtension.getState env asyncMode).state

def Lean.PersistentEnvExtension.setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) :

Set the current state of the given extension in the given environment.

Equations

ext.setState env s = ext.toEnvExtension.modifyState env fun (ps : Lean.PersistentEnvExtensionState α σ) => { importedEntries := ps.importedEntries, state := s }

def Lean.PersistentEnvExtension.modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) :

Modify the state of the given extension in the given environment by applying the given function.

Equations

ext.modifyState env f = ext.toEnvExtension.modifyState env fun (ps : Lean.PersistentEnvExtensionState α σ) => { importedEntries := ps.importedEntries, state := f ps.state }

def Lean.PersistentEnvExtension.findStateAsync {α β σ : Type} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) (declPrefix : Name) :

σ

Returns the final extension state on the environment branch corresponding to the passed declaration name, if any, or otherwise the state on the current branch. In other words, at most one environment branch will be blocked on.

Equations

ext.findStateAsync env declPrefix = (ext.toEnvExtension.findStateAsync env declPrefix).state

opaque Lean.persistentEnvExtensionsRef :

IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState))

structure Lean.PersistentEnvExtensionDescr (α β σ : Type) :

name : Name
mkInitial : IO σ
addImportedFn : Array (Array α) → ImportM σ
addEntryFn : σ → β → σ
exportEntriesFn : σ → Array α
statsFn : σ → Format
asyncMode : EnvExtension.AsyncMode
replay? : Option (ReplayFn σ)

unsafe def Lean.registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) :

IO (PersistentEnvExtension α β σ)

Equations

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

@[implemented_by Lean.registerPersistentEnvExtensionUnsafe]

opaque Lean.registerPersistentEnvExtension {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) :

IO (PersistentEnvExtension α β σ)

def Lean.SimplePersistentEnvExtension (α σ : Type) :

Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries.

Equations

Lean.SimplePersistentEnvExtension α σ = Lean.PersistentEnvExtension α α (List α × σ)

Instances For

Lean.SimplePersistentEnvExtension.instInhabited

@[specialize #[]]

def Lean.mkStateFromImportedEntries {α σ : Type} (addEntryFn : σ → α → σ) (initState : σ) (as : Array (Array α)) :

σ

Equations

Lean.mkStateFromImportedEntries addEntryFn initState as = Array.foldl (fun (r : σ) (es : Array α) => Array.foldl (fun (r : σ) (e : α) => addEntryFn r e) r es) initState as

structure Lean.SimplePersistentEnvExtensionDescr (α σ : Type) :

name : Name
addEntryFn : σ → α → σ
addImportedFn : Array (Array α) → σ
toArrayFn : List α → Array α
asyncMode : EnvExtension.AsyncMode

def Lean.registerSimplePersistentEnvExtension {α σ : Type} [Inhabited σ] (descr : SimplePersistentEnvExtensionDescr α σ) :

IO (SimplePersistentEnvExtension α σ)

Equations

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

instance Lean.SimplePersistentEnvExtension.instInhabited {α σ : Type} [Inhabited σ] :

Inhabited (SimplePersistentEnvExtension α σ)

Equations

Lean.SimplePersistentEnvExtension.instInhabited = inferInstanceAs (Inhabited (Lean.PersistentEnvExtension α α (List α × σ)))

def Lean.SimplePersistentEnvExtension.getEntries {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) :

Get the list of values used to update the state of the given SimplePersistentEnvExtension in the current file.

Equations

ext.getEntries env = (Lean.PersistentEnvExtension.getState ext env).fst

def Lean.SimplePersistentEnvExtension.getState {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) :

σ

Get the current state of the given SimplePersistentEnvExtension.

Equations

ext.getState env asyncMode = (Lean.PersistentEnvExtension.getState ext env asyncMode).snd

def Lean.SimplePersistentEnvExtension.setState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (s : σ) :

Set the current state of the given SimplePersistentEnvExtension. This change is not persisted across files.

Equations

ext.setState env s = Lean.PersistentEnvExtension.modifyState ext env fun (x : List α × σ) => match x with | (entries, snd) => (entries, s)

def Lean.SimplePersistentEnvExtension.modifyState {α σ : Type} (ext : SimplePersistentEnvExtension α σ) (env : Environment) (f : σ → σ) :

Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.

Equations

ext.modifyState env f = Lean.PersistentEnvExtension.modifyState ext env fun (x : List α × σ) => match x with | (entries, s) => (entries, f s)

def Lean.SimplePersistentEnvExtension.findStateAsync {α σ : Type} [Inhabited σ] (ext : SimplePersistentEnvExtension α σ) (env : Environment) (declPrefix : Name) :

σ

Returns the final extension state on the environment branch corresponding to the passed declaration name, if any, or otherwise the state on the current branch. In other words, at most one environment branch will be blocked on.

Equations

ext.findStateAsync env declPrefix = (Lean.PersistentEnvExtension.findStateAsync ext env declPrefix).snd

def Lean.TagDeclarationExtension :

Environment extension for tagging declarations. Declarations must only be tagged in the module where they were declared.

Equations

Lean.TagDeclarationExtension = Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet

Instances For

Lean.TagDeclarationExtension.instInhabited

def Lean.mkTagDeclarationExtension (name : Name := by exact decl_name%) :

IO TagDeclarationExtension

Equations

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

instance Lean.TagDeclarationExtension.instInhabited :

Inhabited TagDeclarationExtension

Equations

Lean.TagDeclarationExtension.instInhabited = inferInstanceAs (Inhabited (Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet))

def Lean.TagDeclarationExtension.tag (ext : TagDeclarationExtension) (env : Environment) (declName : Name) :

Equations

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

def Lean.TagDeclarationExtension.isTagged (ext : TagDeclarationExtension) (env : Environment) (declName : Name) :

Equations

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

def Lean.MapDeclarationExtension (α : Type) :

Environment extension for mapping declarations to values. Declarations must only be inserted into the mapping in the module where they were declared.

Equations

Lean.MapDeclarationExtension α = Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)

Instances For

Lean.MapDeclarationExtension.instInhabited

def Lean.mkMapDeclarationExtension {α : Type} (name : Name := by exact decl_name%) :

IO (MapDeclarationExtension α)

Equations

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

instance Lean.MapDeclarationExtension.instInhabited {α : Type} :

Inhabited (MapDeclarationExtension α)

Equations

Lean.MapDeclarationExtension.instInhabited = inferInstanceAs (Inhabited (Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)))

def Lean.MapDeclarationExtension.insert {α : Type} (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) (val : α) :

Equations

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

def Lean.MapDeclarationExtension.find? {α : Type} [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) :

Equations

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

def Lean.MapDeclarationExtension.contains {α : Type} [Inhabited α] (ext : MapDeclarationExtension α) (env : Environment) (declName : Name) :

Equations

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

@[extern lean_save_module_data]

opaque Lean.saveModuleData (fname : System.FilePath) (mod : Name) (data : ModuleData) :

@[extern lean_read_module_data]

opaque Lean.readModuleData (fname : System.FilePath) :

IO (ModuleData × CompactedRegion)

@[noinline, export lean_environment_free_regions]

unsafe def Lean.Environment.freeRegions (env : Environment) :

Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in particular, env should be the last reference to any Environment derived from these imports.

Equations

env.freeRegions = Array.forM Lean.CompactedRegion.free env.header.regions

def Lean.mkModuleData (env : Environment) :

Equations

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

@[export lean_write_module]

def Lean.writeModule (env : Environment) (fname : System.FilePath) :

Equations

Lean.writeModule env fname = do let __do_lift ← Lean.mkModuleData env Lean.saveModuleData fname env.mainModule __do_lift

def Lean.mkExtNameMap (startingAt : Nat) :

IO (Std.HashMap Name Nat)

Construct a mapping from persistent extension name to extension index at the array of persistent extensions. We only consider extensions starting with index >= startingAt.

Equations

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

@[extern 2 lean_update_env_attributes]

opaque Lean.updateEnvAttributes :

Environment → IO Environment

"Forward declaration" needed for updating the attribute table with user-defined attributes. User-defined attributes are declared using the initialize command. The initialize command is just syntax sugar for the init attribute. The init attribute is initialized after the attributeExtension is initialized. We cannot change the order since the init attribute is an attribute, and requires this extension. The attributeExtension initializer uses attributeMapRef to initialize the attribute mapping. When we a new user-defined attribute declaration is imported, attributeMapRef is updated. Later, we set this method with code that adds the user-defined attributes that were imported after we initialized attributeExtension.

@[extern 1 lean_get_num_attributes]

opaque Lean.getNumBuiltinAttributes :

"Forward declaration" for retrieving the number of builtin attributes.

structure Lean.ImportState :

moduleNameSet : NameHashSet
moduleNames : Array Name
moduleData : Array ModuleData
regions : Array CompactedRegion

def Lean.throwAlreadyImported {α : Type} (s : ImportState) (const2ModIdx : Std.HashMap Name ModuleIdx) (modIdx : Nat) (cname : Name) :

IO α

Equations

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

@[reducible, inline]

abbrev Lean.ImportStateM (α : Type) :

Equations

Lean.ImportStateM = StateRefT' IO.RealWorld Lean.ImportState IO

@[inline]

def Lean.ImportStateM.run {α : Type} (x : ImportStateM α) (s : ImportState := { moduleNameSet := ∅, moduleNames := #[], moduleData := #[], regions := #[] }) :

IO (α × ImportState)

Equations

x.run s = StateRefT'.run x s

partial def Lean.importModulesCore (imports : Array Import) :

ImportStateM Unit

def Lean.finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (leakEnv : Bool := false) :

Construct environment from importModulesCore results.

If leakEnv is true, we mark the environment as persistent, which means it will not be freed. We set this when the object would survive until the end of the process anyway. In exchange, RC updates are avoided, which is especially important when they would be atomic because the environment is shared across threads (potentially, storing it in an IO.Ref is sufficient for marking it as such).

Equations

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

@[export lean_import_modules]

def Lean.importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv : Bool := false) :

Equations

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

unsafe def Lean.withImportModules {α : Type} (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (act : Environment → IO α) :

IO α

Create environment object from imports and free compacted regions after calling act. No live references to the environment object or imported objects may exist after act finishes.

Equations

Lean.withImportModules imports opts trustLevel act = do let env ← Lean.importModules imports opts trustLevel tryFinally (act env) env.freeRegions

opaque Lean.namespacesExt :

SimplePersistentEnvExtension Name NameSSet

Environment extension for tracking all namespace declared by users.

def Lean.Kernel.enableDiag (env : Lean.Environment) (flag : Bool) :

Lean.Environment

Enables/disables kernel diagnostics.

Equations

Lean.Kernel.enableDiag env flag = Lean.Environment.modifyCheckedAsync✝ env fun (x : Lean.Kernel.Environment) => x.enableDiag flag

def Lean.Kernel.isDiagnosticsEnabled (env : Lean.Environment) :

Equations

Lean.Kernel.isDiagnosticsEnabled env = env.checkedWithoutAsync.isDiagnosticsEnabled

def Lean.Kernel.resetDiag (env : Lean.Environment) :

Lean.Environment

Equations

Lean.Kernel.resetDiag env = Lean.Environment.modifyCheckedAsync✝ env fun (x : Lean.Kernel.Environment) => x.resetDiag

def Lean.Kernel.getDiagnostics (env : Lean.Environment) :

Equations

Lean.Kernel.getDiagnostics env = env.checked.get.diagnostics

def Lean.Kernel.setDiagnostics (env : Lean.Environment) (diag : Diagnostics) :

Lean.Environment

Equations

Lean.Kernel.setDiagnostics env diag = Lean.Environment.modifyCheckedAsync✝ env fun (x : Lean.Kernel.Environment) => x.setDiagnostics diag

def Lean.Environment.registerNamespace (env : Environment) (n : Name) :

Register a new namespace in the environment.

Equations

env.registerNamespace n = if (Lean.namespacesExt.getState env).contains n = true then env else Lean.PersistentEnvExtension.addEntry Lean.namespacesExt env n

def Lean.Environment.isNamespace (env : Environment) (n : Name) :

Return true if n is the name of a namespace in env.

Equations

env.isNamespace n = (Lean.namespacesExt.getState env).contains n

def Lean.Environment.getNamespaceSet (env : Environment) :

Return a set containing all namespaces in env.

Equations

env.getNamespaceSet = Lean.namespacesExt.getState env

@[export lean_display_stats]

def Lean.Environment.displayStats (env : Environment) :

Equations

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

@[extern lean_eval_const]

unsafe opaque Lean.Environment.evalConst (α : Type u_1) (env : Environment) (opts : Options) (constName : Name) :

Except String α

Evaluate the given declaration under the given environment to a value of the given type. This function is only safe to use if the type matches the declaration's type in the environment and if enableInitializersExecution has been used before importing any modules.

unsafe def Lean.Environment.evalConstCheck (α : Type) (env : Environment) (opts : Options) (typeName constName : Name) :

ExceptT String Id α

Like evalConst, but first check that constName indeed is a declaration of type typeName. Note that this function cannot guarantee that typeName is in fact the name of the type α.

Equations

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

def Lean.Environment.hasUnsafe (env : Environment) (e : Expr) :

Equations

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

def Lean.Environment.realizeConst (env : Environment) (forConst constName : Name) (realize : Environment → Options → BaseIO (Environment × Dynamic)) :

IO (Environment × Dynamic)

Plumbing function for Lean.Meta.realizeConst; see documentation there.

Equations

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

def Lean.Environment.realizeConst.maybeAddToKernelEnv (oldEnv newEnv : Environment) (consts : List AsyncConst) (kenv : Kernel.Environment) (exts : Array (EnvExtension EnvExtensionState)) :

Kernel.Environment

Equations

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

Kernel API #

@[extern lean_kernel_is_def_eq]

opaque Lean.Kernel.isDefEq (env : Lean.Environment) (lctx : LocalContext) (a b : Expr) :

Except Exception Bool

Kernel isDefEq predicate. We use it mainly for debugging purposes. Recall that the kernel type checker does not support metavariables. When implementing automation, consider using the MetaM methods.

def Lean.Kernel.isDefEqGuarded (env : Lean.Environment) (lctx : LocalContext) (a b : Expr) :

Equations

Lean.Kernel.isDefEqGuarded env lctx a b = match Lean.Kernel.isDefEq env lctx a b with | Except.ok result => result | x => false

@[extern lean_kernel_whnf]

opaque Lean.Kernel.whnf (env : Lean.Environment) (lctx : LocalContext) (a : Expr) :

Except Exception Expr

Kernel WHNF function. We use it mainly for debugging purposes. Recall that the kernel type checker does not support metavariables. When implementing automation, consider using the MetaM methods.

@[extern lean_kernel_check]

opaque Lean.Kernel.check (env : Lean.Environment) (lctx : LocalContext) (a : Expr) :

Except Exception Expr

Kernel typecheck function. We use it mainly for debugging purposes. Recall that the Kernel type checker does not support metavariables. When implementing automation, consider using the MetaM methods.

class Lean.MonadEnv (m : Type → Type) :

getEnv : m Environment
modifyEnv : (Environment → Environment) → m Unit

Instances

@[always_inline]

instance Lean.instMonadEnvOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadEnv m] :

Equations

Lean.instMonadEnvOfMonadLift m n = { getEnv := liftM Lean.getEnv, modifyEnv := fun (f : Lean.Environment → Lean.Environment) => liftM (Lean.modifyEnv f) }

def Lean.mkDefinitionValInferrringUnsafe {m : Type → Type} [Monad m] [MonadEnv m] (name : Name) (levelParams : List Name) (type value : Expr) (hints : ReducibilityHints) :

m DefinitionVal

Constructs a DefinitionVal, inferring the unsafe field

Equations

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

def Lean.getMaxHeight (env : Environment) (e : Expr) :

Equations

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