Documentation

Lean.Environment

opaque Lean.EnvExtensionStateSpec :
(α : Type) ×

Opaque environment extension state.

Equations
Equations
@[inline]
Equations
• = midx
Equations
@[inline]
Equations
structure Lean.Import :
Instances For
Equations
Equations

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
@[extern lean_compacted_region_is_memory_mapped]
@[extern lean_compacted_region_free]

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

Opaque persistent environment extension entry.

• imports :
• 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

constNames :
• constants :
• 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.

extraConstNames :
• entries :

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

Instances For
Equations
• Lean.instInhabitedModuleData = { default := { imports := default, constNames := default, constants := default, extraConstNames := default, entries := default } }
• 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.

trustLevel : UInt32
• quotInit = true if the command init_quot has already been executed for the environment, and Quot declarations have been added to the environment.

quotInit : Bool
• Name of the module being compiled.

mainModule : Lean.Name
• Direct imports

imports :
• Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management.

regions :
• Name of all imported modules (directly and indirectly).

moduleNames :
• Module data for all imported modules.

moduleData :

Environment fields that are not used often.

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

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

constants : Lean.ConstMap
• Environment extensions. It also includes user-defined extensions.

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

extraConstNames : Lean.NameSet

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.

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

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.
@[export lean_environment_find]
Equations
Equations
Equations
@[export lean_environment_set_main_module]
Equations
• One or more equations did not get rendered due to their size.
@[export lean_environment_main_module]
Equations
Equations
Equations
Equations

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

Instances For

Type check given declaration and add it to the environment

Equations
• ext :
• inhabitedExt : {σ : Type} → Inhabited (ext σ)
• registerExt : {σ : Type} → IO σIO (ext σ)
• setState : {σ : Type} → ext σ
• modifyState : {σ : Type} → ext σLean.Environment(σσ) → Lean.Environment
• getState : {σ : Type} → [inst : ] → ext σ
• mkInitialExtStates :
• ensureExtensionsSize :

Interface for managing environment extensions.

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

Unsafe implementation of EnvExtensionInterface#

• idx : Nat
• mkInitial : IO σ
Instances For
Equations
• Lean.EnvExtensionInterfaceUnsafe.instInhabitedExt = { default := { idx := default, mkInitial := default } }

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
Equations
• One or more equations did not get rendered due to their size.
@[inline]
unsafe def Lean.EnvExtensionInterfaceUnsafe.modifyState {σ : Type} (ext : ) (env : Lean.Environment) (f : σσ) :
Equations
• One or more equations did not get rendered due to their size.
unsafe def Lean.EnvExtensionInterfaceUnsafe.getState {σ : Type} [inst : ] (ext : ) (env : Lean.Environment) :
σ
Equations
• One or more equations did not get rendered due to their size.
unsafe def Lean.EnvExtensionInterfaceUnsafe.registerExt {σ : Type} (mkInitial : IO σ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by Lean.EnvExtensionInterfaceUnsafe.imp]
Equations
Equations
• Lean.EnvExtension.instInhabitedEnvExtension =
Equations
def Lean.EnvExtension.modifyState {σ : Type} (ext : ) (env : Lean.Environment) (f : σσ) :
Equations
def Lean.EnvExtension.getState {σ : Type} [inst : ] (ext : ) (env : Lean.Environment) :
σ
Equations
def Lean.registerEnvExtension {σ : Type} (mkInitial : IO σ) :

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
@[export lean_mk_empty_environment]
def Lean.mkEmptyEnvironment (trustLevel : ) :
Equations
• One or more equations did not get rendered due to their size.
• importedEntries : Array ()
• state : σ
Instances For
@[inline]
abbrev Lean.ImportM (α : Type) :
Equations
structure Lean.PersistentEnvExtension (α : Type) (β : Type) (σ : Type) :
• toEnvExtension :
• name : Lean.Name
• exportEntriesFn : σ
• statsFn :

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.

Remark: for most extensions α and β coincide.

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


without using IO. We have many functions like addAlias.

α and ‵β do not coincide for extensions where the data used to update the state contains, for example, closures which we currently cannot store in files.

Instances For
instance Lean.instInhabitedPersistentEnvExtensionState {α : Type} {σ : Type} [inst : ] :
Equations
• Lean.instInhabitedPersistentEnvExtensionState = { default := { importedEntries := #[], state := default } }
instance Lean.instInhabitedPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
def Lean.PersistentEnvExtension.getModuleEntries {α : Type} {β : Type} {σ : Type} [inst : ] (ext : ) (env : Lean.Environment) (m : Lean.ModuleIdx) :
Equations
def Lean.PersistentEnvExtension.addEntry {α : Type} {β : Type} {σ : Type} (ext : ) (env : Lean.Environment) (b : β) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.PersistentEnvExtension.getState {α : Type} {β : Type} {σ : Type} [inst : ] (ext : ) (env : Lean.Environment) :
σ

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

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

Set the current state of the given extension in the given environment. This change is not persisted across files.

Equations
def Lean.PersistentEnvExtension.modifyState {α : Type} {β : Type} {σ : Type} (ext : ) (env : Lean.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
structure Lean.PersistentEnvExtensionDescr (α : Type) (β : Type) (σ : Type) :
• name :
• mkInitial : IO σ
• exportEntriesFn : σ
• statsFn :
Instances For
unsafe def Lean.registerPersistentEnvExtensionUnsafe {α : Type} {β : Type} {σ : Type} [inst : ] (descr : ) :
IO ()
Equations
• One or more equations did not get rendered due to their size.
@[implemented_by Lean.registerPersistentEnvExtensionUnsafe]
opaque Lean.registerPersistentEnvExtension {α : Type} {β : Type} {σ : Type} [inst : ] (descr : ) :
IO ()

Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries.

Equations
@[specialize #[]]
def Lean.mkStateFromImportedEntries {α : Type} {σ : Type} (addEntryFn : σασ) (initState : σ) (as : Array ()) :
σ
Equations
• name :
• toArrayFn : List α
Instances For
def Lean.registerSimplePersistentEnvExtension {α : Type} {σ : Type} [inst : ] (descr : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
def Lean.SimplePersistentEnvExtension.getEntries {α : Type} {σ : Type} [inst : ] (ext : ) (env : Lean.Environment) :
List α

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

Equations
• = ().fst
def Lean.SimplePersistentEnvExtension.getState {α : Type} {σ : Type} [inst : ] (ext : ) (env : Lean.Environment) :
σ

Get the current state of the given SimplePersistentEnvExtension.

Equations
• = ().snd

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

Equations

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

Equations

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

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

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

Equations
def Lean.mkMapDeclarationExtension {α : Type} [inst : ] (name : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• Lean.MapDeclarationExtension.instInhabitedMapDeclarationExtension =
def Lean.MapDeclarationExtension.insert {α : Type} (ext : ) (env : Lean.Environment) (declName : Lean.Name) (val : α) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.MapDeclarationExtension.find? {α : Type} [inst : ] (ext : ) (env : Lean.Environment) (declName : Lean.Name) :
Equations
• One or more equations did not get rendered due to their size.
def Lean.MapDeclarationExtension.contains {α : Type} [inst : ] (ext : ) (env : Lean.Environment) (declName : Lean.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 : Lean.Name) (data : Lean.ModuleData) :
@[noinline, export lean_environment_free_regions]

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
Equations
• One or more equations did not get rendered due to their size.
@[export lean_write_module]
Equations
@[extern 2 lean_update_env_attributes]

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

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

Instances For
def Lean.throwAlreadyImported {α : Type} (s : Lean.ImportState) (const2ModIdx : ) (modIdx : Nat) (cname : Lean.Name) :
IO α
Equations
• One or more equations did not get rendered due to their size.
@[export lean_import_modules]
def Lean.importModules (imports : ) (opts : Lean.Options) (trustLevel : ) :
Equations
• One or more equations did not get rendered due to their size.
unsafe def Lean.withImportModules {α : Type} (imports : ) (opts : Lean.Options) (trustLevel : ) (x : ) :
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

Environment extension for tracking all namespace declared by users.

Register a new namespace in the environment.

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

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

Equations

Return a set containing all namespaces in env.

Equations
Equations
@[export lean_display_stats]
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 : Lean.Environment) (opts : Lean.Options) (constName : Lean.Name) :

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 : Lean.Environment) (opts : Lean.Options) (typeName : Lean.Name) (constName : Lean.Name) :

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.
Equations
• One or more equations did not get rendered due to their size.

Kernel API #

@[extern lean_kernel_is_def_eq]

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.

Equations
@[extern lean_kernel_whnf]

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.

class Lean.MonadEnv (m : ) :
• getEnv :
• modifyEnv : () → m Unit
Instances
@[always_inline]
instance Lean.instMonadEnv (m : ) (n : ) [inst : ] [inst : ] :
Equations
• = { getEnv := liftM Lean.getEnv, modifyEnv := fun f => }