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.
Instances For
Equations
- Lean.Core.getMaxHeartbeats opts = Lean.Option.get opts Lean.maxHeartbeats * 1000
Instances For
Equations
Instances For
Cache for the CoreM
monad
- instLevelType : Lean.Core.InstantiateLevelCache
- instLevelValue : Lean.Core.InstantiateLevelCache
Instances For
Equations
- Lean.Core.instInhabitedCache = { default := { instLevelType := default, instLevelValue := default } }
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
FVarId
s,MVarId
s, andLMVarId
s - 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.
- snapshotTasks : Array (Lean.Language.SnapshotTask Lean.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.
Instances For
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 : Lean.Name
- openDecls : List Lean.OpenDecl
- initHeartbeats : Nat
- maxHeartbeats : Nat
- currMacroScope : Lean.MacroScope
- diag : Bool
- 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 alsologMessage
below.
Instances For
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
Instances For
Equations
- Lean.Core.instMonadCoreM = Monad.mk
Equations
- Lean.Core.instInhabitedCoreM = { default := fun (x : Lean.Core.Context) (x : ST.Ref IO.RealWorld Lean.Core.State) => throw default }
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
- Lean.Core.instMonadOptionsCoreM = { getOptions := do let __do_lift ← read pure __do_lift.options }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Core.instAddMessageContextCoreM = { addMessageContext := Lean.addMessageContextPartial }
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
Equations
- Lean.Core.instMonadLiftIOCoreM = { monadLift := fun {α : Type} => Lean.Core.liftIOCore }
Equations
- One or more equations did not get rendered due to their size.
- passedHeartbeats : Nat
Number of heartbeats passed inside
withRestoreOrSaveFull
, not used otherwise.
Instances For
Equations
- Lean.Core.saveState = do let s ← get pure { toState := s, passedHeartbeats := 0 }
Instances For
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)
Instances For
Restore backtrackable parts of the state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- x.run ctx s = (Lean.Core.withConsistentCtx✝ x ctx).run s
Instances For
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Core.withIncRecDepth x = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => Lean.withIncRecDepth (runInBase x)
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Core.checkMaxHeartbeats moduleName = do let __do_lift ← read Lean.Core.checkMaxHeartbeatsCore moduleName `maxHeartbeats __do_lift.maxHeartbeats
Instances For
Equations
- Lean.checkSystem moduleName = do Lean.Core.checkInterrupted Lean.Core.checkMaxHeartbeats moduleName
Instances For
Equations
- Lean.withCurrHeartbeats x = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => Lean.Core.withCurrHeartbeatsImp✝ (runInBase x)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Core.getMessageLog = do let __do_lift ← get pure __do_lift.messages
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
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.
Instances For
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.
Instances For
Option for capturing output to stderr during elaboration.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.tagged `runtime.maxHeartbeats a)).isMaxHeartbeat = true
- ex.isMaxHeartbeat = false
Instances For
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)
Instances For
Iterated mkArrow
, creates the expression a₁ → a₂ → … → aₙ → b
. Also see arrowDomainsN
.
Equations
- Lean.mkArrowN ds e = Array.foldrM Lean.mkArrow e ds
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.getDiag opts = Lean.Option.get opts Lean.diagnostics
Instances For
Return true
if diagnostic information collection is enabled.
Equations
- Lean.isDiagnosticsEnabled = do let __do_lift ← read pure __do_lift.diag
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return true
if the exception was generated by one of our resource limits.
Instances For
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
Instances For
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
Instances For
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.
Instances For
Equations
- Lean.instMonadExceptOfExceptionCoreM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Core.tryCatch }
- tryCatchRuntimeEx : {α : Type} → m α → (Lean.Exception → m α) → m α
Instances
Equations
- Lean.instMonadRuntimeExceptionCoreM = { tryCatchRuntimeEx := fun {α : Type} => Lean.Core.tryCatchRuntimeEx }
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
- Lean.mapCoreM f x = controlAt Lean.CoreM fun (runInBase : {β : Type} → m β → Lean.CoreM (stM Lean.CoreM m β)) => f (runInBase x)
Instances For
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.