- env : Environment
- messages : MessageLog
- usedQuotCtxts : NameSet
- nextMacroScope : Nat
- maxRecDepth : Nat
- ngen : NameGenerator
- auxDeclNGen : DeclNameGenerator
- infoState : InfoState
- traceState : TraceState
- snapshotTasks : Array (Language.SnapshotTask Language.SnapshotTree)
Instances For
- fileName : String
- fileMap : FileMap
- currRecDepth : Nat
- cmdPos : String.Pos
- macroStack : MacroStack
- currMacroScope : MacroScope
- ref : Syntax
Snapshot for incremental reuse and reporting of command elaboration. Currently only used for (mutual) defs and contained tactics, in which case the
DynamicSnapshot
is aHeadersParsedSnapshot
.Definitely resolved in
Lean.Elab.Command.elabCommandTopLevel
.Invariant: if the bundle's
old?
is set, the context and state at the beginning of current and old elaboration are identical.- cancelTk? : Option IO.CancelToken
Cancellation token forwarded to
Core.cancelTk?
. - suppressElabErrors : Bool
If set (when
showPartialSyntaxErrors
is not set and parsing failed), suppresses most elaboration errors; see alsologMessage
below.
Instances For
Equations
Instances For
Instances For
- run : Syntax → CommandElabM Unit
- name : Name
Instances For
Equations
- One or more equations did not get rendered due to their size.
Like Core.tryCatchRuntimeEx
; runtime errors are generally used to abort term elaboration, so we do
want to catch and process them at the command level.
Equations
- Lean.Elab.Command.tryCatch x h = tryCatch x fun (ex : Lean.Exception) => if ex.isInterrupt = true then throw ex else h ex
Instances For
Equations
- Lean.Elab.Command.instMonadExceptOfExceptionCommandElabM = { throw := fun {α : Type} => throw, tryCatch := fun {α : Type} => Lean.Elab.Command.tryCatch }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.addLinter l = do let ls ← ST.Ref.get Lean.Elab.Command.lintersRef ST.Ref.set Lean.Elab.Command.lintersRef (ls.push l)
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
- Lean.Elab.Command.getRef = do let __do_lift ← read pure __do_lift.ref
Instances For
Equations
- Lean.Elab.Command.instAddMessageContextCommandElabM = { 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.
Equations
- Lean.Elab.Command.getCurrMacroScope = do let __do_lift ← read pure __do_lift.currMacroScope
Instances For
Equations
- Lean.Elab.Command.getMainModule = do let __do_lift ← Lean.getEnv pure __do_lift.mainModule
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.
Equations
- Lean.Elab.Command.liftCoreM x = do let __do_lift ← Lean.Elab.Command.runCore✝ (observing x) ofExcept __do_lift
Instances For
Equations
- Lean.Elab.Command.liftIO x = do let ctx ← read liftM (IO.toEIO (fun (ex : IO.Error) => Lean.Exception.error ctx.ref ((Lean.MessageData.ofFormat ∘ Std.format) ex.toString)) x)
Instances For
Equations
- Lean.Elab.Command.instMonadLiftTIOCommandElabM = { monadLift := fun {α : Type} => Lean.Elab.Command.liftIO }
Return the current scope.
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
Catches and logs exceptions occurring in x
. Unlike try catch
in CommandElabM
, this function
catches interrupt exceptions as well and thus is intended for use at the top level of elaboration.
Interrupt and abort exceptions are caught but not logged.
Equations
- Lean.Elab.Command.withLoggingExceptions x ctx ref = liftM ((Lean.Elab.withLogging x ctx ref).catchExceptions fun (x : Lean.Exception) => pure ())
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
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.
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Registers a command elaborator for the given syntax node kind.
A command elaborator should have type Lean.Elab.Command.CommandElab
(which is
Lean.Syntax → Lean.Elab.Term.CommandElabM Unit
), i.e. should take syntax of the given syntax
node kind as a parameter and perform an action.
The elab_rules
and elab
commands should usually be preferred over using this attribute
directly.
Disables incremental command reuse and reporting for act
if cond
is true by setting
Context.snap?
to none
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Elaborate x
with stx
on the macro stack
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.
Snapshot after macro expansion of a command.
- macroDecl : Name
The declaration name of the macro.
- newStx : Syntax
The expanded syntax tree.
- newNextMacroScope : Nat
State.nextMacroScope
after expansion. - hasTraces : Bool
Whether any traces were present after expansion.
Follow-up elaboration snapshots, one per command if
newStx
is a sequence of commands.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Option for showing elaboration errors from partial syntax errors.
If hint?
is some hint
, establishes a new context for macro scope naming and runs act
in it,
otherwise runs act
directly without changes.
Context names as documented in Note Macro Scope Representation
help with avoiding rebuilds and
prefer_native
lookup misses from macro scopes in declaration names and other exported information.
This function establishes a new context with a globally unique name by combining the name of the
current module with hint
while also checking for previously used hint
s in the same module.
Thus hint
does not need to be unique but ensuring it is usually unique helps with keeping the
context name stable.
In the current implementation, we call withInitQuotContext
once in elabCommandTopLevel
using the
source input of the command as the hint. This helps with keeping macro scopes stable on changes to
other parts of the file but not on changes to the command itself. Thus in each declaration
elaborator we call withInitQuotContext
again with the declaration name(s) as a hint so that
changes to any other part of the declaration do not change the context name.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Elab.Command.withInitQuotContext hint? act = act
Instances For
elabCommand
wrapper that should be used for the initial invocation, not for recursive calls after
macro expansion etc.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Adapt a syntax transformation to a regular, command-producing elaborator.
Equations
- Lean.Elab.Command.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Command.withMacroExpansion stx stx' (Lean.Elab.Command.elabCommand stx')
Instances For
The environment linter framework needs to be able to run linters with the same context
as liftTermElabM
, so we expose that context as a public function here.
Equations
- Lean.Elab.Command.mkMetaContext = { keyedConfig := { foApprox := true, ctxApprox := true, quasiPatternApprox := true }.toConfigWithKey }
Instances For
Return identifier names in the given bracketed binder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lift the TermElabM
monadic action x
into a CommandElabM
monadic action.
Note that x
is executed with an empty message log. Thus, x
cannot modify/view messages produced by
previous commands.
If you need to access the free variables corresponding to the ones declared using the variable
command,
consider using runTermElabM
.
Recall that TermElabM
actions can automatically lift MetaM
and CoreM
actions.
Example:
public import Lean
open Lean Elab Command Meta
def printExpr (e : Expr) : MetaM Unit := do
IO.println s!"{← ppExpr e} : {← ppExpr (← inferType e)}"
#eval
liftTermElabM do
printExpr (mkConst ``Nat)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Elab.Command.instMonadEvalTermElabMCommandElabM = { monadEval := fun {α : Type} => Lean.Elab.Command.liftTermElabM }
Execute the monadic action elabFn xs
as a CommandElabM
monadic action, where xs
are free variables
corresponding to all active scoped variables declared using the variable
command.
This method is similar to liftTermElabM
, but it elaborates all scoped variables declared using the variable
command.
Example:
public import Lean
public section
open Lean Elab Command Meta
variable {α : Type u} {f : α → α}
variable (n : Nat)
#eval
runTermElabM fun xs => do
for x in xs do
IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return the stack of all currently active scopes: the base scope always comes last; new scopes are prepended in the front. In particular, the current scope is always the first element.
Equations
- Lean.Elab.Command.getScopes = do let __do_lift ← get pure __do_lift.scopes
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.Elab.Command.getLevelNames = do let __do_lift ← Lean.Elab.Command.getScope pure __do_lift.levelNames
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lifts an action in CommandElabM
into CoreM
, updating the environment,
messages, info trees, traces, the name generator, and macro scopes.
The action is run in a context with an empty message log, empty trace state, and empty info trees.
If throwOnError
is true, then if the command produces an error message, it is converted into an exception.
In this case, info trees and messages are not carried over.
Commands that modify the processing of subsequent commands,
such as open
and namespace
commands,
only have an effect for the remainder of the CommandElabM
computation passed here,
and do not affect subsequent commands.
Warning: when using this from MetaM
monads, the caches are not reset.
If the command defines new instances for example, you should use Lean.Meta.resetSynthInstanceCache
to reset the instance cache.
While the modifyEnv
function for MetaM
clears its caches entirely,
liftCommandElabM
has no way to reset these caches.
Equations
- Lean.liftCommandElabM cmd throwOnError = do let __do_lift ← Lean.liftCommandElabMCore✝ (observing cmd) throwOnError ofExcept __do_lift
Instances For
Given a command elaborator cmd
, returns a new command elaborator that
first evaluates any local set_option ... in ...
clauses and then invokes cmd
on what remains.