Opaque environment extension state.
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.
Instances For
Free a compacted region and its contents. No live references to the contents may exist at the time of invocation.
- imports : Array Lean.Import
constNames
contains all constant names inconstants
. This information is redundant. It is equal toconstants.map fun c => c.name
, but it improves the performance ofimportModules
.perf
reports that 12% of the runtime was being spent onConstantInfo.name
when importing a file containing onlyimport Lean
- constants : Array Lean.ConstantInfo
Extra entries for the
const2ModIdx
map in theEnvironment
object. The code generator creates auxiliary declarations that are not in the mappingconstants
, but we want to know in which module they were generated.- entries : Array (Lake.Name × Array Lean.EnvExtensionEntry)
Content of a .olean file.
We use compact.cpp
to generate the image of this object in disk.
Instances For
- 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.
- quotInit : Bool
- mainModule : Lake.Name
Name of the module being compiled.
- imports : Array Lean.Import
Direct imports
- regions : Array Lean.CompactedRegion
Compacted regions for all imported modules. Objects in compacted memory regions do no require any memory management.
Name of all imported modules (directly and indirectly).
- moduleData : Array Lean.ModuleData
Module data for all imported modules.
Environment fields that are not used often.
Instances For
- const2ModIdx : Lean.HashMap Lake.Name Lean.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 theModuleIdx
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. - constants : Lean.ConstMap
Mapping from constant name to
ConstantInfo
. It contains all constants (definitions, theorems, axioms, etc) that have been already type checked by the kernel. - extensions : Array Lean.EnvExtensionState
Environment extensions. It also includes user-defined extensions.
- extraConstNames : Lean.NameSet
Constant names to be saved in the field
extraConstNames
atModuleData
. It contains auxiliary declaration names created by the code generator which are not inconstants
. When importing modules, we want to insert them atconst2ModIdx
. - header : Lean.EnvironmentHeader
The header contains additional information that is not updated often.
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
Instances For
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.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
- unknownConstant: Lean.Environment → Lake.Name → Lean.KernelException
- alreadyDeclared: Lean.Environment → Lake.Name → Lean.KernelException
- declTypeMismatch: Lean.Environment → Lean.Declaration → Lean.Expr → Lean.KernelException
- declHasMVars: Lean.Environment → Lake.Name → Lean.Expr → Lean.KernelException
- declHasFVars: Lean.Environment → Lake.Name → Lean.Expr → Lean.KernelException
- funExpected: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
- typeExpected: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
- letTypeMismatch: Lean.Environment → Lean.LocalContext → Lake.Name → Lean.Expr → Lean.Expr → Lean.KernelException
- exprTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.KernelException
- appTypeMismatch: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.Expr → Lean.Expr → Lean.KernelException
- invalidProj: Lean.Environment → Lean.LocalContext → Lean.Expr → Lean.KernelException
- other: String → Lean.KernelException
- deterministicTimeout: Lean.KernelException
- excessiveMemory: Lean.KernelException
- deepRecursion: Lean.KernelException
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
Instances For
Instances For
- inhabitedExt : {σ : Type} → Inhabited σ → Inhabited (Lean.EnvExtensionInterface.ext s σ)
- registerExt : {σ : Type} → IO σ → IO (Lean.EnvExtensionInterface.ext s σ)
- setState : {σ : Type} → Lean.EnvExtensionInterface.ext s σ → Lean.Environment → σ → Lean.Environment
- modifyState : {σ : Type} → Lean.EnvExtensionInterface.ext s σ → Lean.Environment → (σ → σ) → Lean.Environment
- getState : {σ : Type} → [inst : Inhabited σ] → Lean.EnvExtensionInterface.ext s σ → Lean.Environment → σ
- mkInitialExtStates : IO (Array Lean.EnvExtensionState)
- ensureExtensionsSize : Lean.Environment → IO Lean.Environment
Interface for managing environment extensions.
Instances For
Unsafe implementation of EnvExtensionInterface
#
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 import
s.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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 import
s.
For that, you need to register a persistent environment extension.
Instances For
Instances For
- toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)
- name : Lake.Name
- addImportedFn : Array (Array α) → Lean.ImportM σ
- addEntryFn : σ → β → σ
- exportEntriesFn : σ → Array α
- statsFn : σ → Lean.Format
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 :=
aliasExtension.addEntry env (a, e)
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
Instances For
Instances For
Get the current state of the given extension in the given environment.
Instances For
Set the current state of the given extension in the given environment. This change is not persisted across files.
Instances For
Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.
Instances For
- name : Lake.Name
- mkInitial : IO σ
- addImportedFn : Array (Array α) → Lean.ImportM σ
- addEntryFn : σ → β → σ
- exportEntriesFn : σ → Array α
- statsFn : σ → Lean.Format
Instances For
Instances For
Simple PersistentEnvExtension
that implements exportEntriesFn
using a list of entries.
Instances For
Instances For
Get the list of values used to update the state of the given
SimplePersistentEnvExtension
in the current file.
Instances For
Get the current state of the given SimplePersistentEnvExtension
.
Instances For
Set the current state of the given SimplePersistentEnvExtension
. This change is not persisted across files.
Instances For
Modify the state of the given extension in the given environment by applying the given function. This change is not persisted across files.
Instances For
Environment extension for tagging declarations. Declarations must only be tagged in the module where they were declared.
Instances For
Instances For
Instances For
Instances For
Environment extension for mapping declarations to values. Declarations must only be inserted into the mapping in the module where they were declared.
Instances For
Instances For
Instances For
Instances For
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.
Instances For
Instances For
"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
.
"Forward declaration" for retrieving the number of builtin attributes.
- moduleNameSet : Lean.NameHashSet
- moduleData : Array Lean.ModuleData
- regions : Array Lean.CompactedRegion
Instances For
Instances For
Instances For
Instances For
Instances For
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.
Instances For
Environment extension for tracking all namespace
declared by users.
Register a new namespace in the environment.
Instances For
Return true
if n
is the name of a namespace in env
.
Instances For
Return a set containing all namespaces in env
.
Instances For
Instances For
Instances For
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.
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 α
.
Instances For
Kernel API #
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.
Instances For
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.
- getEnv : m Lean.Environment
- modifyEnv : (Lean.Environment → Lean.Environment) → m Unit