opaque Lean.diagnostics : Lean.Option Bool

opaque Lean.diagnostics.threshold : Lean.Option Nat

opaque Lean.maxHeartbeats : Lean.Option Nat

def Lean.Core.getMaxHeartbeats (opts : Lean.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 Lake.Name (List Lean.Level × Lean.Expr)

structure Lean.Core.Cache : Type

Cache for the CoreM monad

• instLevelType : Lean.Core.InstantiateLevelCache
• instLevelValue : Lean.Core.InstantiateLevelCache

instance Lean.Core.instInhabitedCache : Inhabited Lean.Core.Cache

Equations

• Lean.Core.instInhabitedCache = { default := { instLevelType := default, instLevelValue := default } }

structure Lean.Core.State : Type

State for the CoreM monad.

• env : Lean.Environment

  Current environment.

• nextMacroScope : Lean.MacroScope

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

• ngen : Lean.NameGenerator

  Name generator for producing unique FVarIds, MVarIds, and LMVarIds

• traceState : Lean.TraceState

  Trace messages

• cache : Lean.Core.Cache

  Cache for instantiating universe polymorphic declarations.

• messages : Lean.MessageLog

  Message log.

• infoState : Lean.Elab.InfoState

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

instance Lean.Core.instNonemptyState : Nonempty Lean.Core.State

Equations

• Lean.Core.instNonemptyState = ⋯

structure Lean.Core.Context : Type

Context for the CoreM monad.

• fileName : String

  Name of the file being compiled.

• fileMap : Lean.FileMap

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

• options : Lean.Options
• currRecDepth : Nat
• maxRecDepth : Nat
• ref : Lean.Syntax
• currNamespace : Lake.Name
• openDecls : List Lean.OpenDecl
• initHeartbeats : Nat
• maxHeartbeats : Nat
• currMacroScope : Lean.MacroScope
• catchRuntimeEx : Bool

  If catchRuntimeEx = false, then given try x catch ex => h ex, an runtime exception occurring in x is not handled by h. Recall that runtime exceptions are maxRecDepth or maxHeartbeats.

• diag : Bool

  If diag := true, different parts of the system collect diagnostics. Use the set_option diag true to set it to true.

instance Lean.Core.instNonemptyContext : Nonempty Lean.Core.Context

Equations

• Lean.Core.instNonemptyContext = ⋯

@[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))

@[always_inline]

instance Lean.Core.instMonadCoreM : Monad Lean.CoreM

Equations

• Lean.Core.instMonadCoreM = let i := inferInstanceAs (Monad Lean.CoreM); Monad.mk

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

Equations

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

instance Lean.Core.instMonadRefCoreM : Lean.MonadRef Lean.CoreM

Equations

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

instance Lean.Core.instMonadEnvCoreM : Lean.MonadEnv Lean.CoreM

Equations

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

instance Lean.Core.instMonadOptionsCoreM : Lean.MonadOptions Lean.CoreM

Equations

• Lean.Core.instMonadOptionsCoreM = { getOptions := do let __do_lift ← read pure __do_lift.options }

instance Lean.Core.instMonadWithOptionsCoreM : Lean.MonadWithOptions Lean.CoreM

Equations

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

instance Lean.Core.instAddMessageContextCoreM : Lean.AddMessageContext Lean.CoreM

Equations

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

instance Lean.Core.instMonadNameGeneratorCoreM : Lean.MonadNameGenerator Lean.CoreM

Equations

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

instance Lean.Core.instMonadRecDepthCoreM : Lean.MonadRecDepth Lean.CoreM

Equations

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

instance Lean.Core.instMonadResolveNameCoreM : Lean.MonadResolveName Lean.CoreM

Equations

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

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

Equations

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

instance Lean.Core.instMonadQuotationCoreM : Lean.MonadQuotation Lean.CoreM

Equations

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

instance Lean.Core.instMonadInfoTreeCoreM : Lean.Elab.MonadInfoTree Lean.CoreM

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

def Lean.Core.instantiateValueLevelParams (c : Lean.ConstantInfo) (us : List Lean.Level) : Lean.CoreM Lean.Expr

Equations

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

@[inline]

def Lean.Core.liftIOCore {α : Type} (x : IO α) : Lean.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 Lean.Core.instMonadLiftIOCoreM : MonadLift IO Lean.CoreM

Equations

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

instance Lean.Core.instMonadTraceCoreM : Lean.MonadTrace Lean.CoreM

Equations

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

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

Restore backtrackable parts of the state.

Equations

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

def Lean.Core.restoreFull (b : Lean.Core.State) : Lean.CoreM Unit

Restores full state including sources for unique identifiers. Only intended for incremental reuse between elaboration runs, not for backtracking within a single run.

Equations

• Lean.Core.restoreFull b = set b

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

Equations

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

@[inline]

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

Equations

• x.run ctx s = (x ctx).run s

@[inline]

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

Equations

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

@[inline]

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

Equations

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

instance Lean.Core.instMetaEvalCoreM {α : Type} [Lean.MetaEval α] : Lean.MetaEval (Lean.CoreM α)

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 Lean.CoreM m] (x : m α) : m α

Equations

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

@[inline]

def Lean.Core.checkInterrupted : Lean.CoreM Unit

Equations

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

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

Equations

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

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

Equations

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

def Lean.Core.checkMaxHeartbeats (moduleName : String) : Lean.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) : Lean.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 Lean.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 : Lean.MessageLog) : Lean.CoreM Unit

Equations

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

def Lean.Core.resetMessageLog : Lean.CoreM Unit

Equations

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

def Lean.Core.getMessageLog : Lean.CoreM Lean.MessageLog

Equations

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

def Lean.Core.getAndEmptyMessageLog : Lean.CoreM Lean.MessageLog

Returns the current log and then resets its messages but does NOT reset 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.

instance Lean.Core.instMonadLogCoreM : Lean.MonadLog Lean.CoreM

Equations

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

@[inline]

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

Equations

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

@[inline]

def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Lean.Exception m] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.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 Lean.Exception m] (ids : List Lean.InternalExceptionId) (x : m α) (h : Lean.Exception → m α) : m α

Equations

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

def Lean.Exception.isMaxHeartbeat (ex : Lean.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

• ex.isMaxHeartbeat = match ex with | Lean.Exception.error ref (Lean.MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg | x => false

def Lean.mkArrow (d : Lean.Expr) (b : Lean.Expr) : Lean.CoreM Lean.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 Lean.Expr) (e : Lean.Expr) : Lean.CoreM Lean.Expr

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

Equations

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

def Lean.addDecl (decl : Lean.Declaration) : Lean.CoreM Unit

Equations

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

opaque Lean.compiler.enableNew : Lean.Option Bool

@[extern lean_lcnf_compile_decls]

opaque Lean.compileDeclsNew (declNames : List Lake.Name) : Lean.CoreM Unit

def Lean.compileDecl (decl : Lean.Declaration) : Lean.CoreM Unit

Equations

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

def Lean.compileDecls (decls : List Lake.Name) : Lean.CoreM Unit

Equations

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

def Lean.addAndCompile (decl : Lean.Declaration) : Lean.CoreM Unit

Equations

• Lean.addAndCompile decl = do Lean.addDecl decl Lean.compileDecl decl

def Lean.getDiag (opts : Lean.Options) : Bool

Equations

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

def Lean.isDiagnosticsEnabled : Lean.CoreM Bool

Return true if diagnostic information collection is enabled.

Equations

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

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

Equations

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

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

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

Equations

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

@[inline]

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

Custom try-catch for all monads based on CoreM. We don't want to catch "runtime exceptions" in these monads, but on CommandElabM. See issues #2775 and #2744 as well as MonadAlwayExcept.

Equations

• Lean.Core.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => do let __do_lift ← read if (ex.isRuntime && !__do_lift.catchRuntimeEx) = true then throw ex else h ex

instance Lean.instMonadExceptOfExceptionCoreM : MonadExceptOf Lean.Exception Lean.CoreM

Equations

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

@[inline]

def Lean.Core.withCatchingRuntimeEx {α : Type} (flag : Bool) (x : Lean.CoreM α) : Lean.CoreM α

Equations

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

@[inline]

def Lean.mapCoreM {m : Type → Type u_1} [MonadControlT Lean.CoreM m] [Monad m] (f : {α : Type} → Lean.CoreM α → Lean.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)

@[inline]

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

Execute x with catchRuntimeEx = flag. That is, given try x catch ex => h ex, if x throws a runtime exception, the handler h will be invoked if flag = true Recall that

Equations

• Lean.withCatchingRuntimeEx x = Lean.mapCoreM (fun {α : Type} => Lean.Core.withCatchingRuntimeEx true) x

@[inline]

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

Equations

• Lean.withoutCatchingRuntimeEx x = Lean.mapCoreM (fun {α : Type} => Lean.Core.withCatchingRuntimeEx false) x