Documentation

Lean.CoreM

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

    Cache for the CoreM monad

    Instances For
      Equations

      State for the CoreM monad.

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

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

                              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
                                  @[inline]
                                  Equations
                                  Instances For
                                    @[inline]
                                    Equations
                                    • x.run' ctx s = Prod.fst <$> x.run ctx s
                                    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.
                                        def Lean.Core.withIncRecDepth {m : TypeType u_1} {α : Type} [Monad m] [MonadControlT Lean.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 : Lake.Name) (optionName : Lake.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 : Lake.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 Lean.CoreM m] (x : m α) :
                                                  m α
                                                  Equations
                                                  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
                                                        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.
                                                            @[inline]
                                                            def Lean.withAtLeastMaxRecDepth {m : TypeType u_1} {α : Type} [MonadFunctorT Lean.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 Lean.Exception m] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.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 Lean.Exception m] (ids : List Lean.InternalExceptionId) (x : m α) (h : Lean.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
                                                                        @[extern lean_lcnf_compile_decls]
                                                                        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 diagnostic information collection is enabled.

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

                                                                                Equations
                                                                                • ex.isRuntime = (ex.isMaxHeartbeat || ex.isMaxRecDepth)
                                                                                Instances For

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

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[inline]

                                                                                    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]

                                                                                      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
                                                                                        Instances
                                                                                          Equations
                                                                                          @[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 Lean.CoreM m] [Monad m] (f : {α : Type} → Lean.CoreM αLean.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 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.
                                                                                            Instances For