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 : Type

Equations

• Lean.EnvExtensionState = Lean.EnvExtensionStateSpec.fst

@[instance_reducible]

instance Lean.instInhabitedEnvExtensionState : Inhabited EnvExtensionState

Equations

• Lean.instInhabitedEnvExtensionState = Lean.EnvExtensionStateSpec.snd

def Lean.ModuleIdx : Type

Equations

• Lean.ModuleIdx = Nat

@[instance_reducible]

instance Lean.instBEqModuleIdx : BEq ModuleIdx

Equations

• Lean.instBEqModuleIdx = { beq := Lean.instBEqModuleIdx._aux_1 }

@[instance_reducible]

instance Lean.instToStringModuleIdx : ToString ModuleIdx

Equations

• Lean.instToStringModuleIdx = { toString := Lean.instToStringModuleIdx._aux_1 }

@[instance_reducible]

instance Lean.instHashableModuleIdx : Hashable ModuleIdx

Equations

• Lean.instHashableModuleIdx = { hash := Lean.instHashableModuleIdx._aux_1 }

@[reducible, inline]

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

Equations

• midx.toNat = midx

@[instance_reducible]

instance Lean.instInhabitedModuleIdx : Inhabited ModuleIdx

Equations

• Lean.instInhabitedModuleIdx = { default := 0 }

@[instance_reducible]

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_reducible]

instance Lean.instGetElem?ArrayModuleIdxLtNatToNatSize {α : Type u_1} : GetElem? (Array α) ModuleIdx α fun (a : Array α) (i : ModuleIdx) => i.toNat < a.size

Equations

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

@[reducible, inline]

abbrev Lean.ConstMap : Type

Equations

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

opaque Lean.EnvExtensionEntrySpec : NonemptyType

Opaque persistent environment extension entry.

def Lean.EnvExtensionEntry : Type

Equations

• Lean.EnvExtensionEntry = Lean.EnvExtensionEntrySpec.type

instance Lean.instNonemptyEnvExtensionEntry : Nonempty EnvExtensionEntry

structure Lean.ModuleData : Type

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

• isModule : Bool

  Participating in the module system?

• 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)

@[instance_reducible]

instance Lean.instInhabitedModuleData : Inhabited ModuleData

Equations

• Lean.instInhabitedModuleData = { default := Lean.instInhabitedModuleData.default }

structure Lean.EffectiveImport extends Lean.Import : Type

Import including information resulting from processing of the entire import DAG.

• module : Name
• importAll : Bool
• isExported : Bool
• isMeta : Bool
• irPhases : IRPhases

  Phases for which the import's IR is available.

• hasData : Bool

  Whether the import's .olean* data has been loaded (otherwise only the .ir is).

@[instance_reducible]

instance Lean.instInhabitedEffectiveImport : Inhabited EffectiveImport

Equations

• Lean.instInhabitedEffectiveImport = { default := Lean.instInhabitedEffectiveImport.default }

structure Lean.EnvironmentHeader : Type

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.

• isModule : Bool

  Participating in the module system?

• 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.

• modules : Array EffectiveImport

  Direct and transitive imports. Modules are given with their effective import modifiers, not their original ones. Each module is listed at most once. The index of a module in the array equals the ModuleIdx for the same module.

• 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.

• moduleName2Idx : Std.HashMap Lean.Name Lean.ModuleIdx
• importAllModules : Array EffectiveImport

  Subset of modules for which importAll is true. This is assumed to be a much smaller set so we precompute it instead of iterating over all of modules multiple times. However, note that in a non-module file, this is identical to modules.

• moduleData : Array ModuleData

  Module data for all imported modules.

instance Lean.instNonemptyEnvironmentHeader : Nonempty EnvironmentHeader

structure Lean.Kernel.Diagnostics : Type

• 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.

@[instance_reducible]

instance Lean.Kernel.instInhabitedDiagnostics : Inhabited Diagnostics

Equations

• Lean.Kernel.instInhabitedDiagnostics = { default := Lean.Kernel.instInhabitedDiagnostics.default }

structure Lean.Kernel.Environment : Type

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
• irBaseExts : Array Lean.EnvExtensionState
• extGens : Array Nat
• trackedGen : Nat

  Counter bumped by every modification of a generation-tracked extension (PersistentEnvExtensionDescrCore.trackGen): while it is unchanged, no such extension has changed. Like the generations, it rolls back with the environment, so after a rollback a different modification can reach a value seen before. Results stored in the environment roll back with it and stay sound. As the counter only grows along one environment branch, a result stored outside the environment stays sound across a rollback only if it was stamped with at most the restored value; later ones must be dropped.

• header : EnvironmentHeader

  The header contains additional information that is set at import time.

instance Lean.Kernel.instNonemptyEnvironment : Nonempty Environment

inductive Lean.Kernel.Exception : Type

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

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 maxRecDepth : 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) : Bool

Equations

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

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

Enables/disables kernel diagnostics.

Equations

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

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

Equations

• env.isDiagnosticsEnabled = env.diagnostics.enabled

def Lean.Kernel.Environment.resetDiag (env : Environment) : 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) : Diagnostics

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) : Diagnostics

Equations

• env.getDiagnostics = env.diagnostics

@[export lean_kernel_set_diag]

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

Equations

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

inductive Lean.ConstantKind : Type

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

@[instance_reducible]

instance Lean.instInhabitedConstantKind : Inhabited ConstantKind

Equations

• Lean.instInhabitedConstantKind = { default := Lean.instInhabitedConstantKind.default }

@[instance_reducible]

instance Lean.instBEqConstantKind : BEq ConstantKind

Equations

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

def Lean.instBEqConstantKind.beq : ConstantKind → ConstantKind → Bool

Equations

• Lean.instBEqConstantKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Lean.instReprConstantKind : Repr ConstantKind

Equations

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

def Lean.instReprConstantKind.repr : ConstantKind → Nat → Format

Equations

• Lean.instReprConstantKind.repr Lean.ConstantKind.defn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.defn")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.thm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.thm")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.axiom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.axiom")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.opaque prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.opaque")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.quot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.quot")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.induct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.induct")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.ctor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.ctor")).group prec✝
• Lean.instReprConstantKind.repr Lean.ConstantKind.recursor prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.ConstantKind.recursor")).group prec✝

def Lean.ConstantKind.ofConstantInfo : ConstantInfo → ConstantKind

Equations

• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.defnInfo val) = Lean.ConstantKind.defn
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.thmInfo val) = Lean.ConstantKind.thm
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.axiomInfo val) = Lean.ConstantKind.axiom
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.opaqueInfo val) = Lean.ConstantKind.opaque
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.quotInfo val) = Lean.ConstantKind.quot
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.inductInfo val) = Lean.ConstantKind.induct
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.ctorInfo val) = Lean.ConstantKind.ctor
• Lean.ConstantKind.ofConstantInfo (Lean.ConstantInfo.recInfo val) = Lean.ConstantKind.recursor

structure Lean.AsyncConstantInfo : Type

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.

@[instance_reducible]

instance Lean.instInhabitedAsyncConstantInfo : Inhabited AsyncConstantInfo

Equations

• Lean.instInhabitedAsyncConstantInfo = { default := Lean.instInhabitedAsyncConstantInfo.default }

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

Equations

• c.toConstantVal = c.sig.get

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

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 } }

def Lean.AsyncConstantInfo.isUnsafe (c : AsyncConstantInfo) : Bool

Equations

• c.isUnsafe = match c.kind with | Lean.ConstantKind.thm => false | x => c.toConstantInfo.isUnsafe

inductive Lean.Environment.Visibility : Type

Accessibility levels of declarations in Lean.Environment.

• private : Visibility

  Information private to the module.

• public : Visibility

  Information to be exported to other modules.

@[instance_reducible]

instance Lean.Environment.instInhabitedVisibility : Inhabited Visibility

Equations

• Lean.Environment.instInhabitedVisibility = { default := Lean.Environment.instInhabitedVisibility.default }

def Lean.Environment.instBEqVisibility.beq : Visibility → Visibility → Bool

Equations

• Lean.Environment.instBEqVisibility.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Lean.Environment.instBEqVisibility : BEq Visibility

Equations

• Lean.Environment.instBEqVisibility = { beq := Lean.Environment.instBEqVisibility.beq }

structure Lean.DeclChangeLog : Type

The declarations whose declaration-keyed state changed, as recorded in Environment.declChangeLog. A list with the newest entry first, as the log only grows at one end and validation only reads the entries logged since some position: appending then never copies the log, even while older environments share it.

• size : Nat

  Number of entries, which positions in the log refer to.

• entries : List Name

  The logged declarations, newest first.

@[instance_reducible]

instance Lean.instInhabitedDeclChangeLog : Inhabited DeclChangeLog

Equations

• Lean.instInhabitedDeclChangeLog = { default := Lean.instInhabitedDeclChangeLog.default }

def Lean.DeclChangeLog.push (log : DeclChangeLog) (declName : Name) : DeclChangeLog

Appends declName to the log.

Equations

• log.push declName = { size := log.size + 1, entries := declName :: log.entries }

def Lean.DeclChangeLog.allSince (log : DeclChangeLog) (fromPos : Nat) (p : Name → Bool) : Bool

Returns whether p holds for all entries logged since position fromPos.

Equations

• log.allSince fromPos p = Lean.DeclChangeLog.allSince.go✝ p (log.size - fromPos) log.entries

structure Lean.Environment : Type

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

• base : VisibilityMap Lean.Kernel.Environment
• serverBaseExts : Array Lean.EnvExtensionState
• 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.

• asyncConstsMap : VisibilityMap AsyncConsts
• asyncCtx? : Option AsyncContext
• importRealizationCtx? : Option RealizationContext
• localRealizationCtxMap : Lean.NameMap RealizationContext
• allRealizations : Task (Lean.NameMap AsyncConst)
• isExporting : Bool

  Indicates whether the environment is being used in an exported context, i.e. whether it should provide access to only the data to be imported by other modules participating in the module system. Apart from controlling access, some operations such as mkAuxDeclName may also change their output based on this flag.

  By default, isExporting is set to false when command elaborators are invoked such that they have access to the full local environment. Use with(out)Exporting to modify based on context. For example, elabDeclaration sets it based on (← getScope).isPublic on the top level, then elabMutualDef may switch from public to private when e.g. entering the proof of a theorem.

• isRecordingDeps : Bool

  Mirrors Lean.Core.Context.isRecordingDeps for pure extension reads, which cannot see the context: while set, a generation-tracked extension must be read with (genRecorded := true), by which the caller asserts that it recorded the generation (Lean.recordExtGenAccess), and any other extension must have EnvExtension.logWrites; other reads panic.

• synthCacheRaw? : Option NonScalar
• declChangeLog : DeclChangeLog

  Log of declaration-keyed state changes some recording computation could have observed (logDeclChange): a write about a declaration is appended when the declaration was added before the latest recording started (recordingConstGen), as writes about younger declarations cannot invalidate a recorded result. A recorded result is validated against the entries appended since it was recorded (checkDeclChangeLog); reducibility changes are the most common source.

• recordingConstGen : Nat

  constGen when a recording computation last started on this branch, or a later value carried over a rollback (raiseRecordingConstGen); see declChangeLog.

• constAddedGens : PHashMap Name Nat

  For each constant added on this environment branch, the constGen at which it became observable here (synchronous addDecl, asynchronous registration, merged realizations); see constAddedGen.

• constGen : Nat

  Counter bumped by every constant added on this environment branch: a consumer capturing it at some point knows that a constant with a larger constAddedGen did not exist then.

instance Lean.instNonemptyEnvironment : Nonempty Environment

def Lean.Environment.trackedGen (env : Environment) : Nat

Counter bumped by every modification of a generation-tracked extension (PersistentEnvExtensionDescrCore.trackGen): while it is unchanged, no such extension has changed. Like the generations, it rolls back with the environment, so after a rollback a different modification can reach a value seen before. Results stored in the environment roll back with it and stay sound. As the counter only grows along one environment branch, a result stored outside the environment stays sound across a rollback only if it was stamped with at most the restored value; later ones must be dropped.

Equations

• env.trackedGen = (Lean.VisibilityMap.private✝ (Lean.Environment.base✝ env)).trackedGen

def Lean.Environment.header (env : Environment) : EnvironmentHeader

Equations

• env.header = (Lean.VisibilityMap.private✝ (Lean.Environment.base✝ env)).header

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

Equations

• env.imports = env.header.imports

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

Equations

• env.allImportedModuleNames = env.header.moduleNames

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

Constructs an elaboration environment from a given kernel environment's constants. All constants are accessible in both the private and public scope. All other data is empty.

Equations

• Lean.Environment.ofKernelEnv env = { base := { «private» := env, «public» := env }, importRealizationCtx? := none }

@[export lean_elab_environment_to_kernel_env]

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

Equations

• env.toKernelEnv = env.checked.get

def Lean.Environment.setExporting (env : Environment) (isExporting : Bool) : Environment

Updates env.isExporting. Ignored if env.header.isModule is false.

Equations

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

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

Registers n as added now on this environment branch, unless it already was: a constant announced by addConstAsync keeps the generation of its announcement when its asynchronous branch adds it.

Equations

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

def Lean.Environment.constAddedGen (env : Environment) (n : Name) : Nat

The constGen at which n was added on this branch. Constants not registered, in particular imported ones, have generation 0, i.e. are treated as older than anything a consumer captured. For caching that is a conservative approximation as lower generation numbers lead to more cache misses.

Equations

• env.constAddedGen n = (Lean.PersistentHashMap.find? env.constAddedGens n).getD 0

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

Records a change of the declaration-keyed state about declName in Environment.declChangeLog, if some recording computation could have observed the previous state. Callers invoke this only for writes that change observable state.

Equations

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

def Lean.Environment.checkDeclChangeLog (env : Environment) (fromPos baseConstGen : Nat) : Bool

Returns whether a result recorded at log position fromPos when constGen was baseConstGen is still valid: every change logged since must be about a declaration added after that point.

Equations

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

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

Notes that a recording computation starts on this branch; see Environment.declChangeLog.

Equations

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

def Lean.Environment.raiseRecordingConstGen (env : Environment) (gen : Nat) : Environment

Raises recordingConstGen to at least gen. A rollback of the environment restores an earlier recording start, while results recorded since may survive it; carrying the later start over keeps changes to the declarations they could have observed logged.

Equations

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

def Lean.Environment.setRecordingDeps (env : Environment) (recording : Bool) : Environment

Updates Environment.isRecordingDeps.

Equations

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

def Lean.Environment.asyncPrefix? (env : Environment) : Option Name

The declaration prefix to which the environment is restricted to, if any.

Equations

• env.asyncPrefix? = Option.map (fun (x : Lean.AsyncContext✝) => Lean.AsyncContext.declPrefix✝ x) (Lean.Environment.asyncCtx?✝ env)

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

True while inside realizeConst's realize.

Equations

• env.isRealizing = Option.any (fun (x : Lean.AsyncContext✝) => !(Lean.AsyncContext.realizingStack✝ x).isEmpty) (Lean.Environment.asyncCtx?✝ env)

def Lean.Environment.importEnv? (env : Environment) : Option Environment

Returns the environment just after importing. none if finalizeImport has never been called on it.

Equations

• env.importEnv? = Lean.Environment.importEnv?.unsafe_impl_2✝ env

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

Forgets about the asynchronous context restrictions. Used only for withoutModifyingEnv.

Equations

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

def Lean.Environment.addDeclCore (env : Environment) (maxHeartbeats maxRecDepth : 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) : ConstMap

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.findAsync? (env : Environment) (n : Name) (skipRealize : Bool := false) : Option AsyncConstantInfo

Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration tasks unless necessary. This can usually be done efficiently because addConstAsync ensures that declarations added in an environment branch have that branch's declaration name as a prefix, so we know exactly what tasks to wait for to find a declaration. However, this is not true for declarations from realizeConst, which are not restricted to the current prefix, and reference to which may escape the branch(es) they have been realized on such as when looking into the type Expr of a declaration found on another branch. Thus when we cannot find the declaration using the fast prefix-based lookup, we fall back to waiting for and looking at the realizations from all branches. To avoid this expensive search for realizations from other branches, skipRealize can be set to ensure negative lookups are as fast as positive ones.

Use findTask instead if any blocking should be avoided.

Equations

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

def Lean.Environment.findTask (env : Environment) (n : Name) (skipRealize : Bool := false) : Task (Option AsyncConstantInfo)

Like findAsync? but returns a task instead of resorting to blocking.

Equations

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

def Lean.Environment.findConstVal? (env : Environment) (n : Name) (skipRealize : Bool := false) : Option ConstantVal

Like findAsync but blocks on everything but the constant's body (if any), which is not accessible through the result.

Equations

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

def Lean.Environment.find? (env : Environment) (n : Name) (skipRealize : Bool := false) : Option ConstantInfo

Like findAsync?, but blocks until the constant's info is fully available.

Equations

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

def Lean.Environment.hasExposedBody (env : Environment) (n : Name) : Bool

Checks if, in the public scope (Environment.isExporting), the given name refers to a definition with a visible body, i.e. ConstantInfo.hasValue. Recall that outside the module system, this is any definition.

Equations

• env.hasExposedBody n = Option.any (fun (x : Lean.ConstantInfo) => x.hasValue) ((env.setExporting true).find? n)

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

Equations

• env.getModuleIdxFor? declName = (Lean.VisibilityMap.get✝ (Lean.Environment.base✝ env) env).const2ModIdx[declName]?

def Lean.Environment.isImportedConst (env : Environment) (declName : Name) : Bool

Equations

• env.isImportedConst declName = (env.getModuleIdxFor? declName).isSome

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 before the declaration is actually added to the environment, we cannot automatically check that it isn't otherwise called too early in the sense that helper declarations and environment extension state that may be relevant to realizations may not have been added yet. We do check that we are not calling it from a different branch than c was added on, which would be definitely too late. Thus, this function should generally be called in elaborators calling addDecl (when that declaration is a plausible target for realization) at the latest possible point, i.e. at the very end of the elaborator or just before a first realization may be triggered if any.

Equations

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

def Lean.Environment.areRealizationsEnabledForConst (env : Environment) (c : Name) : Bool

Equations

• env.areRealizationsEnabledForConst c = (env.isImportedConst c || (Lean.Environment.localRealizationCtxMap✝ env).contains c)

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

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) : BaseIO String

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 : Type

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.realizingStack (env : Environment) : List Name

Equations

• env.realizingStack = (Option.map (fun (x : Lean.AsyncContext✝) => Lean.AsyncContext.realizingStack✝ x) (Lean.Environment.asyncCtx?✝ env)).getD []

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) : BaseIO Unit

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 : Type

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
• exportedKind? : Option Lean.ConstantKind
• sigPromise : IO.Promise Lean.ConstantVal
• constPromise : IO.Promise ConstPromiseVal
• checkedEnvPromise : IO.Promise Lean.Kernel.Environment
• allRealizationsPromise : IO.Promise (Lean.NameMap AsyncConst)

def Lean.Environment.addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (exportedKind? : Option ConstantKind := some kind) (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.

exportedKind? must be passed if the eventual kind of the constant in the exported constant map will differ from that of the private version. It must be none if the constant will not be exported.

Equations

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

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

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? exportedInfo? : Option ConstantInfo := none) : IO Unit

Commits the full constant info as well as the current environment extension state and set of nested asynchronous constants 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) : IO Unit

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, (asynchronously) 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) (skipRealize : Bool := true) : Bool

Checks whether findAsync? would return a result.

NOTE: Unlike findAsync, this function defaults skipRealize to true to avoid unnecessary blocking on realizations, which should always be brought into scope by running realizeConst, which does its own, optimized existence check.

Equations

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

def Lean.Environment.containsOnBranch (env : Environment) (n : Name) : Bool

Checks whether the given declaration is known on the current branch, in which case findAsync? will not block.

Equations

• env.containsOnBranch n = ((Lean.AsyncConsts.find?✝ (Lean.Environment.asyncConsts✝ env) n).isSome || Lean.SMap.contains (Lean.VisibilityMap.get✝ (Lean.Environment.base✝ env) env).constants n)

def Lean.Environment.realizationEnvContains (env : Environment) (forConst c : Name) : Bool

Returns whether realizeConst forConst callbacks can access c in the private scope, i.e. whether c is part of the realization environment of forConst. Returns false if realizations for forConst are not enabled on the current environment branch. Like contains, may block on asynchronous elaboration.

Use this to choose forConst when a realization depends on two (or more) constants: a correct target is one whose realization environment contains all others.

Equations

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

def Lean.Environment.getLocalConstantInfos (env : Environment) (skipTheoremSubDecls : Bool := false) : BaseIO (Array AsyncConstantInfo)

Returns the constants added in the current module, in elaboration tree pre-order: the top-level declarations in elaboration order, each followed by its asynchronous sub-declarations, recursively. The recursive part can optionally be skipped for theorems for when their sub-decls are unimportant and visiting them would only add latency by having to wait for proof elaboration to finish.

Unlike iterating env.constants.map₂, this does not block on env.checked, i.e. kernel checking.

Equations

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

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

Equations

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

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

Equations

• env.mainModule = env.header.mainModule

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

Equations

• env.isConstructor declName = Option.any (fun (x : Lean.AsyncConstantInfo) => x.kind == Lean.ConstantKind.ctor) (env.findAsync? declName)

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

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 = (Lean.EnvironmentHeader.moduleName2Idx✝ env.header)[moduleName]?

def Lean.ConstantVal.instantiateTypeLevelParams (c : ConstantVal) (ls : List Level) : Expr

Equations

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

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

Equations

• c.instantiateTypeLevelParams ls = c.toConstantVal.instantiateTypeLevelParams ls

def Lean.ConstantInfo.instantiateValueLevelParams! (c : ConstantInfo) (ls : List Level) (allowOpaque : Bool := false) : Expr

Equations

• c.instantiateValueLevelParams! ls allowOpaque = (c.value! allowOpaque).instantiateLevelParams c.levelParams ls

inductive Lean.AsyncBranch : Type

Branch specification for asynchronous environment extension access.

Note: For declarations not created via addConstAsync, including those created via realizeConst, the two specifiers are equivalent.

• mainEnv : AsyncBranch

  The main branch that initiated adding a declaration, i.e. AddConstAsyncResult.mainEnv.

  This is the more common case and true for e.g. all accesses from attributes.

• asyncEnv : AsyncBranch

  The async branch that finished adding a declaration, i.e. AddConstAsyncResult.asyncEnv.

def Lean.instBEqAsyncBranch.beq : AsyncBranch → AsyncBranch → Bool

Equations

• Lean.instBEqAsyncBranch.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Lean.instBEqAsyncBranch : BEq AsyncBranch

Equations

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

inductive Lean.EnvExtension.AsyncMode : Type

Async access mode for environment extensions used in EnvExtension.get/set/modifyState. When modified in concurrent contexts, extensions may need to switch to a different mode than the default mainOnly, which will panic in such cases. The access mode is set at environment extension registration time but can be overridden when calling the mentioned functions 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 (asyncMode := .sync) called on the main environment branch at the end of the file, i.e. it encompasses all modifications on all branches except for local modifications for which only the main branch is included.

• sync : AsyncMode

  Safest access mode, writes and reads 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 fallback for when mainOnly is not sufficient, 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

  Default access mode. 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 with local 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 (branch : AsyncBranch) : AsyncMode

  Accumulates modifications in the checked environment like sync, but get/modify/setState will panic instead of blocking unless their asyncDecl parameter is specified, which will access the state of the environment branch corresponding to the passed declaration name, if any; see AsyncBranch for a description of the specific state accessed. In other words, at most the environment branch corresponding to that declaration 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. In particular, this mode is closest to how the environment's own constant map works which provides findAsync? for block-avoiding access.

@[instance_reducible]

instance Lean.EnvExtension.instInhabitedAsyncMode : Inhabited AsyncMode

Equations

• Lean.EnvExtension.instInhabitedAsyncMode = { default := Lean.EnvExtension.instInhabitedAsyncMode.default }

@[reducible, inline]

abbrev Lean.ReplayFn (σ : Type) : Type

Equations

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

@[implemented_by _private.Lean.Environment.0.Lean.takeNewEntriesRevUnsafe]

def Lean.takeNewEntriesRev {α : Type u_1} (newEntries oldEntries : List α) : List α

Returns the entries newEntries has in front of its suffix oldEntries, oldest first.

This is intended for ReplayFn implementations of extensions that record entries in a list, where newEntries is oldEntries with the entries added in the meantime consed on. The suffix is found by pointer equality, so the cost is proportional to the number of new entries rather than to the number of all entries added in the current file; the latter matters because every realization replays every such extension. If oldEntries is not a physical suffix of newEntries, the leading newEntries.length - oldEntries.length entries are returned instead.

Equations

• Lean.takeNewEntriesRev newEntries oldEntries = (List.take (newEntries.length - oldEntries.length) newEntries).reverse

def Lean.takeNewEntries {α : Type u_1} (newEntries oldEntries : List α) : List α

Like takeNewEntriesRev, but returns the new entries in their order in newEntries.

Equations

• Lean.takeNewEntries newEntries oldEntries = (Lean.takeNewEntriesRev newEntries oldEntries).reverse

structure Lean.EnvExtension (σ : Type) : 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.

• name : Name

  Name for diagnostics; set automatically for persistent extensions.

• genIdx? : Option Nat

  For a generation-tracked extension (PersistentEnvExtensionDescrCore.trackGen), the index of its generation in Kernel.Environment.extGens.

• logWrites : Bool

  Whether writes are logged by declaration in Environment.declChangeLog, so that type class resolution may read the extension without recording the read: every write some recording computation could have observed is appended to the log. Hence each write must name its declaration or be marked unlogged; see EnvExtension.modifyState.

@[instance_reducible]

instance Lean.instInhabitedEnvExtension {a✝ : Type} : Inhabited (EnvExtension a✝)

Equations

• Lean.instInhabitedEnvExtension = { default := Lean.instInhabitedEnvExtension.default }

def Lean.EnvExtension.isGenTracked {σ : Type} (ext : EnvExtension σ) : Bool

Whether ext is generation-tracked; see PersistentEnvExtensionDescrCore.trackGen.

Equations

• ext.isGenTracked = ext.genIdx?.isSome

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

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.asyncMayModify {σ : Type} (ext : EnvExtension σ) (env : Environment) (asyncDecl : Name) (asyncMode : AsyncMode := ext.asyncMode) : Bool

Checks whether modifyState (asyncDecl := declName) may be called on an async environment extension; see AsyncMode.async for details.

Equations

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

inductive Lean.EnvExtension.WriteLog : Type

How a write to an extension is logged; see EnvExtension.modifyState.

• missing : WriteLog

  No declaration named; panics for an extension with logWrites.

• decl (declName : Name) : WriteLog

  Logs the write as a change of the state about declName (Environment.logDeclChange).

• unlogged : WriteLog

  Not logged, where no unlogged change can be observed; the call site should state why.

@[inline]

def Lean.EnvExtension.modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) (asyncMode : AsyncMode := ext.asyncMode) (asyncDecl : Name := Name.anonymous) (bumpGen : Bool := true) (log : WriteLog := WriteLog.missing) : Environment

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

For generation-tracked extensions the modification bumps the generation if bumpGen is set; see PersistentEnvExtensionDescrCore.trackGen. For an extension with logWrites, log must name the declaration the write is about, which logs it, or state .unlogged; otherwise the write panics.

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.
• ext.modifyState env f asyncMode asyncDecl bumpGen Lean.EnvExtension.WriteLog.unlogged = Lean.EnvExtension.modifyStateCore✝ ext env f asyncMode asyncDecl bumpGen

@[inline]

def Lean.EnvExtension.setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) (asyncMode : AsyncMode := ext.asyncMode) (log : WriteLog := WriteLog.missing) : Environment

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 asyncMode log = ext.modifyState env (fun (x : σ) => s) asyncMode Lean.Name.anonymous true log

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

opaque Lean.EnvExtension.getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) (asyncMode : AsyncMode := ext.asyncMode) (asyncDecl : Name := Name.anonymous) (genRecorded : Bool := false) : σ

Returns the current extension state. See AsyncMode for details on how modifications from different environment branches are reconciled.

Overriding the extension's default AsyncMode is usually not recommended and should be considered only for important optimizations.

genRecorded asserts that the caller recorded the extension's generation in the current recording computation (Lean.recordExtGenAccess), which reading a generation-tracked extension while Environment.isRecordingDeps is set requires.

def Lean.EnvExtension.getGenAt (env : Environment) (genIdx : Nat) : Nat

Generation of the generation-tracked extension with index genIdx (EnvExtension.genIdx?) on the current branch of env.

Equations

• Lean.EnvExtension.getGenAt env genIdx = (Lean.Kernel.Environment.extGens✝ (Lean.VisibilityMap.private✝ (Lean.Environment.base✝ env)))[genIdx]!

def Lean.EnvExtension.getGen {σ : Type} (ext : EnvExtension σ) (env : Environment) : Nat

Generation of the generation-tracked extension ext on the current branch of env.

Equations

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

def Lean.registerEnvExtension {σ : Type} (mkInitial : IO σ) (replay? : Option (ReplayFn σ) := none) (asyncMode : EnvExtension.AsyncMode := EnvExtension.AsyncMode.mainOnly) (name : Name := by exact decl_name%) (trackGen logWrites : Bool := false) : 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.

trackGen makes the extension generation-tracked; see PersistentEnvExtensionDescrCore.trackGen.

Equations

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

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

Equations

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

structure Lean.PersistentEnvExtensionState (α σ : Type) : Type

• importedEntries : Array (Array α)
• state : σ

structure Lean.ImportM.Context : Type

• env : Environment
• opts : Options

@[reducible, inline]

abbrev Lean.ImportM (α : Type) : Type

Equations

• Lean.ImportM = ReaderT Lean.ImportM.Context IO

inductive Lean.OLeanLevel : Type

The level of information to save/load. Each level includes all previous ones.

• exported : OLeanLevel

  Information from exported contexts.

• server : OLeanLevel

  Environment extension state for the language server.

• private : OLeanLevel

  Private module data.

@[instance_reducible]

instance Lean.instDecidableEqOLeanLevel : DecidableEq OLeanLevel

Equations

• Lean.instDecidableEqOLeanLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Lean.instOrdOLeanLevel : Ord OLeanLevel

Equations

• Lean.instOrdOLeanLevel = { compare := Lean.instOrdOLeanLevel.ord }

def Lean.instOrdOLeanLevel.ord : OLeanLevel → OLeanLevel → Ordering

Equations

• Lean.instOrdOLeanLevel.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

def Lean.instReprOLeanLevel.repr : OLeanLevel → Nat → Format

Equations

• Lean.instReprOLeanLevel.repr Lean.OLeanLevel.exported prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.OLeanLevel.exported")).group prec✝
• Lean.instReprOLeanLevel.repr Lean.OLeanLevel.server prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.OLeanLevel.server")).group prec✝
• Lean.instReprOLeanLevel.repr Lean.OLeanLevel.private prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Lean.OLeanLevel.private")).group prec✝

@[instance_reducible]

instance Lean.instReprOLeanLevel : Repr OLeanLevel

Equations

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

@[instance_reducible]

instance Lean.instLEOLeanLevel : LE OLeanLevel

Equations

• Lean.instLEOLeanLevel = leOfOrd

@[instance_reducible]

instance Lean.instLTOLeanLevel : LT OLeanLevel

Equations

• Lean.instLTOLeanLevel = ltOfOrd

structure Lean.OLeanEntries (α : Type) : Type

Data computed once per extension for all three olean levels. Avoids calling the export function three separate times so that expensive computations can be shared.

• exported : α
• server : α
• private : α

@[instance_reducible]

instance Lean.instInhabitedOLeanEntries {a✝ : Type} [Inhabited a✝] : Inhabited (OLeanEntries a✝)

Equations

• Lean.instInhabitedOLeanEntries = { default := Lean.instInhabitedOLeanEntries.default }

def Lean.OLeanEntries.uniform {α : Type} (a : α) : OLeanEntries α

Create OLeanEntries with the same value for all levels.

Equations

• Lean.OLeanEntries.uniform a = { exported := a, server := a, «private» := a }

def Lean.OLeanEntries.get {α : Type} (e : OLeanEntries α) : OLeanLevel → α

Look up the entry for a given level.

Equations

• e.get Lean.OLeanLevel.exported = e.exported
• e.get Lean.OLeanLevel.server = e.server
• e.get Lean.OLeanLevel.private = e.private

structure Lean.PersistentEnvExtension (α β σ : Type) : 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 : Environment → σ → OLeanEntries (Array α)

  Function to transform state into data that should be imported into other modules. Returns entries for all three olean levels at once so that expensive computations can be shared. When using the module system without import all, OLeanLevel.exported is imported, else OLeanLevel.private. Additionally, when using the module system in the language server, the OLeanLevel.server data is accessible via getModuleEntries (level := .server). By convention, each level should include all data of previous levels.

  This function is run once after elaborating the file and joining all asynchronous threads. For non-module files, only the private field is used.

• statsFn : σ → Format

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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) (level : OLeanLevel := OLeanLevel.exported) : Array α

Returns the data saved by ext.exportEntriesFn when m was elaborated. See docs on the function for details. When using the module system, level can be used to select the level of data to retrieve, but is limited to the maximum level actually imported: exported on the cmdline and server in the language server. Higher levels will return the data of the maximum imported level.

Equations

• ext.getModuleEntries env m = Lean.PersistentEnvExtension.getModuleEntries.unsafe_impl_2✝ ext m (Lean.Kernel.Environment.extensions✝ (Lean.VisibilityMap.private✝ (Lean.Environment.base✝ env)))
• ext.getModuleEntries env m level = Lean.PersistentEnvExtension.getModuleEntries.unsafe_impl_2✝ ext m (Lean.Environment.serverBaseExts✝ env)

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

Retrieves additional IR extension state for the interpreter.

Equations

• ext.getModuleIREntries env m = Lean.PersistentEnvExtension.getModuleIREntries.unsafe_impl_2✝ ext env m

@[inline]

def Lean.PersistentEnvExtension.addEntry {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (b : β) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := Name.anonymous) (log : EnvExtension.WriteLog := EnvExtension.WriteLog.missing) : Environment

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) (asyncDecl : Name := Name.anonymous) (genRecorded : Bool := false) : σ

Get the current state of the given extension in the given environment. For genRecorded, see EnvExtension.getState.

Equations

• ext.getState env asyncMode asyncDecl genRecorded = (ext.toEnvExtension.getState env asyncMode asyncDecl genRecorded).state

@[inline]

def Lean.PersistentEnvExtension.setState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (s : σ) (log : EnvExtension.WriteLog := EnvExtension.WriteLog.missing) : Environment

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

Equations

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

@[inline]

def Lean.PersistentEnvExtension.modifyState {α β σ : Type} (ext : PersistentEnvExtension α β σ) (env : Environment) (f : σ → σ) (asyncMode : EnvExtension.AsyncMode := ext.toEnvExtension.asyncMode) (asyncDecl : Name := Name.anonymous) (bumpGen : Bool := true) (log : EnvExtension.WriteLog := EnvExtension.WriteLog.missing) : Environment

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

Equations

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

opaque Lean.persistentEnvExtensionsRef : IO.Ref (Array (PersistentEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState))

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

• name : Name
• mkInitial : IO σ
• addImportedFn : Array (Array α) → ImportM σ
• addEntryFn : σ → β → σ
• exportEntriesFnEx : Environment → σ → OLeanEntries (Array α)

  Function to transform state into data that should be imported into other modules. Returns entries for all three olean levels at once so that expensive computations can be shared. When using the module system without import all, OLeanLevel.exported is imported, else OLeanLevel.private. Additionally, when using the module system in the language server, the OLeanLevel.server data is accessible via getModuleEntries (level := .server). By convention, each level should include all data of previous levels.

  This function is run once after elaborating the file and joining all asynchronous threads. For non-module files, only the private field is used.

• statsFn : σ → Format
• asyncMode : EnvExtension.AsyncMode
• replay? : Option (ReplayFn σ)
• trackGen : Bool

  Whether the extension is generation-tracked: every modification bumps its generation (EnvExtension.getGen), so that a result computed from the state can be validated later by comparing generations. Generation-tracked extensions must use AsyncMode.local or .mainOnly, as generations are branch-local.

  Generations only grow along an environment branch, even when a modification restores an earlier state: returning to an earlier generation would let a later, different modification reach a generation some result was recorded at, validating it against a state it never saw. The environment itself rolling back to an earlier generation is covered at Kernel.Environment.trackedGen.

• logWrites : Bool

  See EnvExtension.logWrites.

def Lean.useDefaultIfOtherFieldGiven {α : Sort u_1} {β : Sort u_2} (default : α) (_otherField : β) : α

Auxiliary function to signal to the structure instance elaborator that default should be used as the default value for a field but only if _otherField has been given, which is added as an artificial dependency.

Equations

• Lean.useDefaultIfOtherFieldGiven default _otherField = default

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

• name : Name
• mkInitial : IO σ
• addImportedFn : Array (Array α) → ImportM σ
• addEntryFn : σ → β → σ
• exportEntriesFnEx : Environment → σ → OLeanEntries (Array α)
• statsFn : σ → Format
• asyncMode : EnvExtension.AsyncMode
• replay? : Option (ReplayFn σ)
• trackGen : Bool
• logWrites : Bool
• exportEntriesFn : σ → Array α

  Obsolete simpler version of exportEntriesFnEx that returns the same entries for all levels. Its value is ignored if the latter is also specified.

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.saveModuleDataParts (mod : Name) (parts : Array (System.FilePath × ModuleData)) : IO Unit

Stores each given module data in the respective file name. Objects shared with prior parts are not duplicated. Thus the data cannot be loaded with individual readModuleData calls but must loaded by passing (a prefix of) the file names to readModuleDataParts. mod is used to determine an arbitrary but deterministic base address for mmap.

Equations

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

def Lean.readModuleDataParts (fnames : Array System.FilePath) : IO (Array (ModuleData × CompactedRegion))

Loads the module data from the given file names. The files must be (a prefix of) the result of a saveModuleDataParts call.

Equations

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

def Lean.saveModuleData (fname : System.FilePath) (mod : Name) (data : ModuleData) : IO Unit

Equations

• Lean.saveModuleData fname mod data = do let _ ← Lean.saveModuleData.unsafe_impl_2✝ fname mod data pure ()

def Lean.readModuleData (fname : System.FilePath) : IO (ModuleData × CompactedRegion)

Equations

• Lean.readModuleData fname = Lean.readModuleData.unsafe_impl_2✝ fname

@[noinline, export lean_environment_free_regions]

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

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.OLeanLevel.adjustFileName (base : System.FilePath) : OLeanLevel → System.FilePath

Equations

• Lean.OLeanLevel.adjustFileName base Lean.OLeanLevel.exported = base
• Lean.OLeanLevel.adjustFileName base Lean.OLeanLevel.server = base.addExtension "server"
• Lean.OLeanLevel.adjustFileName base Lean.OLeanLevel.private = base.addExtension "private"

def Lean.mkModuleData (env : Environment) (level : OLeanLevel := OLeanLevel.private) (extEntries? : Option (OLeanEntries (Array (Name × Array EnvExtensionEntry))) := none) : IO ModuleData

Equations

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

def Lean.writeModule (env : Environment) (fname : System.FilePath) (writeIR : Bool := true) : IO Unit

Equations

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

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 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 lean_get_num_attributes]

opaque Lean.getNumBuiltinAttributes : IO Nat

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

structure Lean.ImportState : Type

• moduleNameMap : Std.HashMap Lean.Name ImportedModule
• moduleNames : Array Lean.Name

@[instance_reducible]

instance Lean.instInhabitedImportState : Inhabited ImportState

Equations

• Lean.instInhabitedImportState = { default := Lean.instInhabitedImportState.default }

def Lean.ImportState.markAllExported (self : ImportState) : ImportState

Bumps all modules' isExported flag to true, intended for use in shake only.

Equations

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

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) : Type

Equations

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

@[inline]

def Lean.ImportStateM.run {α : Type} (x : ImportStateM α) (s : ImportState := default) : IO (α × ImportState)

Equations

• x.run s = StateRefT'.run x s

def Lean.importModulesCore (imports : Array Import) (globalLevel : OLeanLevel := OLeanLevel.private) (arts : NameMap ImportArtifacts := ∅) (isExported : Bool := decide (globalLevel < OLeanLevel.private)) (loadIRSig : Bool := false) : ImportStateM Unit

Equations

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

def Lean.finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (leakEnv loadExts : Bool) (level : OLeanLevel := OLeanLevel.private) (isModule : Bool := level != OLeanLevel.private) (loadIRSig : Bool := false) : IO Environment

Constructs environment from importModulesCore results.

See also importModules for parameter documentation.

Equations

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

def Lean.importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) (plugins : Array Plugin := #[]) (leakEnv loadExts : Bool := false) (level : OLeanLevel := OLeanLevel.private) (arts : NameMap ImportArtifacts := ∅) : IO Environment

Creates environment object from given imports.

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

If loadExts is true, we initialize the environment extensions using the imported data. Doing so may use the interpreter and thus is only safe to do after calling enableInitializersExecution; see also caveats there. If not set, every extension will have its initial value as its state. While the environment's constant map can be accessed without loadExts, many functions that take Environment or are in a monad carrying it such as CoreM may not function properly without it.

If level is exported, the module to be elaborated is assumed to be participating in the module system and imports will be restricted accordingly. If it is server, the data for getModuleEntries (includeServer := true) is loaded as well. If it is private, all data is loaded as if no module annotations were present in the imports.

Equations

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

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

Creates environment object from imports and frees compacted regions after calling act. No live references to the environment object or imported objects may exist after act finishes. As this cannot be ruled out after loading environment extensions, importModules's loadExts is always unset using this function.

Equations

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

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) : Bool

Equations

• Lean.Kernel.isDiagnosticsEnabled env = (Lean.VisibilityMap.private✝ (Lean.Environment.base✝ env)).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) : Diagnostics

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.displayStats (env : Environment) : IO Unit

Equations

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

@[noinline]

unsafe def Lean.Environment.evalConst (α : Type) (env : Environment) (opts : Options) (constName : Name) (checkMeta : Bool := true) : Except String α

Evaluates 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.

If checkMeta is true (the default), the function checks that all referenced imported constants are marked or imported as meta or otherwise fails with an error. It should only be set to false in cases where it is acceptable for code to work only in the language server, where more IR is loaded, such as in #eval.

Equations

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

def Lean.Environment.replayConsts (dest oldEnv newEnv : Environment) (skipExisting : Bool := false) : BaseIO Environment

Replays the difference between newEnv and oldEnv onto dest: the set of constants in newEnv but not oldEnv and the environment extension state for extensions defining replay?. If skipExisting is true, constants that are already in dest are not added. If newEnv and dest are not derived from oldEnv, the result is undefined.

Equations

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

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) : Bool

Equations

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

def Lean.Environment.realizeValue {α : Type u_1} [BEq α] [Hashable α] [TypeName α] (env : Environment) (forConst : Name) (key : α) (realize : Environment → Options → BaseIO Dynamic) : IO Dynamic

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

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 × Task (Option Kernel.Exception) × Dynamic)

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

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) : Bool

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) : Type

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

def Lean.getMainModule {m : Type → Type} [Monad m] [MonadEnv m] : m Name

Returns the module name of the current file.

Equations

• Lean.getMainModule = do let __do_lift ← Lean.getEnv pure __do_lift.header.mainModule

@[instance_reducible, always_inline]

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

Equations

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

def Lean.withExporting {m : Type → Type} {α : Type} [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α) (isExporting : Bool := true) : m α

Sets Environment.isExporting to the given value while executing x. No-op if EnvironmentHeader.isModule is false.

Equations

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

def Lean.withoutExporting {m : Type → Type} {α : Type} [Monad m] [MonadEnv m] [MonadFinally m] [MonadOptions m] (x : m α) (when : Bool := true) : m α

If when is true, sets Environment.isExporting to false while executing x.

Equations

• Lean.withoutExporting x when = if when = true then Lean.withExporting x false else x

def Lean.mkDefinitionValInferringUnsafe {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.mkThmOrUnsafeDef {m : Type → Type} [Monad m] [MonadEnv m] (thm : TheoremVal) : m Declaration

Constructs a declaration from a theorem, resorting to an unsafe def if needed

Equations

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

opaque Lean.defHeightOverrideExt : EnvExtension (NameMap UInt32)

Environment extension for overriding the height that getMaxHeight assigns to a definition. This is consulted for all definitions regardless of their reducibility hints. Currently used by structural recursion to ensure that parent definitions get the correct height even though the _f helper definitions are marked as .abbrev (which getMaxHeight would otherwise ignore).

def Lean.setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment

Register a height override for a definition so that getMaxHeight uses it.

Equations

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

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

Equations

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