opaque Lean.diagnostics : Lean.Option Bool

opaque Lean.diagnostics.threshold : Lean.Option Nat

opaque Lean.maxHeartbeats : Lean.Option Nat

opaque Lean.Elab.async : Lean.Option Bool

opaque Lean.Elab.inServer : Lean.Option Bool

opaque Lean.internal.cmdlineSnapshots : Lean.Option Bool

Performance option used by cmdline driver.

def Lean.useDiagnosticMsg : MessageData

If the diagnostics option is not already set, gives a message explaining this option. Begins with a \n\n, so an error message can look like m!"some error occurred{useDiagnosticMsg}". The double newline gives better visual separation from the main error message

Equations

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

structure Lean.DeclNameGenerator : Type

Name generator that creates user-accessible names.

• namePrefix : Name
• idx : Nat
• parentIdxs : List Nat

@[instance_reducible]

instance Lean.instInhabitedDeclNameGenerator : Inhabited DeclNameGenerator

Equations

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

def Lean.DeclNameGenerator.ofPrefix (namePrefix : Name) : DeclNameGenerator

Equations

• Lean.DeclNameGenerator.ofPrefix namePrefix = { namePrefix := namePrefix }

def Lean.DeclNameGenerator.next (g : DeclNameGenerator) : DeclNameGenerator

Equations

• g.next = { namePrefix := g.namePrefix, idx := g.idx + 1, parentIdxs := g.parentIdxs }

def Lean.DeclNameGenerator.mkUniqueName (env : Environment) (g : DeclNameGenerator) («infix» : Name) : Name × DeclNameGenerator

Creates a user-accessible unique name of the following structure:

<name prefix>.<infix>_<numeric components>_...

Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other branching elaboration steps, mkChild must be used (automatically done in wrapAsync*).

Equations

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

def Lean.DeclNameGenerator.mkChild (g : DeclNameGenerator) : DeclNameGenerator × DeclNameGenerator

Equations

• g.mkChild = ({ namePrefix := g.namePrefix, parentIdxs := g.idx :: g.parentIdxs }, { namePrefix := g.namePrefix, idx := g.idx + 1, parentIdxs := g.parentIdxs })

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

• getDeclNGen : m DeclNameGenerator
• setDeclNGen : DeclNameGenerator → m Unit

@[instance_reducible]

instance Lean.instMonadDeclNameGeneratorOfMonadLift {m n : Type → Type} [MonadLift m n] [MonadDeclNameGenerator m] : MonadDeclNameGenerator n

Equations

• Lean.instMonadDeclNameGeneratorOfMonadLift = { getDeclNGen := liftM Lean.getDeclNGen, setDeclNGen := fun (ngen : Lean.DeclNameGenerator) => liftM (Lean.setDeclNGen ngen) }

def Lean.mkAuxDeclName {m : Type → Type} [Monad m] [MonadEnv m] [MonadDeclNameGenerator m] (kind : Name := `_aux) : m Name

Creates a new name for use as an auxiliary declaration that can be assumed to be globally unique.

Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other branching elaboration steps, mkChild must be used (automatically done in wrapAsync*).

Equations

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

def Lean.withDeclNameForAuxNaming {m : Type → Type} {α : Type} [Monad m] [MonadFinally m] [MonadDeclNameGenerator m] (name : Name) (x : m α) : m α

Adjusts the namePrefix of getDeclNGen to the given name and resets the nested counter.

Equations

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

structure Lean.OptionFlags : Type

Boolean options resolved eagerly into a single word, so that hot paths test a bit instead of looking the option up in a KVMap. The word is recomputed wherever the options change (withOptions and Core.Context.setOptions) and defaulted from them at construction; Core.Context.optionFlags_eq guarantees that it always agrees with the options in scope.

Bits 0 to 8 are the definitional-equality and unfolding compatibility flags read on every step of isDefEq and whnf. Bit 9 is diagnostics.

• bits : UInt16

@[instance_reducible]

instance Lean.instInhabitedOptionFlags : Inhabited OptionFlags

Equations

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

@[instance_reducible]

instance Lean.instBEqOptionFlags : BEq OptionFlags

Equations

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

def Lean.instBEqOptionFlags.beq : OptionFlags → OptionFlags → Bool

Equations

• Lean.instBEqOptionFlags.beq { bits := a } { bits := b } = (a == b)
• Lean.instBEqOptionFlags.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.instHashableOptionFlags : Hashable OptionFlags

Equations

• Lean.instHashableOptionFlags = { hash := Lean.instHashableOptionFlags.hash }

def Lean.instHashableOptionFlags.hash : OptionFlags → UInt64

Equations

• Lean.instHashableOptionFlags.hash { bits := a } = mixHash 0 (hash a)

@[inline]

def Lean.OptionFlags.respectTransparency (f : OptionFlags) : Bool

Equations

• f.respectTransparency = (Lean.OptionFlags.bits✝ f &&& 1 != 0)

@[inline]

def Lean.OptionFlags.respectTransparencyTypes (f : OptionFlags) : Bool

Equations

• f.respectTransparencyTypes = (Lean.OptionFlags.bits✝ f &&& 2 != 0)

@[inline]

def Lean.OptionFlags.respectTransparencyInstanceSearchTypes (f : OptionFlags) : Bool

Equations

• f.respectTransparencyInstanceSearchTypes = (Lean.OptionFlags.bits✝ f &&& 4 != 0)

@[inline]

def Lean.OptionFlags.implicitBump (f : OptionFlags) : Bool

Equations

• f.implicitBump = (Lean.OptionFlags.bits✝ f &&& 8 != 0)

@[inline]

def Lean.OptionFlags.reducibleClassField (f : OptionFlags) : Bool

Equations

• f.reducibleClassField = (Lean.OptionFlags.bits✝ f &&& 16 != 0)

@[inline]

def Lean.OptionFlags.lazyProjDelta (f : OptionFlags) : Bool

Equations

• f.lazyProjDelta = (Lean.OptionFlags.bits✝ f &&& 32 != 0)

@[inline]

def Lean.OptionFlags.lazyWhnfCore (f : OptionFlags) : Bool

Equations

• f.lazyWhnfCore = (Lean.OptionFlags.bits✝ f &&& 64 != 0)

@[inline]

def Lean.OptionFlags.smartUnfolding (f : OptionFlags) : Bool

Equations

• f.smartUnfolding = (Lean.OptionFlags.bits✝ f &&& 128 != 0)

@[inline]

def Lean.OptionFlags.throwOnStuckAfterApp (f : OptionFlags) : Bool

Equations

• f.throwOnStuckAfterApp = (Lean.OptionFlags.bits✝ f &&& 256 != 0)

@[inline]

def Lean.OptionFlags.diag (f : OptionFlags) : Bool

Equations

• f.diag = (Lean.OptionFlags.bits✝ f &&& 512 != 0)

def Lean.OptionFlags.ofOptions (opts : Options) : OptionFlags

Resolves the flags from opts.

The definitional-equality options are read by name because their declarations live in modules this one does not import.

Equations

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

structure Lean.RecordedDeps : Type

The dependencies observed by a recording computation, accumulated in Core.State.recordedDeps. A result cached by the computation stays valid as long as they give the same answers. Currently used by type class resolution, see Lean.Meta.SynthInstance.

• options : Array Name

  The names of the options looked up, deduplicated.

• base : Options

  The options in effect when recording started, against which a cached entry is later validated. A lookup answering differently was served by a write inside the computation (Lean.withSetOption), so it does not depend on the ambient options and is not recorded. The recorded answers are read from it, so a stored entry keeps it, restricted to the looked-up names.

• extGens : Array (Nat × Nat)

  The generation-tracked extensions read, as EnvExtension.genIdx? and observed generation.

• baseTrackedGen : Nat

  Environment.trackedGen when recording started, or when the dependencies were last validated. Together with baseChangeLogPos it is the stamp of the dependencies: as long as the environment's trackedGen and change log length still equal the stamp, none of the environment dependencies can have changed since then.

• baseChangeLogPos : Nat

  Length of Environment.declChangeLog when recording started, or when the dependencies were last validated; see baseTrackedGen.

• baseConstGen : Nat

  Environment.constGen when recording started. Environment.checkDeclChangeLog ignores the changes logged since baseChangeLogPos to declarations added after recording started, as the recorded computation cannot have observed them.

@[instance_reducible]

instance Lean.instInhabitedRecordedDeps : Inhabited RecordedDeps

Equations

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

def Lean.Core.getMaxHeartbeats (opts : Options) : Nat

Equations

• Lean.Core.getMaxHeartbeats opts = Lean.Option.get opts Lean.maxHeartbeats * 1000

@[reducible, inline]

abbrev Lean.Core.InstantiateLevelCache : Type

Equations

• Lean.Core.InstantiateLevelCache = Lean.PersistentHashMap Lean.Name (List Lean.Level × Lean.Expr)

structure Lean.Core.Cache : Type

Cache for the CoreM monad

• instLevelType : InstantiateLevelCache
• instLevelValue : InstantiateLevelCache

@[instance_reducible]

instance Lean.Core.instInhabitedCache : Inhabited Cache

Equations

• Lean.Core.instInhabitedCache = { default := Lean.Core.instInhabitedCache.default }

structure Lean.Core.State : Type

State for the CoreM monad.

• env : Environment

  Current environment.

• nextMacroScope : MacroScope

  Next macro scope. We use macro scopes to avoid accidental name capture.

• ngen : NameGenerator

  Name generator for producing unique FVarIds, MVarIds, and LMVarIds

• auxDeclNGen : DeclNameGenerator

  Name generator for creating persistent auxiliary declarations. Separate from ngen to keep numbers smaller and create user-accessible names.

• traceState : TraceState

  Trace messages

• cache : Cache

  Cache for instantiating universe polymorphic declarations.

• recordedDeps : RecordedDeps

  The dependencies observed by the recording computation, if enabled (Core.Context.isRecordingDeps); they become the dependency log of the cache entry it produces, see Lean.Meta.SynthInstanceCache. Not restored by SavedState.restore, so that dependencies observed on a rolled-back path are kept.

• messages : MessageLog

  Message log.

• infoState : Elab.InfoState

  Info tree. We have the info tree here because we want to update it while adding attributes.

• snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree)

  Snapshot trees of asynchronous subtasks. As these are untyped and reported only at the end of the command's main elaboration thread, they are only useful for basic message log reporting; for incremental reporting and reuse within a long-running elaboration thread, types rooted in CommandParsedSnapshot need to be adjusted.

instance Lean.Core.instNonemptyState : Nonempty State

structure Lean.Core.Context.Cold : Type

The pointer-typed fields of Core.Context that are not updated on a recursion or withRef step.

withReader can never reuse the Context record, so every withIncRecDepth and withRef pays one reference count increment per pointer field. Grouping the remaining fields into a subobject makes them cost a single increment together.

Rarely-updated fields in particular tend to be MT during async elaboration, which makes RC traffic elisions on them even more valueable, explaining an outsized task-clock vs instrs impact of this optimization.

• fileName : String

  Name of the file being compiled.

• fileMap : FileMap

  Auxiliary datastructure for converting String.Pos into Line/Column number.

• options : Options
• maxRecDepth : Nat
• currNamespace : Name
• openDecls : List OpenDecl
• initHeartbeats : Nat
• maxHeartbeats : Nat
• quotContext : Name
• currMacroScope : MacroScope
• cancelTk? : Option IO.CancelToken

  If set, used to cancel elaboration from outside when results are not needed anymore.

• inheritedTraceOptions : Std.HashSet Name

  Cache of Lean.inheritedTraceOptions.

instance Lean.Core.Context.instNonemptyCold : Nonempty Cold

structure Lean.Core.Context extends Lean.Core.Context.Cold : Type

Context for the CoreM monad.

• fileName : String
• fileMap : FileMap
• options : Options
• maxRecDepth : Nat
• currNamespace : Name
• openDecls : List OpenDecl
• initHeartbeats : Nat
• maxHeartbeats : Nat
• quotContext : Name
• currMacroScope : MacroScope
• cancelTk? : Option IO.CancelToken
• inheritedTraceOptions : Std.HashSet Name
• currRecDepth : Nat
• ref : Syntax
• optionFlags : OptionFlags

  Boolean options resolved from options; see Lean.OptionFlags.

• optionFlags_eq : self.optionFlags = OptionFlags.ofOptions self.options

  Enforces that optionFlags is always consistent with options.

• suppressElabErrors : Bool

  If set (when showPartialSyntaxErrors is not set and parsing failed), suppresses most elaboration errors; see also logMessage below.

• isRecordingDeps : Bool

  Whether the current computation records its dependencies into Core.State.recordedDeps. While set, reading state that is not recorded panics, see instance MonadOptions CoreM.

instance Lean.Core.instNonemptyContext : Nonempty Context

def Lean.Core.Context.setOptions (ctx : Context) (options : Options) : Context

Replaces the options, re-resolving the fields derived from them. Changing options directly leaves optionFlags behind, which optionFlags_eq rejects; use this instead.

Equations

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

@[reducible, inline]

abbrev Lean.Core.CoreM (α : Type) : Type

CoreM is a monad for manipulating the Lean environment. It is the base monad for MetaM. The main features it provides are:

• name generator state
• environment state
• Lean options context
• the current open namespace

Equations

• Lean.CoreM = ReaderT Lean.Core.Context (StateRefT' IO.RealWorld Lean.Core.State (EIO Lean.Exception))

@[instance_reducible, always_inline]

instance Lean.Core.instMonadCoreM : Monad CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instInhabitedCoreM {α : Type} : Inhabited (CoreM α)

Equations

• Lean.Core.instInhabitedCoreM = { default := fun (x : Lean.Core.Context) (x_1 : ST.Ref IO.RealWorld Lean.Core.State) => throw default }

@[instance_reducible]

instance Lean.Core.instMonadRefCoreM : MonadRef CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadEnvCoreM : MonadEnv CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadOptionsCoreM : MonadOptions CoreM

Equations

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

@[noinline]

def Lean.Core.instMonadOptionsCoreM.checkedOptions (ctx : Context) : Options

The options of ctx, panicking inside a recording computation. Out of line, as getOptions is inlined at every call site.

Equations

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

@[inline]

def Lean.Core.withOptionsUnrestricted {α : Type} (f : Options → Options) (x : CoreM α) : CoreM α

Applies f to the options in scope of x, without the recording check of withOptions. Each use must argue that f's result on an option read through Lean.getRecordedOption does not depend on the ambient options; Lean.withSetOption does so by construction.

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadWithOptionsCoreM : MonadWithOptions CoreM

Equations

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

@[noinline]

def Lean.Core.instMonadWithOptionsCoreM.reportViolation : Options → Options

Reports a withOptions call inside a recording computation and leaves the options unchanged. Out of line, as withOptions is inlined at every call site; it takes no argument so that f stays a known function there.

Equations

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

@[instance_reducible]

instance Lean.Core.instAddMessageContextCoreM : AddMessageContext CoreM

Equations

• Lean.Core.instAddMessageContextCoreM = { addMessageContext := Lean.addMessageContextPartial }

@[instance_reducible]

instance Lean.Core.instMonadNameGeneratorCoreM : MonadNameGenerator CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadDeclNameGeneratorCoreM : MonadDeclNameGenerator CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadRecDepthCoreM : MonadRecDepth CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadResolveNameCoreM : MonadResolveName CoreM

Equations

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

def Lean.Core.withFreshMacroScope {α : Type} (x : CoreM α) : CoreM α

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadQuotationCoreM : MonadQuotation CoreM

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadInfoTreeCoreM : Elab.MonadInfoTree CoreM

Equations

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

@[inline]

def Lean.Core.modifyCache (f : Cache → Cache) : CoreM Unit

Equations

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

@[inline]

def Lean.Core.modifyRecordedDeps (f : RecordedDeps → RecordedDeps) : CoreM Unit

Equations

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

@[inline]

def Lean.Core.modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit

Equations

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

@[inline]

def Lean.Core.modifyInstLevelValueCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit

Equations

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

def Lean.Core.instantiateTypeLevelParams (c : ConstantVal) (us : List Level) : CoreM Expr

Equations

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

def Lean.Core.instantiateValueLevelParams (c : ConstantInfo) (us : List Level) (allowOpaque : Bool := false) : CoreM Expr

Equations

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

@[inline]

def Lean.Core.liftIOCore {α : Type} (x : IO α) : CoreM α

Equations

• Lean.Core.liftIOCore x = do let ref ← Lean.getRef liftM (IO.toEIO (fun (err : IO.Error) => Lean.Exception.error ref ((Lean.MessageData.ofFormat ∘ Std.format) (toString err))) x)

@[instance_reducible]

instance Lean.Core.instMonadLiftIOCoreM : MonadLift IO CoreM

Equations

• Lean.Core.instMonadLiftIOCoreM = { monadLift := fun {α : Type} => Lean.Core.liftIOCore }

@[instance_reducible]

instance Lean.Core.instMonadTraceCoreM : MonadTrace CoreM

Equations

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

structure Lean.Core.SavedState extends Lean.Core.State : Type

• env : Environment
• nextMacroScope : MacroScope
• ngen : NameGenerator
• auxDeclNGen : DeclNameGenerator
• traceState : TraceState
• cache : Cache
• recordedDeps : RecordedDeps
• messages : MessageLog
• infoState : Elab.InfoState
• snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree)
• passedHeartbeats : Nat

  Number of heartbeats passed inside withRestoreOrSaveFull, not used otherwise.

instance Lean.Core.instNonemptySavedState : Nonempty SavedState

def Lean.Core.saveState : CoreM SavedState

Equations

• Lean.Core.saveState = do let s ← get pure { toState := s, passedHeartbeats := 0 }

@[specialize #[]]

def Lean.Core.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × SavedState)) (act : CoreM α) : CoreM (α × SavedState)

Incremental reuse primitive: if reusableResult? is none, runs act and returns its result together with the saved monadic state after act including the heartbeats used by it. If reusableResult? on the other hand is some (a, state), restores full state including heartbeats used and returns (a, state).

The intention is for steps that support incremental reuse to initially pass none as reusableResult? and store the result and state in a snapshot. In a further run, if reuse is possible, reusableResult? should be set to the previous result and state, ensuring that the state after running withRestoreOrSaveFull is identical in both runs. Note however that necessarily this is only an approximation in the case of heartbeats as heartbeats used by withRestoreOrSaveFull itself after calling act as well as by reuse-handling code such as the one supplying reusableResult? are not accounted for.

Equations

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

def Lean.Core.SavedState.restore (b : SavedState) : CoreM Unit

Restore backtrackable parts of the state.

Equations

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

def Lean.Core.mkFreshUserName (n : Name) : CoreM Name

Creates a name from n that is guaranteed to be unique. This is intended to be used for creating inaccessible user names for free variables and constants.

It works by adding a fresh macro scope to n. Applying Lean.Name.eraseMacroScopes to the resulting name yields n.

See also Lean.LocalContext.getUnusedName (for creating a new accessible user name that is unused in the local context) and Lean.Meta.mkFreshBinderNameForTactic (for creating names that are conditionally inaccessible, depending on the current value of the tactic.hygiene option).

Equations

• Lean.mkFreshUserName n = Lean.Core.mkFreshNameImp✝ n

@[inline]

def Lean.Core.CoreM.run {α : Type} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State)

Equations

• x.run ctx s = (Lean.Core.withConsistentCtx✝ x ctx).run s

@[inline]

def Lean.Core.CoreM.run' {α : Type} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception α

Equations

• x.run' ctx s = Prod.fst <$> x.run ctx s

@[inline]

def Lean.Core.CoreM.toIO {α : Type} (x : CoreM α) (ctx : Context) (s : State) : IO (α × State)

Run a CoreM monad in IO. Note that the value of ctx.initHeartbeats is ignored and replaced with IO.getNumHeartbeats.

Equations

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

@[inline]

def Lean.Core.CoreM.toIO' {α : Type} (x : CoreM α) (ctx : Context) (s : State) : IO α

Equations

• x.toIO' ctx s = (fun (x : α × Lean.Core.State) => x.fst) <$> x.toIO ctx s

@[inline]

def Lean.Core.checkInterrupted : CoreM Unit

Throws an internal interrupt exception if cancellation has been requested. The exception is not caught by try catch but is intended to be caught by Command.withLoggingExceptions at the top level of elaboration. In particular, we want to skip producing further incremental snapshots after the exception has been thrown.

Like checkSystem but without the global heartbeat check, for callers that have their own heartbeat tracking (e.g. SynthInstance).

Equations

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

def Lean.Core.withIncRecDepth {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT CoreM m] (x : m α) : m α

withIncRecDepth for a monad m such that [MonadControlT CoreM n]. Also checks for cancellation, so that recursive elaboration functions (inferType, whnf, isDefEq, …) respond promptly to interrupt requests.

Equations

• Lean.Core.withIncRecDepth x = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => do Lean.Core.checkInterrupted Lean.withIncRecDepth (runInBase x)

opaque Lean.Core.debug.moduleNameAtTimeout : Lean.Option Bool

def Lean.Core.throwMaxHeartbeat (moduleName optionName : Name) (max : Nat) : CoreM Unit

Equations

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

def Lean.Core.checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit

Equations

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

def Lean.Core.checkMaxHeartbeats (moduleName : String) : CoreM Unit

Equations

• Lean.Core.checkMaxHeartbeats moduleName = do let __do_lift ← read Lean.Core.checkMaxHeartbeatsCore moduleName `maxHeartbeats __do_lift.maxHeartbeats

def Lean.Core.checkSystem (moduleName : String) : CoreM Unit

Equations

• Lean.checkSystem moduleName = do Lean.Core.checkInterrupted Lean.Core.checkMaxHeartbeats moduleName

def Lean.Core.withCurrHeartbeats {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT CoreM m] (x : m α) : m α

Equations

• Lean.withCurrHeartbeats x = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => Lean.Core.withCurrHeartbeatsImp✝ (runInBase x)

def Lean.Core.setMessageLog (messages : MessageLog) : CoreM Unit

Equations

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

def Lean.Core.resetMessageLog : CoreM Unit

Equations

• Lean.Core.resetMessageLog = Lean.Core.setMessageLog { }

def Lean.Core.getMessageLog : CoreM MessageLog

Equations

• Lean.Core.getMessageLog = do let __do_lift ← get pure __do_lift.messages

def Lean.Core.getAndEmptyMessageLog : CoreM MessageLog

Returns the current log and then resets its messages while adjusting MessageLog.hadErrors. Used for incremental reporting during elaboration of a single command.

Equations

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

def Lean.Core.getAndEmptySnapshotTasks : CoreM (Array (Language.SnapshotTask Language.SnapshotTree))

Returns the current set of tasks added by logSnapshotTask and then resets it. When saving/restoring state of an action that may have logged such tasks during incremental reuse, this function must be used to store them in the corresponding snapshot tree; otherwise, they will leak outside and may be cancelled by a later step, potentially leading to inconsistent state being reused.

Equations

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

@[instance_reducible]

instance Lean.Core.instMonadLogCoreM : MonadLog CoreM

Equations

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

def Lean.Core.logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM Unit

Includes a given task (such as from wrapAsyncAsSnapshot) in the overall snapshot tree for this command's elaboration, making its result available to reporting and the language server. The reporter will not know about this snapshot tree node until the main elaboration thread for this command has finished so this function is not useful for incremental reporting within a longer elaboration thread but only for tasks that outlive it such as background kernel checking or proof elaboration.

Equations

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

def Lean.Core.wrapAsync {β α : Type} (act : α → CoreM β) (cancelTk? : Option IO.CancelToken) : CoreM (α → EIO Exception β)

Wraps the given action for use in EIO.asTask etc., discarding its final monadic state.

Equations

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

opaque Lean.Core.stderrAsMessages : Lean.Option Bool

Option for capturing output to stderr during elaboration.

def Lean.Core.mkSnapshot? (output : String) (ctx : Context) (st : State) (desc : String := by exact decl_name%.toString) : BaseIO (Option Language.SnapshotTree)

Creates snapshot reporting given withIsolatedStreams output and diagnostics and traces from the given state.

Equations

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

def Lean.Core.wrapAsyncAsSnapshot {α : Type} (act : α → CoreM Unit) (cancelTk? : Option IO.CancelToken) (desc : String := by exact decl_name%.toString) : CoreM (α → BaseIO Language.SnapshotTree)

Wraps the given action for use in BaseIO.asTask etc., discarding its final state except for logSnapshotTask tasks, which are reported as part of the returned tree. The given cancellation token, if any, should be stored in a SnapshotTask for the server to trigger it when the result is no longer needed.

Equations

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

@[inline]

def Lean.withAtLeastMaxRecDepth {m : Type → Type u_1} {α : Type} [MonadFunctorT CoreM m] (max : Nat) : m α → m α

Equations

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

@[inline]

def Lean.withSetOptionByName {m : Type → Type u_1} {β α : Type} [MonadFunctorT CoreM m] [KVMap.Value β] (name : Name) (v : β) : m α → m α

Runs the given computation with the option name set to v. Unlike withOptions, this is allowed inside a computation recording its dependencies: v does not depend on the ambient options, so a recorded read of name in this scope observes v in every context.

Equations

• Lean.withSetOptionByName name v = monadMap fun {β_1 : Type} => Lean.Core.withOptionsUnrestricted fun (x : Lean.Options) => x.set name v

@[inline]

def Lean.withSetOption {m : Type → Type u_1} {β α : Type} [MonadFunctorT CoreM m] [KVMap.Value β] (opt : Lean.Option β) (v : β) : m α → m α

withSetOptionByName for an option given as a Lean.Option.

Equations

• Lean.withSetOption opt v = Lean.withSetOptionByName opt.name v

@[inline]

def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exception → m α) : m α

Equations

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

@[inline]

def Lean.catchInternalIds {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Exception m] (ids : List InternalExceptionId) (x : m α) (h : Exception → m α) : m α

Equations

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

def Lean.Exception.isMaxHeartbeat (ex : Exception) : Bool

Return true if ex was generated by throwMaxHeartbeat. This function is a bit hackish. The heartbeat exception should probably be an internal exception. We used a similar hack at Exception.isMaxRecDepth

Equations

• (Lean.Exception.error ref msg).isMaxHeartbeat = (msg.stripNestedTags.kind == `runtime.maxHeartbeats)
• ex.isMaxHeartbeat = false

def Lean.mkArrow (d b : Expr) : CoreM Expr

Creates the expression d → b

Equations

• Lean.mkArrow d b = do let __do_lift ← Lean.mkFreshUserName `x pure (Lean.mkForall __do_lift Lean.BinderInfo.default d b)

def Lean.mkArrowN (ds : Array Expr) (e : Expr) : CoreM Expr

Iterated mkArrow, creates the expression a₁ → a₂ → … → aₙ → b. Also see arrowDomainsN.

Equations

• Lean.mkArrowN ds e = Array.foldrM Lean.mkArrow e ds

def Lean.traceBlock {α : Type} (tag : String) (t : Task α) : CoreM α

If t has not finished yet, waits for it under an Elab.block trace node. Returns t's result.

Equations

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

opaque Lean.compileDeclsRef : IO.Ref (Array Name → Options → CoreM Unit)

This ref exists to break a linking cycle that goes as follows:

• We start in Environment.lean, there we have functions referencing the compiler such as evalConst
• This pulls in the entire compiler transitively as well as all of its dependents
• The compiler relies on things like WHNF to inspect types
• WHNF in turn imports Environment

On Windows this causes a large amount of symbols to be included in one DLL as everything that imports the Environment instantly requires a large chunk of the Meta stack to be linked. This ref breaks the cycle by making compileDeclsImpl a "dynamic" call through the ref that is not visible to the linker. In the compiler there is a matching builtin_initialize to set this ref to the actual implementation of compileDeclsRef.

def Lean.compileDecls (decls : Array Name) (logErrors : Bool := true) : CoreM Unit

Equations

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

def Lean.compileDecl (decl : Declaration) (logErrors : Bool := true) : CoreM Unit

Equations

• Lean.compileDecl decl logErrors = Lean.compileDecls (Lean.Compiler.getDeclNamesForCodeGen decl) logErrors

def Lean.recordExtGenAccess {σ : Type} (ext : EnvExtension σ) : CoreM Unit

Inside a recording computation, records the current generation of the generation-tracked extension ext in Core.State.recordedDeps. Callers then read the state with (genRecorded := true).

Equations

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

def Lean.getRecordedOption {α : Type} [KVMap.Value α] (opt : Lean.Option α) : CoreM α

Reads an option and, inside a recording computation, records the lookup in Core.State.recordedDeps, see Lean.Meta.SynthInstanceCache. Outside a recording computation this is Lean.Option.get.

Equations

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

def Lean.getDiag (opts : Options) : Bool

Equations

• Lean.getDiag opts = Lean.Option.get opts Lean.diagnostics

@[inline]

def Lean.getOptionFlags {m : Type → Type u_1} [Monad m] [MonadReaderOf Core.Context m] : m OptionFlags

The boolean options in effect, resolved eagerly; see Lean.OptionFlags.

Equations

• Lean.getOptionFlags = do let __do_lift ← readThe Lean.Core.Context pure __do_lift.optionFlags

def Lean.isDiagnosticsEnabled : CoreM Bool

Return true if diagnostic information collection is enabled.

Equations

• Lean.isDiagnosticsEnabled = do let __do_lift ← Lean.getOptionFlags pure __do_lift.diag

def Lean.ImportM.runCoreM {α : Type} (x : CoreM α) : ImportM α

Equations

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

def Lean.Exception.isRuntime (ex : Exception) : Bool

Return true if the exception was generated by one of our resource limits.

Equations

• ex.isRuntime = (ex.isMaxHeartbeat || ex.isMaxRecDepth)

@[inline]

def Lean.Core.tryCatch {α : Type} (x : CoreM α) (h : Exception → CoreM α) : CoreM α

Custom try-catch for all monads based on CoreM. We usually don't want to catch "runtime exceptions" these monads, but on CommandElabM or, in specific cases, using tryCatchRuntimeEx. See issues #2775 and #2744 as well as MonadAlwaysExcept. Also, we never want to catch interrupt exceptions inside the elaborator.

Equations

• Lean.Core.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => if (ex.isInterrupt || ex.isRuntime) = true then throw ex else h ex

@[inline]

def Lean.Core.tryCatchRuntimeEx {α : Type} (x : CoreM α) (h : Exception → CoreM α) : CoreM α

A variant of tryCatch that also catches runtime exception (see also tryCatch documentation). Like tryCatch, this function does not catch interrupt exceptions, which are not considered runtime exceptions.

Equations

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

@[instance_reducible]

instance Lean.instMonadExceptOfExceptionCoreM : MonadExceptOf Exception CoreM

Equations

• Lean.instMonadExceptOfExceptionCoreM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Core.tryCatch }

class Lean.MonadRuntimeException (m : Type → Type) : Type 1

• tryCatchRuntimeEx {α : Type} (body : m α) (handler : Exception → m α) : m α

@[instance_reducible]

instance Lean.instMonadRuntimeExceptionCoreM : MonadRuntimeException CoreM

Equations

• Lean.instMonadRuntimeExceptionCoreM = { tryCatchRuntimeEx := fun {α : Type} => Lean.Core.tryCatchRuntimeEx }

@[instance_reducible, inline]

instance Lean.instMonadRuntimeExceptionReaderT {m : Type → Type} {ρ : Type} [MonadRuntimeException m] : MonadRuntimeException (ReaderT ρ m)

Equations

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

@[instance_reducible, inline]

instance Lean.instMonadRuntimeExceptionStateRefT' {m : Type → Type} {ω σ : Type} [MonadRuntimeException m] : MonadRuntimeException (StateRefT' ω σ m)

Equations

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

@[inline]

def Lean.mapCoreM {m : Type → Type u_1} [MonadControlT CoreM m] [Monad m] (f : {α : Type} → CoreM α → CoreM α) {α : Type} (x : m α) : m α

Equations

• Lean.mapCoreM f x = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => f (runInBase x)

def Lean.logMessageKind (kind : Name) : CoreM Bool

Returns true if the given message kind has not been reported in the message log, and then mark it as logged. Otherwise, returns false. We use this API to ensure we don't log the same kind of warning multiple times.

Equations

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

def Lean.enableRealizationsForConst (n : Name) : CoreM Unit

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

• Lean.enableRealizationsForConst n = do let __do_lift ← Lean.getEnv let __do_lift_1 ← Lean.getOptions let env ← liftM (__do_lift.enableRealizationsForConst __do_lift_1 n) Lean.setEnv env

@[inline]

def Lean.Core.mapError {m : Type → Type u_1} {α : Type} [MonadControlT CoreM m] [Monad m] (x : m α) (f : MessageData → MessageData) : m α

Execute x, and apply f to the produced error message

Equations

• Lean.Core.mapError x f = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => Lean.mapErrorImp✝ (runInBase x) f

@[inline]

def Lean.Core.prependError {m : Type → Type u_1} {α : Type} [MonadControlT CoreM m] [Monad m] (msg : MessageData) (x : m α) : m α

Execute x. If it throws an error, indent and prepend msg to it.

Equations

• Lean.Core.prependError msg x = Lean.Core.mapError x fun (e : Lean.MessageData) => Lean.toMessageData msg ++ Lean.toMessageData (Lean.indentD e)