opaque Lean.diagnostics : Lean.Option Bool

opaque Lean.diagnostics.threshold : Lean.Option Nat

opaque Lean.maxHeartbeats : Lean.Option Nat

def Lean.useDiagnosticMsg : Lean.MessageData

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

Equations

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

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

Instances For

• Lean.Core.instInhabitedCache

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.

Instances For

• Lean.Core.instNonemptyState

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
• diag : Bool

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

• cancelTk? : Option IO.CancelToken

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

• suppressElabErrors : Bool

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

Instances For

• Lean.Core.instNonemptyContext

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

Instances For

• Lean.Core.instAddMessageContextCoreM
• Lean.Core.instInhabitedCoreM
• Lean.Core.instMetaEvalCoreM
• Lean.Core.instMonadCoreM
• Lean.Core.instMonadEnvCoreM
• Lean.Core.instMonadInfoTreeCoreM
• Lean.Core.instMonadLiftIOCoreM
• Lean.Core.instMonadLogCoreM
• Lean.Core.instMonadNameGeneratorCoreM
• Lean.Core.instMonadOptionsCoreM
• Lean.Core.instMonadQuotationCoreM
• Lean.Core.instMonadRecDepthCoreM
• Lean.Core.instMonadRefCoreM
• Lean.Core.instMonadResolveNameCoreM
• Lean.Core.instMonadTraceCoreM
• Lean.Core.instMonadWithOptionsCoreM
• Lean.instMonadExceptOfExceptionCoreM
• Lean.instMonadRuntimeExceptionCoreM

@[always_inline]

instance Lean.Core.instMonadCoreM : Monad Lean.CoreM

Equations

• Lean.Core.instMonadCoreM = 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 ∘ Lean.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.

structure Lean.Core.SavedStateextends Lean.Core.State : Type

• env : Lean.Environment
• nextMacroScope : Lean.MacroScope
• ngen : Lean.NameGenerator
• traceState : Lean.TraceState
• cache : Lean.Core.Cache
• messages : Lean.MessageLog
• infoState : Lean.Elab.InfoState
• passedHeartbeats : Nat

  Number of heartbeats passed inside withRestoreOrSaveFull, not used otherwise.

Instances For

• Lean.Core.instNonemptySavedState

instance Lean.Core.instNonemptySavedState : Nonempty Lean.Core.SavedState

Equations

• Lean.Core.instNonemptySavedState = ⋯

def Lean.Core.saveState : Lean.CoreM Lean.Core.SavedState

Equations

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

@[specialize #[]]

def Lean.Core.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × Lean.Core.SavedState)) (act : Lean.CoreM α) : Lean.CoreM (α × Lean.Core.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.
• Lean.Core.withRestoreOrSaveFull (some (val, state)) act = do set state.toState liftM (IO.addHeartbeats state.passedHeartbeats.toUInt64) pure (val, state)

def Lean.Core.SavedState.restore (b : Lean.Core.SavedState) : 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.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 = (Lean.Core.withConsistentCtx 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)

opaque Lean.Core.interruptExceptionId : Lean.InternalExceptionId

@[inline]

def Lean.Core.checkInterrupted : Lean.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.

Equations

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

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

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

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

• (Lean.Exception.error ref (Lean.MessageData.ofFormatWithInfos { fmt := Std.Format.text msg, infos := infos })).isMaxHeartbeat = "(deterministic) timeout".isPrefixOf msg
• ex.isMaxHeartbeat = 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

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.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 of our resource limits.

Equations

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

def Lean.Exception.isInterrupt : Lean.Exception → Bool

Returns true if the exception is an interrupt generated by checkInterrupted.

Equations

• (Lean.Exception.internal id extra).isInterrupt = (id == Lean.Core.interruptExceptionId)
• x.isInterrupt = false

@[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 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 : Lean.CoreM α) (h : Lean.Exception → Lean.CoreM α) : Lean.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 Lean.instMonadExceptOfExceptionCoreM : MonadExceptOf Lean.Exception Lean.CoreM

Equations

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

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

• tryCatchRuntimeEx : {α : Type} → m α → (Lean.Exception → m α) → m α

Instances

• Lean.instMonadRuntimeExceptionCoreM
• Lean.instMonadRuntimeExceptionReaderT
• Lean.instMonadRuntimeExceptionStateRefT'

instance Lean.instMonadRuntimeExceptionCoreM : Lean.MonadRuntimeException Lean.CoreM

Equations

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

@[inline]

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

Equations

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

@[inline]

instance Lean.instMonadRuntimeExceptionStateRefT' {m : Type → Type} {ω : Type} {σ : Type} [Lean.MonadRuntimeException m] : Lean.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 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)

def Lean.reportMessageKind (kind : Lake.Name) : Lean.CoreM Bool

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

Equations

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