Documentation

Lean.CoreM

Performance option used by cmdline driver.

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

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

    Name generator that creates user-accessible names.

    Instances For

      Creates a user-accessible unique name of the following structure:

      <name prefix>.<infix>_<numeric components>_...
      

      Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other branching elaboration steps, mkChild must be used (automatically done in wrapAsync*).

      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
          Instances
            def Lean.mkAuxDeclName {m : TypeType} [Monad m] [MonadEnv m] [MonadDeclNameGenerator m] (kind : Name := `_aux) :

            Creates a new name for use as an auxiliary declaration that can be assumed to be globally unique.

            Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other branching elaboration steps, mkChild must be used (automatically done in wrapAsync*).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.withDeclNameForAuxNaming {m : TypeType} {α : Type} [Monad m] [MonadFinally m] [MonadDeclNameGenerator m] (name : Name) (x : m α) :
              m α

              Adjusts the namePrefix of getDeclNGen to the given name and resets the nested counter.

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

                Cache for the CoreM monad

                Instances For
                  Equations

                  State for the CoreM monad.

                  • Current environment.

                  • nextMacroScope : MacroScope

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

                  • Name generator for producing unique FVarIds, MVarIds, and LMVarIds

                  • auxDeclNGen : DeclNameGenerator

                    Name generator for creating persistent auxiliary declarations. Separate from ngen to keep numbers smaller and create user-accessible names.

                  • traceState : TraceState

                    Trace messages

                  • cache : Cache

                    Cache for instantiating universe polymorphic declarations.

                  • messages : MessageLog

                    Message log.

                  • infoState : Elab.InfoState

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

                  • 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 : FileMap

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

                    • options : Options
                    • currRecDepth : Nat
                    • maxRecDepth : Nat
                    • ref : Syntax
                    • currNamespace : Name
                    • openDecls : List OpenDecl
                    • initHeartbeats : Nat
                    • maxHeartbeats : Nat
                    • currMacroScope : MacroScope
                    • diag : Bool

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

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

                    • inheritedTraceOptions : Std.HashSet Name
                    Instances For
                      @[reducible, inline]
                      abbrev Lean.Core.CoreM (α : 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
                      Instances For
                        @[always_inline]
                        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
                        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
                        • 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.
                          @[inline]
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[inline]
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[inline]
                              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
                                    @[inline]
                                    def Lean.Core.liftIOCore {α : Type} (x : IO α) :
                                    Equations
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Equations
                                      Instances For
                                        @[specialize #[]]
                                        def Lean.Core.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × SavedState)) (act : CoreM α) :

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

                                          Restore backtrackable parts of the state.

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

                                            Creates a name from n that is guaranteed to be unique. This is intended to be used for creating inaccessible user names for free variables and constants.

                                            It works by adding a fresh macro scope to n. Applying Lean.Name.eraseMacroScopes to the resulting name yields n.

                                            See also Lean.LocalContext.getUnusedName (for creating a new accessible user name that is unused in the local context) and Lean.Meta.mkFreshBinderNameForTactic (for creating names that are conditionally inaccessible, depending on the current value of the tactic.hygiene option).

                                            Equations
                                            Instances For
                                              @[inline]
                                              def Lean.Core.CoreM.run {α : Type} (x : CoreM α) (ctx : Context) (s : State) :
                                              Equations
                                              Instances For
                                                @[inline]
                                                def Lean.Core.CoreM.run' {α : Type} (x : CoreM α) (ctx : Context) (s : State) :
                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Lean.Core.CoreM.toIO {α : Type} (x : CoreM α) (ctx : Context) (s : State) :
                                                  IO (α × State)
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Lean.Core.withIncRecDepth {m : TypeType u_1} {α : Type} [Monad m] [MonadControlT CoreM m] (x : m α) :
                                                    m α
                                                    Equations
                                                    Instances For
                                                      @[inline]

                                                      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
                                                        def Lean.Core.throwMaxHeartbeat (moduleName optionName : Name) (max : Nat) :
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          def Lean.Core.checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) :
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            Instances For
                                                              def Lean.Core.withCurrHeartbeats {m : TypeType u_1} {α : Type} [Monad m] [MonadControlT CoreM m] (x : m α) :
                                                              m α
                                                              Equations
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  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

                                                                      Returns the current set of tasks added by logSnapshotTask and then resets it. When saving/restoring state of an action that may have logged such tasks during incremental reuse, this function must be used to store them in the corresponding snapshot tree; otherwise, they will leak outside and may be cancelled by a later step, potentially leading to inconsistent state being reused.

                                                                      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
                                                                          def Lean.Core.wrapAsync {β α : Type} (act : αCoreM β) (cancelTk? : Option IO.CancelToken) :
                                                                          CoreM (αEIO Exception β)

                                                                          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.

                                                                            def Lean.Core.mkSnapshot (output : String) (ctx : Context) (st : State) (desc : String := by exact decl_name%.toString) :

                                                                            Creates snapshot reporting given withIsolatedStreams output and diagnostics and traces from the given state.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Lean.Core.wrapAsyncAsSnapshot {α : Type} (act : αCoreM Unit) (cancelTk? : Option IO.CancelToken) (desc : String := by exact decl_name%.toString) :

                                                                              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
                                                                                @[inline]
                                                                                def Lean.withAtLeastMaxRecDepth {m : TypeType u_1} {α : Type} [MonadFunctorT CoreM m] (max : Nat) :
                                                                                m αm α
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[inline]
                                                                                  def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Exception m] (id : InternalExceptionId) (x : m α) (h : Exceptionm α) :
                                                                                  m α
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[inline]
                                                                                    def Lean.catchInternalIds {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Exception m] (ids : List InternalExceptionId) (x : m α) (h : Exceptionm α) :
                                                                                    m α
                                                                                    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
                                                                                      Instances For

                                                                                        Creates the expression d → b

                                                                                        Equations
                                                                                        Instances For

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

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Lean.traceBlock {α : Type} (tag : String) (t : Task α) :

                                                                                            If t has not finished yet, waits for it under an Elab.block trace node. Returns t's result.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[extern lean_lcnf_compile_decls]
                                                                                              opaque Lean.compileDeclsNew (declNames : List Name) :
                                                                                              @[extern lean_compile_decls]
                                                                                              def Lean.compileDecls (decls : List Name) (ref? : Option Declaration := none) (logErrors : Bool := true) :
                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For
                                                                                                def Lean.compileDecls.doCompile (decls : List Name) (ref? : Option Declaration := none) (logErrors : Bool := true) :
                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  def Lean.compileDecl (decl : Declaration) (logErrors : Bool := true) :
                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    def Lean.getDiag (opts : Options) :
                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      Return true if diagnostic information collection is enabled.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        def Lean.ImportM.runCoreM {α : Type} (x : CoreM α) :
                                                                                                        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.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline]
                                                                                                            def Lean.Core.tryCatch {α : Type} (x : CoreM α) (h : ExceptionCoreM α) :

                                                                                                            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
                                                                                                            Instances For
                                                                                                              @[inline]
                                                                                                              def Lean.Core.tryCatchRuntimeEx {α : Type} (x : CoreM α) (h : ExceptionCoreM α) :

                                                                                                              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
                                                                                                                • tryCatchRuntimeEx {α : Type} (body : m α) (handler : Exceptionm α) : m α
                                                                                                                Instances
                                                                                                                  @[inline]
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  @[inline]
                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  @[inline]
                                                                                                                  def Lean.mapCoreM {m : TypeType u_1} [MonadControlT CoreM m] [Monad m] (f : {α : Type} → CoreM αCoreM α) {α : Type} (x : m α) :
                                                                                                                  m α
                                                                                                                  Equations
                                                                                                                  Instances For

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

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

                                                                                                                      Allows realizeConst calls for the given declaration in all derived environment branches. Realizations will run using the given environment and options to ensure deterministic results. Note that while we check that the function isn't called before the declaration is actually added to the environment, we cannot automatically check that it isn't otherwise called too early in the sense that helper declarations and environment extension state that may be relevant to realizations may not have been added yet. We do check that we are not calling it from a different branch than c was added on, which would be definitely too late. Thus, this function should generally be called in elaborators calling addDecl (when that declaration is a plausible target for realization) at the latest possible point, i.e. at the very end of the elaborator or just before a first realization may be triggered if any.

                                                                                                                      Equations
                                                                                                                      Instances For