Documentation

Lean.Elab.Command

A Scope records the part of the CommandElabM state that respects scoping, such as the data for universe, open, and variable declarations, the current namespace, and currently enabled options. The CommandElabM state contains a stack of scopes, and only the top Scope on the stack is read from or modified. There is always at least one Scope on the stack, even outside any section or namespace, and each new pushed Scope starts as a modified copy of the previous top scope.

  • header : String

    The component of the namespace or section that this scope is associated to. For example, section a.b.c and namespace a.b.c each create three scopes with headers named a, b, and c. This is used for checking the end command. The "base scope" has "" as its header.

  • The current state of all set options at this point in the scope. Note that this is the full current set of options and does not simply contain the options set while this scope has been active.

  • currNamespace : Lean.Name

    The current namespace. The top-level namespace is represented by Name.anonymous.

  • openDecls : List Lean.OpenDecl

    All currently opened namespaces and names.

  • levelNames : List Lean.Name

    The current list of names for universe level variables to use for new declarations. This is managed by the universe command.

  • varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)

    The current list of binders to use for new declarations. This is managed by the variable command. Each binder is represented in Syntax form, and it is re-elaborated within each command that uses this information.

    This is also used by commands, such as #check, to create an initial local context, even if they do not work with binders per se.

  • varUIds : Array Lean.Name

    Globally unique internal identifiers for the varDecls. There is one identifier per variable introduced by the binders (recall that a binder such as (a b c : Ty) can produce more than one variable), and each identifier is the user-provided variable name with a macro scope. This is used by TermElabM in Lean.Elab.Term.Context to help with processing macros that capture these variables.

  • includedVars : List Lean.Name

    included section variable names (from varUIds)

  • omittedVars : List Lean.Name

    omitted section variable names (from varUIds)

  • isNoncomputable : Bool

    If true (default: false), all declarations that fail to compile automatically receive the noncomputable modifier. A scope with this flag set is created by noncomputable section.

    Recall that a new scope inherits all values from its parent scope, so all sections and namespaces nested within a noncomputable section also have this flag set.

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[reducible, inline]
      Instances For
        @[reducible, inline]
        Instances For
          @[inline]

          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.

          Instances For
            def Lean.Elab.Command.mkState (env : Lean.Environment) (messages : Lean.MessageLog := { hadErrors := false, unreported := { root := Lean.PersistentArrayNode.node (Array.mkEmpty Lean.PersistentArray.branching.toNat), tail := Array.mkEmpty Lean.PersistentArray.branching.toNat, size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, reportedKinds := }) (opts : Lean.Options := { entries := [] }) :
            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.
              @[always_inline]
              Equations
              Equations
              Instances For
                @[inline]
                Equations
                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.
                  @[inline]

                  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
                  Instances For

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

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

                      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
                          Instances For
                            Equations
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[implemented_by Lean.Elab.Command.mkCommandElabAttributeUnsafe]

                                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

                                    Snapshot after macro expansion of a command.

                                    Instances For

                                      Option for showing elaboration errors from partial syntax errors.

                                      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.

                                        Instances For
                                          Equations
                                          • Lean.Elab.Command.instInhabitedCommandElabM = { default := throw default }

                                          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.

                                          Instances For

                                            Return identifier names in the given bracketed binder.

                                            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:

                                              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

                                                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:

                                                import Lean
                                                
                                                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
                                                  Instances For
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Lean.liftCommandElabM {α : Type} (cmd : Lean.Elab.Command.CommandElabM α) (throwOnError : Bool := true) :

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