feat: better #eval command (#5627)

This refactors and improves the `#eval` command, introducing some new
features.
* Now evaluated results can be represented using `ToExpr` and pretty
printing. This means **hoverable output**. If `ToExpr` fails, it then
tries `Repr` and then `ToString`. The `eval.pp` option controls whether
or not to try `ToExpr`.
* There is now **auto-derivation** of `Repr` instances, enabled with the
`pp.derive.repr` option (default to **true**). For example:
  ```lean
  inductive Baz
    | a | b

  #eval Baz.a
  -- Baz.a
  ```
It simply does `deriving instance Repr for Baz` when there's no way to
represent `Baz`. If core Lean gets `ToExpr` derive handlers, they could
be used here as well.
* The option `eval.type` controls whether or not to include the type in
the output. For now the default is false.
* Now things like `#eval do return 2` work. It tries using
`CommandElabM`, `TermElabM`, or `IO` when the monad is unknown.
* Now there is no longer `Lean.Eval` or `Lean.MetaEval`. These each used
to be responsible for both adapting monads and printing results. The
concerns have been split into two. (1) The `MonadEval` class is
responsible for adapting monads for evaluation (it is similar to
`MonadLift`, but instances are allowed to use default data when
initializing state) and (2) finding a way to represent results is
handled separately.
* Error messages about failed instance synthesis are now more precise.
Once it detects that a `MonadEval` class applies, then the error message
will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
* Fixes a bug where `Repr`/`ToString` instances can't be found by
unfolding types "under the monad". For example, this works now:
  ```lean
  def Foo := List Nat
  def Foo.mk (l : List Nat) : Foo := l
  #eval show Lean.CoreM Foo from do return Foo.mk [1,2,3]
  ```
* Elaboration errors now abort evaluation. This eliminates some
not-so-relevant error messages.
* Now evaluating a value of type `m Unit` never prints a blank message.
* Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log
messages.

The `run_cmd`, `run_elab`, and `run_meta` commands are now frontends for
`#eval`.

src/Init/Notation.lean

@@ -535,24 +535,21 @@ syntax (name := includeStr) "include_str " term : term
 
 /--
 The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
-This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
-except that it doesn't print an empty diagnostic.
+This is the same as `#eval show CommandElabM Unit from discard do doSeq`.
 -/
 syntax (name := runCmd) "run_cmd " doSeq : command
 
 /--
 The `run_elab doSeq` command executes code in `TermElabM Unit`.
-This is almost the same as `#eval show TermElabM Unit from do doSeq`,
-except that it doesn't print an empty diagnostic.
+This is the same as `#eval show TermElabM Unit from discard do doSeq`.
 -/
 syntax (name := runElab) "run_elab " doSeq : command
 
 /--
 The `run_meta doSeq` command executes code in `MetaM Unit`.
-This is almost the same as `#eval show MetaM Unit from do doSeq`,
-except that it doesn't print an empty diagnostic.
+This is the same as `#eval show MetaM Unit from do discard doSeq`.
 
-(This is effectively a synonym for `run_elab`.)
+(This is effectively a synonym for `run_elab` since `MetaM` lifts to `TermElabM`.)
 -/
 syntax (name := runMeta) "run_meta " doSeq : command
 

src/Init/Prelude.lean

@@ -2869,6 +2869,32 @@ instance (m n o) [MonadLift n o] [MonadLiftT m n] : MonadLiftT m o where
 instance (m) : MonadLiftT m m where
   monadLift x := x
 
+/--
+Typeclass used for adapting monads. This is similar to `MonadLift`, but instances are allowed to
+make use of default state for the purpose of synthesizing such an instance, if necessary.
+Every `MonadLift` instance gives a `MonadEval` instance.
+
+The purpose of this class is for the `#eval` command,
+which looks for a `MonadEval m CommandElabM` or `MonadEval m IO` instance.
+-/
+class MonadEval (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
+  /-- Evaluates a value from monad `m` into monad `n`. -/
+  monadEval : {α : Type u} → m α → n α
+
+instance [MonadLift m n] : MonadEval m n where
+  monadEval := MonadLift.monadLift
+
+/-- The transitive closure of `MonadEval`. -/
+class MonadEvalT (m : Type u → Type v) (n : Type u → Type w) where
+  /-- Evaluates a value from monad `m` into monad `n`. -/
+  monadEval : {α : Type u} → m α → n α
+
+instance (m n o) [MonadEval n o] [MonadEvalT m n] : MonadEvalT m o where
+  monadEval x := MonadEval.monadEval (m := n) (MonadEvalT.monadEval x)
+
+instance (m) : MonadEvalT m m where
+  monadEval x := x
+
 /--
 A functor in the category of monads. Can be used to lift monad-transforming functions.
 Based on [`MFunctor`] from the `pipes` Haskell package, but not restricted to

src/Init/System/IO.lean

@@ -928,41 +928,6 @@ def withIsolatedStreams [Monad m] [MonadFinally m] [MonadLiftT BaseIO m] (x : m
 end FS
 end IO
 
-universe u
-
-namespace Lean
-
-/-- Typeclass used for presenting the output of an `#eval` command. -/
-class Eval (α : Type u) where
-  -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
-  -- so that `()` output is hidden in chained instances such as for some `IO Unit`.
-  -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`)
-  eval : (Unit → α) → (hideUnit : Bool := true) → IO Unit
-
-instance instEval [ToString α] : Eval α where
-  eval a _ := IO.println (toString (a ()))
-
-instance [Repr α] : Eval α where
-  eval a _ := IO.println (repr (a ()))
-
-instance : Eval Unit where
-  eval u hideUnit := if hideUnit then pure () else IO.println (repr (u ()))
-
-instance [Eval α] : Eval (IO α) where
-  eval x _ := do
-    let a ← x ()
-    Eval.eval fun _ => a
-
-instance [Eval α] : Eval (BaseIO α) where
-  eval x _ := do
-    let a ← x ()
-    Eval.eval fun _ => a
-
-def runEval [Eval α] (a : Unit → α) : IO (String × Except IO.Error Unit) :=
-  IO.FS.withIsolatedStreams (Eval.eval a false |>.toBaseIO)
-
-end Lean
-
 syntax "println! " (interpolatedStr(term) <|> term) : term
 
 macro_rules

src/Lean.lean

@@ -20,7 +20,6 @@ import Lean.MetavarContext
 import Lean.AuxRecursor
 import Lean.Meta
 import Lean.Util
-import Lean.Eval
 import Lean.Structure
 import Lean.PrettyPrinter
 import Lean.CoreM

src/Lean/CoreM.lean

@@ -7,7 +7,6 @@ prelude
 import Lean.Util.RecDepth
 import Lean.Util.Trace
 import Lean.Log
-import Lean.Eval
 import Lean.ResolveName
 import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
@@ -277,12 +276,6 @@ def mkFreshUserName (n : Name) : CoreM Name :=
   | Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx
   | Except.ok a                            => return a
 
-instance [MetaEval α] : MetaEval (CoreM α) where
-  eval env opts x _ := do
-    let x : CoreM α := do try x finally printTraces
-    let (a, s) ← (withConsistentCtx x).toIO { fileName := "<CoreM>", fileMap := default, options := opts } { env := env }
-    MetaEval.eval s.env opts a (hideUnit := true)
-
 -- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)

src/Lean/Elab.lean

@@ -42,6 +42,7 @@ import Lean.Elab.Notation
 import Lean.Elab.Mixfix
 import Lean.Elab.MacroRules
 import Lean.Elab.BuiltinCommand
+import Lean.Elab.BuiltinEvalCommand
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.Eval
 import Lean.Elab.Calc

src/Lean/Elab/BuiltinCommand.lean

@@ -311,167 +311,6 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
     failIfSucceeds <| elabCheckCore (ignoreStuckTC := false) (← `(#check $term))
   | _ => throwUnsupportedSyntax
 
-private def mkEvalInstCore (evalClassName : Name) (e : Expr) : MetaM Expr := do
-  let α    ← inferType e
-  let u    ← getDecLevel α
-  let inst := mkApp (Lean.mkConst evalClassName [u]) α
-  try
-    synthInstance inst
-  catch _ =>
-    -- Put `α` in WHNF and try again
-    try
-      let α ← whnf α
-      synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
-    catch _ =>
-      -- Fully reduce `α` and try again
-      try
-        let α ← reduce (skipTypes := false) α
-        synthInstance (mkApp (Lean.mkConst evalClassName [u]) α)
-      catch _ =>
-        throwError "expression{indentExpr e}\nhas type{indentExpr α}\nbut instance{indentExpr inst}\nfailed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `{evalClassName}` class"
-
-private def mkRunMetaEval (e : Expr) : MetaM Expr :=
-  withLocalDeclD `env (mkConst ``Lean.Environment) fun env =>
-  withLocalDeclD `opts (mkConst ``Lean.Options) fun opts => do
-    let α ← inferType e
-    let u ← getDecLevel α
-    let instVal ← mkEvalInstCore ``Lean.MetaEval e
-    let e := mkAppN (mkConst ``Lean.runMetaEval [u]) #[α, instVal, env, opts, e]
-    instantiateMVars (← mkLambdaFVars #[env, opts] e)
-
-private def mkRunEval (e : Expr) : MetaM Expr := do
-  let α ← inferType e
-  let u ← getDecLevel α
-  let instVal ← mkEvalInstCore ``Lean.Eval e
-  instantiateMVars (mkAppN (mkConst ``Lean.runEval [u]) #[α, instVal, mkSimpleThunk e])
-
-unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax): CommandElabM Unit := do
-    let declName := `_eval
-    let addAndCompile (value : Expr) : TermElabM Unit := do
-      let value ← Term.levelMVarToParam (← instantiateMVars value)
-      let type ← inferType value
-      let us := collectLevelParams {} value |>.params
-      let value ← instantiateMVars value
-      let decl := Declaration.defnDecl {
-        name        := declName
-        levelParams := us.toList
-        type        := type
-        value       := value
-        hints       := ReducibilityHints.opaque
-        safety      := DefinitionSafety.unsafe
-      }
-      Term.ensureNoUnassignedMVars decl
-      addAndCompile decl
-    -- Check for sorry axioms
-    let checkSorry (declName : Name) : MetaM Unit := do
-      unless bang do
-        let axioms ← collectAxioms declName
-        if axioms.contains ``sorryAx then
-          throwError ("cannot evaluate expression that depends on the `sorry` axiom.\nUse `#eval!` to " ++
-            "evaluate nevertheless (which may cause lean to crash).")
-    -- Elaborate `term`
-    let elabEvalTerm : TermElabM Expr := do
-      let e ← Term.elabTerm term none
-      Term.synthesizeSyntheticMVarsNoPostponing
-      if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then throwAbortTerm
-      if (← isProp e) then
-        mkDecide e
-      else
-        return e
-    -- Evaluate using term using `MetaEval` class.
-    let elabMetaEval : CommandElabM Unit := do
-      -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
-      -- we don't pollute the environment with auxliary declarations.
-      -- We have special support for `CommandElabM` to ensure `#eval` can be used to execute commands
-      -- that modify `CommandElabM` state not just the `Environment`.
-      let act : Sum (CommandElabM Unit) (Environment → Options → IO (String × Except IO.Error Environment)) ←
-        runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
-          let e ← elabEvalTerm
-          let eType ← instantiateMVars (← inferType e)
-          if eType.isAppOfArity ``CommandElabM 1 then
-            let mut stx ← Term.exprToSyntax e
-            unless (← isDefEq eType.appArg! (mkConst ``Unit)) do
-              stx ← `($stx >>= fun v => IO.println (repr v))
-            let act ← Lean.Elab.Term.evalTerm (CommandElabM Unit) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit)) stx
-            pure <| Sum.inl act
-          else
-            let e ← mkRunMetaEval e
-            addAndCompile e
-            checkSorry declName
-            let act ← evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName
-            pure <| Sum.inr act
-      match act with
-      | .inl act => act
-      | .inr act =>
-        let (out, res) ← act (← getEnv) (← getOptions)
-        logInfoAt tk out
-        match res with
-        | Except.error e => throwError e.toString
-        | Except.ok env  => setEnv env; pure ()
-    -- Evaluate using term using `Eval` class.
-    let elabEval : CommandElabM Unit := runTermElabM fun _ => Term.withDeclName declName do withoutModifyingEnv do
-      -- fall back to non-meta eval if MetaEval hasn't been defined yet
-      -- modify e to `runEval e`
-      let e ← mkRunEval (← elabEvalTerm)
-      addAndCompile e
-      checkSorry declName
-      let act ← evalConst (IO (String × Except IO.Error Unit)) declName
-      let (out, res) ← liftM (m := IO) act
-      logInfoAt tk out
-      match res with
-      | Except.error e => throwError e.toString
-      | Except.ok _    => pure ()
-    if (← getEnv).contains ``Lean.MetaEval then do
-      elabMetaEval
-    else
-      elabEval
-
-@[implemented_by elabEvalCoreUnsafe]
-opaque elabEvalCore (bang : Bool) (tk term : Syntax): CommandElabM Unit
-
-@[builtin_command_elab «eval»]
-def elabEval : CommandElab
-  | `(#eval%$tk $term) => elabEvalCore false tk term
-  | _ => throwUnsupportedSyntax
-
-@[builtin_command_elab evalBang]
-def elabEvalBang : CommandElab
-  | `(Parser.Command.evalBang|#eval!%$tk $term) => elabEvalCore true tk term
-  | _ => throwUnsupportedSyntax
-
-private def checkImportsForRunCmds : CommandElabM Unit := do
-  unless (← getEnv).contains ``CommandElabM do
-    throwError "to use this command, include `import Lean.Elab.Command`"
-
-@[builtin_command_elab runCmd]
-def elabRunCmd : CommandElab
-  | `(run_cmd $elems:doSeq) => do
-    checkImportsForRunCmds
-    (← liftTermElabM <| Term.withDeclName `_run_cmd <|
-      unsafe Term.evalTerm (CommandElabM Unit)
-        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(discard do $elems)))
-  | _ => throwUnsupportedSyntax
-
-@[builtin_command_elab runElab]
-def elabRunElab : CommandElab
-  | `(run_elab $elems:doSeq) => do
-    checkImportsForRunCmds
-    (← liftTermElabM <| Term.withDeclName `_run_elab <|
-      unsafe Term.evalTerm (CommandElabM Unit)
-        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(Command.liftTermElabM <| discard do $elems)))
-  | _ => throwUnsupportedSyntax
-
-@[builtin_command_elab runMeta]
-def elabRunMeta : CommandElab := fun stx =>
-  match stx with
-  | `(run_meta $elems:doSeq) => do
-     checkImportsForRunCmds
-     let stxNew ← `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems))
-     withMacroExpansion stx stxNew do elabCommand stxNew
-  | _ => throwUnsupportedSyntax
-
 @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do
   let term := stx[1]
   withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -0,0 +1,283 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Lean.Util.CollectLevelParams
+import Lean.Util.CollectAxioms
+import Lean.Meta.Reduce
+import Lean.Elab.Eval
+import Lean.Elab.Deriving.Basic
+
+/-!
+# Implementation of `#eval` command
+-/
+
+namespace Lean.Elab.Command
+open Meta
+
+register_builtin_option eval.pp : Bool := {
+  defValue := true
+  descr    := "('#eval' command) enables using 'ToExpr' instances to pretty print the result, \
+               otherwise uses 'Repr' or 'ToString' instances"
+}
+
+register_builtin_option eval.type : Bool := {
+  defValue := false -- TODO: set to 'true'
+  descr    := "('#eval' command) enables pretty printing the type of the result"
+}
+
+register_builtin_option eval.derive.repr : Bool := {
+  defValue := true
+  descr    := "('#eval' command) enables auto-deriving 'Repr' instances as a fallback"
+}
+
+builtin_initialize
+  registerTraceClass `Elab.eval
+
+/--
+Elaborates the term, ensuring the result has no expression metavariables.
+If there would be unsolved-for metavariables, tries hinting that the resulting type
+is a monadic value with the `CommandElabM`, `TermElabM`, or `IO` monads.
+Throws errors if the term is a proof or a type, but lifts props to `Bool` using `mkDecide`.
+-/
+private def elabTermForEval (term : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
+  let ty ← expectedType?.getDM mkFreshTypeMVar
+  let e ← Term.elabTermEnsuringType term ty
+  synthesizeWithHinting ty
+  let e ← instantiateMVars e
+  if (← Term.logUnassignedUsingErrorInfos (← getMVars e)) then throwAbortTerm
+  if ← isProof e then
+    throwError m!"cannot evaluate, proofs are not computationally relevant"
+  let e ← if (← isProp e) then mkDecide e else pure e
+  if ← isType e then
+    throwError m!"cannot evaluate, types are not computationally relevant"
+  trace[Elab.eval] "elaborated term:{indentExpr e}"
+  return e
+where
+  /-- Try different strategies to make `Term.synthesizeSyntheticMVarsNoPostponing` succeed. -/
+  synthesizeWithHinting (ty : Expr) : TermElabM Unit := do
+    Term.synthesizeSyntheticMVarsUsingDefault
+    let s ← saveState
+    try
+      Term.synthesizeSyntheticMVarsNoPostponing
+    catch ex =>
+      let exS ← saveState
+      -- Try hinting that `ty` is a monad application.
+      for m in #[``CommandElabM, ``TermElabM, ``IO] do
+        s.restore true
+        try
+          if ← isDefEq ty (← mkFreshMonadApp m) then
+            Term.synthesizeSyntheticMVarsNoPostponing
+            return
+        catch _ => pure ()
+      -- None of the hints worked, so throw the original error.
+      exS.restore true
+      throw ex
+  mkFreshMonadApp (n : Name) : MetaM Expr := do
+    let m ← mkConstWithFreshMVarLevels n
+    let (args, _, _) ← forallMetaBoundedTelescope (← inferType m) 1
+    return mkAppN m args
+
+private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Unit := do
+  let value ← Term.levelMVarToParam (← instantiateMVars value)
+  let type ← inferType value
+  let us := collectLevelParams {} value |>.params
+  let decl := Declaration.defnDecl {
+    name        := declName
+    levelParams := us.toList
+    type        := type
+    value       := value
+    hints       := ReducibilityHints.opaque
+    safety      := DefinitionSafety.unsafe
+  }
+  Term.ensureNoUnassignedMVars decl
+  addAndCompile decl
+  unless allowSorry do
+    let axioms ← collectAxioms declName
+    if axioms.contains ``sorryAx then
+      throwError "\
+        aborting evaluation since the expression depends on the 'sorry' axiom, \
+        which can lead to runtime instability and crashes.\n\n\
+        To attempt to evaluate anyway despite the risks, use the '#eval!' command."
+
+/--
+Try to make a `@projFn ty inst e` application, even if it takes unfolding the type `ty` of `e` to synthesize the instance `inst`.
+-/
+private partial def mkDeltaInstProj (inst projFn : Name) (e : Expr) (ty? : Option Expr := none) (tryReduce : Bool := true) : MetaM Expr := do
+  let ty ← ty?.getDM (inferType e)
+  if let .some inst ← trySynthInstance (← mkAppM inst #[ty]) then
+    mkAppOptM projFn #[ty, inst, e]
+  else
+    let ty ← whnfCore ty
+    let some ty ← unfoldDefinition? ty
+      | guard tryReduce
+        -- Reducing the type is a strategy `#eval` used before the refactor of #5627.
+        -- The test lean/run/hlistOverload.lean depends on it, so we preserve the behavior.
+        let ty ← reduce (skipTypes := false) ty
+        mkDeltaInstProj inst projFn e ty (tryReduce := false)
+    mkDeltaInstProj inst projFn e ty tryReduce
+
+/-- Try to make a `toString e` application, even if it takes unfolding the type of `e` to find a `ToString` instance. -/
+private def mkToString (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do
+  mkDeltaInstProj ``ToString ``toString e ty?
+
+/-- Try to make a `repr e` application, even if it takes unfolding the type of `e` to find a `Repr` instance. -/
+private def mkRepr (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do
+  mkDeltaInstProj ``Repr ``repr e ty?
+
+/-- Try to make a `toExpr e` application, even if it takes unfolding the type of `e` to find a `ToExpr` instance. -/
+private def mkToExpr (e : Expr) (ty? : Option Expr := none) : MetaM Expr := do
+  mkDeltaInstProj ``ToExpr ``toExpr e ty?
+
+/--
+Returns a representation of `e` using `Format`, or else fails.
+If the `eval.derive.repr` option is true, then tries automatically deriving a `Repr` instance first.
+Currently auto-derivation does not attempt to derive recursively.
+-/
+private def mkFormat (e : Expr) : MetaM Expr := do
+  mkRepr e <|> (do mkAppM ``Std.Format.text #[← mkToString e])
+  <|> do
+    if eval.derive.repr.get (← getOptions) then
+      if let .const name _ := (← whnf (← inferType e)).getAppFn then
+        try
+          trace[Elab.eval] "Attempting to derive a 'Repr' instance for '{MessageData.ofConstName name}'"
+          liftCommandElabM do applyDerivingHandlers ``Repr #[name] none
+          resetSynthInstanceCache
+          return ← mkRepr e
+        catch ex =>
+          trace[Elab.eval] "Failed to use derived 'Repr' instance. Exception: {ex.toMessageData}"
+    throwError m!"could not synthesize a 'Repr' or 'ToString' instance for type{indentExpr (← inferType e)}"
+
+/--
+Returns a representation of `e` using `MessageData`, or else fails.
+Tries `mkFormat` if a `ToExpr` instance can't be synthesized.
+-/
+private def mkMessageData (e : Expr) : MetaM Expr := do
+  (do guard <| eval.pp.get (← getOptions); mkAppM ``MessageData.ofExpr #[← mkToExpr e])
+  <|> (return mkApp (mkConst ``MessageData.ofFormat) (← mkFormat e))
+  <|> do throwError m!"could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type{indentExpr (← inferType e)}"
+
+private structure EvalAction where
+  eval : CommandElabM MessageData
+  /-- Whether to print the result of evaluation.
+  If `some`, the expression is what type to use for the type ascription when `pp.type` is true. -/
+  printVal : Option Expr
+
+unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit := withRef tk do
+  let declName := `_eval
+  -- `t` is either `MessageData` or `Format`, and `mkT` is for synthesizing an expression that yields a `t`.
+  -- The `toMessageData` function adapts `t` to `MessageData`.
+  let mkAct {t : Type} [Inhabited t] (toMessageData : t → MessageData) (mkT : Expr → MetaM Expr) (e : Expr) : TermElabM EvalAction := do
+    -- Create a monadic action given the name of the monad `mc`, the monad `m` itself,
+    -- and an expression `e` to evaluate in this monad.
+    -- A trick here is that `mkMAct?` makes use of `MonadEval` instances are currently available in this stage,
+    -- and we do not need them to be available in the target environment.
+    let mkMAct? (mc : Name) (m : Type → Type) [Monad m] [MonadEvalT m CommandElabM] (e : Expr) : TermElabM (Option EvalAction) := do
+      let some e ← observing? (mkAppOptM ``MonadEvalT.monadEval #[none, mkConst mc, none, none, e])
+        | return none
+      let eType := e.appFn!.appArg!
+      if ← isDefEq eType (mkConst ``Unit) then
+        addAndCompileExprForEval declName e (allowSorry := bang)
+        let mf : m Unit ← evalConst (m Unit) declName
+        return some { eval := do MonadEvalT.monadEval mf; pure "", printVal := none }
+      else
+        let rf ← withLocalDeclD `x eType fun x => do mkLambdaFVars #[x] (← mkT x)
+        let r ← mkAppM ``Functor.map #[rf, e]
+        addAndCompileExprForEval declName r (allowSorry := bang)
+        let mf : m t ← evalConst (m t) declName
+        return some { eval := toMessageData <$> MonadEvalT.monadEval mf, printVal := some eType }
+    if let some act ← mkMAct? ``CommandElabM CommandElabM e
+                    -- Fallbacks in case we are in the Lean package but don't have `CommandElabM` yet
+                    <||> mkMAct? ``TermElabM TermElabM e <||> mkMAct? ``MetaM MetaM e <||> mkMAct? ``CoreM CoreM e
+                    -- Fallback in case nothing is imported
+                    <||> mkMAct? ``IO IO e then
+      return act
+    else
+      -- Otherwise, assume this is a pure value.
+      -- There is no need to adapt pure values to `CommandElabM`.
+      -- This enables `#eval` to work on pure values even when `CommandElabM` is not available.
+      let r ← try mkT e catch ex => do
+        -- Diagnose whether the value is monadic for a representable value, since it's better to mention `MonadEval` in that case.
+        try
+          let some (m, ty) ← isTypeApp? (← inferType e) | failure
+          guard <| (← isMonad? m).isSome
+          -- Verify that there is a way to form some representation:
+          discard <| withLocalDeclD `x ty fun x => mkT x
+        catch _ =>
+          throw ex
+        throwError m!"unable to synthesize '{MessageData.ofConstName ``MonadEval}' instance \
+          to adapt{indentExpr (← inferType e)}\n\
+          to '{MessageData.ofConstName ``IO}' or '{MessageData.ofConstName ``CommandElabM}'."
+      addAndCompileExprForEval declName r (allowSorry := bang)
+      -- `evalConst` may emit IO, but this is collected by `withIsolatedStreams` below.
+      let r ← toMessageData <$> evalConst t declName
+      return { eval := pure r, printVal := some (← inferType e) }
+  let (output, exOrRes) ← IO.FS.withIsolatedStreams do
+    try
+      -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
+      -- we don't pollute the environment with auxiliary declarations.
+      let act : EvalAction ← liftTermElabM do Term.withDeclName declName do withoutModifyingEnv do
+        let e ← elabTermForEval term expectedType?
+        -- If there is an elaboration error, don't evaluate!
+        if e.hasSyntheticSorry then throwAbortTerm
+        -- We want `#eval` to work even in the core library, so if `ofFormat` isn't available,
+        -- we fall back on a `Format`-based approach.
+        if (← getEnv).contains ``Lean.MessageData.ofFormat then
+          mkAct id (mkMessageData ·) e
+        else
+          mkAct Lean.MessageData.ofFormat (mkFormat ·) e
+      let res ← act.eval
+      return Sum.inr (res, act.printVal)
+    catch ex =>
+      return Sum.inl ex
+  if !output.isEmpty then logInfoAt tk output
+  match exOrRes with
+  | .inl ex => logException ex
+  | .inr (_, none) => pure ()
+  | .inr (res, some type) =>
+    if eval.type.get (← getOptions) then
+      logInfo m!"{res} : {type}"
+    else
+      logInfo res
+
+@[implemented_by elabEvalCoreUnsafe]
+opaque elabEvalCore (bang : Bool) (tk term : Syntax) (expectedType? : Option Expr) : CommandElabM Unit
+
+@[builtin_command_elab «eval»]
+def elabEval : CommandElab
+  | `(#eval%$tk $term) => elabEvalCore false tk term none
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab evalBang]
+def elabEvalBang : CommandElab
+  | `(#eval!%$tk $term) => elabEvalCore true tk term none
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runCmd]
+def elabRunCmd : CommandElab
+  | `(run_cmd%$tk $elems:doSeq) => do
+    unless (← getEnv).contains ``CommandElabM do
+      throwError "to use this command, include `import Lean.Elab.Command`"
+    elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runElab]
+def elabRunElab : CommandElab
+  | `(run_elab%$tk $elems:doSeq) => do
+    unless (← getEnv).contains ``TermElabM do
+      throwError "to use this command, include `import Lean.Elab.Term`"
+    elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``TermElabM) (mkConst ``Unit))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runMeta]
+def elabRunMeta : CommandElab := fun stx =>
+  match stx with
+  | `(run_meta%$tk $elems:doSeq) => do
+    unless (← getEnv).contains ``MetaM do
+      throwError "to use this command, include `import Lean.Meta.Basic`"
+    elabEvalCore false tk (← `(discard do $elems)) (mkApp (mkConst ``MetaM) (mkConst ``Unit))
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Command

src/Lean/Elab/Command.lean

@@ -619,6 +619,9 @@ def liftTermElabM (x : TermElabM α) : CommandElabM α := do
   let ((ea, _), _) ← runCore x
   MonadExcept.ofExcept ea
 
+instance : MonadEval TermElabM CommandElabM where
+  monadEval := 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.
@@ -727,6 +730,12 @@ 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.
 -/
 def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
   let (a, commandState) ←

src/Lean/Elab/Term.lean

@@ -2047,13 +2047,6 @@ def TermElabM.toIO (x : TermElabM α)
   let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta
   return (a, sCore, sMeta, s)
 
-instance [MetaEval α] : MetaEval (TermElabM α) where
-  eval env opts x _ := do
-    let x : TermElabM α := do
-      try x finally
-        (← Core.getMessageLog).forM fun msg => do IO.println (← msg.toString)
-    MetaEval.eval env opts (hideUnit := true) <| x.run' {}
-
 /--
   Execute `x` and then tries to solve pending universe constraints.
   Note that, stuck constraints will not be discarded.

src/Lean/Eval.lean

@@ -1,27 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, Sebastian Ullrich
--/
-prelude
-import Lean.Environment
-
-namespace Lean
-
-universe u
-
-/--
-`Eval` extension that gives access to the current environment & options.
-The basic `Eval` class is in the prelude and should not depend on these
-types.
--/
-class MetaEval (α : Type u) where
-  eval : Environment → Options → α → (hideUnit : Bool) → IO Environment
-
-instance {α : Type u} [Eval α] : MetaEval α :=
-  ⟨fun env _ a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env⟩
-
-def runMetaEval {α : Type u} [MetaEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) :=
-  IO.FS.withIsolatedStreams (MetaEval.eval env opts a false |>.toBaseIO)
-
-end Lean

src/Lean/Meta/Basic.lean

@@ -456,9 +456,6 @@ instance : MonadBacktrack SavedState MetaM where
   let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore
   pure (a, sCore, s)
 
-instance [MetaEval α] : MetaEval (MetaM α) :=
-  ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩
-
 protected def throwIsDefEqStuck : MetaM α :=
   throw <| Exception.internal isDefEqStuckExceptionId
 
@@ -501,6 +498,9 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
 
+@[inline] def resetSynthInstanceCache : MetaM Unit :=
+  modifyCache fun c => {c with synthInstance := {}}
+
 @[inline] def modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit := do
   if (← isDiagnosticsEnabled) then
     modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache, zetaDeltaFVarIds, postponed, diag := f diag }

src/Lean/Parser/Command.lean

@@ -462,9 +462,33 @@ structure Pair (α : Type u) (β : Type v) : Type (max u v) where
   "#check " >> termParser
 @[builtin_command_parser] def check_failure  := leading_parser
   "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
-@[builtin_command_parser] def eval           := leading_parser
+/--
+`#eval e` evaluates the expression `e` by compiling and evaluating it.
+
+* The command attempts to use `ToExpr`, `Repr`, or `ToString` instances to print the result.
+* If `e` is a monadic value of type `m ty`, then the command tries to adapt the monad `m`
+  to one of the monads that `#eval` supports, which include `IO`, `CoreM`, `MetaM`, `TermElabM`, and `CommandElabM`.
+  Users can define `MonadEval` instances to extend the list of supported monads.
+
+The `#eval` command gracefully degrades in capability depending on what is imported.
+Importing the `Lean.Elab.Command` module provides full capabilities.
+
+Due to unsoundness, `#eval` refuses to evaluate expressions that depend on `sorry`, even indirectly,
+since the presence of `sorry` can lead to runtime instability and crashes.
+This check can be overridden with the `#eval! e` command.
+
+Options:
+* If `eval.pp` is true (default: true) then tries to use `ToExpr` instances to make use of the
+  usual pretty printer. Otherwise, only tries using `Repr` and `ToString` instances.
+* If `eval.type` is true (default: false) then pretty prints the type of the evaluated value.
+* If `eval.derive.repr` is true (default: true) then attempts to auto-derive a `Repr` instance
+  when there is no other way to print the result.
+
+See also: `#reduce e` for evaluation by term reduction.
+-/
+@[builtin_command_parser, builtin_doc] def eval := leading_parser
   "#eval " >> termParser
-@[builtin_command_parser] def evalBang       := leading_parser
+@[builtin_command_parser, inherit_doc eval] def evalBang := leading_parser
   "#eval! " >> termParser
 @[builtin_command_parser] def synth          := leading_parser
   "#synth " >> termParser

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
-some { range := { pos := { line := 194, column := 42 },
-             charUtf16 := 42,
-             endPos := { line := 200, column := 31 },
-             endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 194, column := 46 },
-                      charUtf16 := 46,
-                      endPos := { line := 194, column := 58 },
-                      endCharUtf16 := 58 } }
+some
+  {
+    range :=
+      { pos := { line := 194, column := 42 }, charUtf16 := 42, endPos := { line := 200, column := 31 },
+        endCharUtf16 := 31 },
+    selectionRange :=
+      { pos := { line := 194, column := 46 }, charUtf16 := 46, endPos := { line := 194, column := 58 },
+        endCharUtf16 := 58 } }

tests/lean/1240.lean.expected.out

@@ -1,2 +1 @@
-
-1240.lean:4:0-5:65: error: import failed, trying to import module with anonymous name
+1240.lean:4:0-4:5: error: import failed, trying to import module with anonymous name

tests/lean/277a.lean.expected.out

@@ -1,3 +1 @@
 277a.lean:4:7-4:15: error: unknown identifier 'nonexistent'
-277a.lean:4:0-4:25: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/277b.lean.expected.out

@@ -1,4 +1,2 @@
 277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
   List Point
-277b.lean:8:0-8:16: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/440.lean.expected.out

@@ -6,5 +6,6 @@ context:
 x : Nat
 ⊢ Nat
 f (x : Nat) : Nat
-440.lean:11:0-11:9: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
+440.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+
+To attempt to evaluate anyway despite the risks, use the '#eval!' command.

tests/lean/474.lean

@@ -1,6 +1,13 @@
 import Lean
 open Lean Meta
 
+open PrettyPrinter Delaborator SubExpr in
+@[delab fvar]
+def delabFVar : Delab := do
+  let Expr.fvar fvarId ← getExpr | unreachable!
+  let none := (← getLCtx).find? fvarId | failure
+  return mkIdent `FREE
+
 #eval do
   let e ← withLetDecl `y (mkConst ``Nat) (mkConst ``Nat.zero) fun y => do
     let m ← mkFreshExprMVar (mkConst ``Nat)

tests/lean/474.lean.expected.out

@@ -1,7 +1,7 @@
 let y := Nat.zero;
 y.add y
 fun y_1 => y.add y_1
-fun y => Nat.add _fvar.1 y
+fun y => Nat.add FREE y
 fun (y : Nat) => Nat.add y y
 ?m.add y
 Nat.add (?m #0) #0

tests/lean/casesOnCases.lean.expected.out

@@ -1,2 +0,0 @@
-
-

tests/lean/coe.lean.expected.out

@@ -1,5 +1,3 @@
-
-
 ↑n : Nat
 ↑n : Nat
 ⇑f : Nat → Nat

tests/lean/evalInstMessage.lean.expected.out

@@ -1,7 +1,2 @@
-evalInstMessage.lean:3:0-3:12: error: expression
-  double
-has type
+evalInstMessage.lean:3:0-3:5: error: could not synthesize a 'Repr' or 'ToString' instance for type
   Nat → Nat
-but instance
-  Lean.Eval (Nat → Nat)
-failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.Eval` class

tests/lean/evalSorry.lean.expected.out

@@ -7,7 +7,9 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-evalSorry.lean:7:0-7:15: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
-evalSorry.lean:11:0-11:15: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
+evalSorry.lean:7:0-7:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+
+To attempt to evaluate anyway despite the risks, use the '#eval!' command.
+evalSorry.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+
+To attempt to evaluate anyway despite the risks, use the '#eval!' command.

tests/lean/eval_except.lean.expected.out

@@ -1,5 +1,3 @@
-
-eval_except.lean:4:0-4:57: error: this is my error
-
-eval_except.lean:5:0-5:80: error: no such file or directory (error code: 31)
+eval_except.lean:4:0-4:5: error: this is my error
+eval_except.lean:5:0-5:5: error: no such file or directory (error code: 31)
   file: file.ext

tests/lean/file_not_found.lean.expected.out

@@ -1,9 +1,5 @@
-
-file_not_found.lean:6:0-6:77: error: no such file or directory (error code: 2)
+file_not_found.lean:6:0-6:5: error: no such file or directory (error code: 2)
   file: non-existent-file.txt
-
-
-file_not_found.lean:13:0-13:69: error: permission denied (error code: 13)
+file_not_found.lean:13:0-13:5: error: permission denied (error code: 13)
   file: readonly.txt
-
-file_not_found.lean:14:0-18:9: error: invalid argument (error code: 9, bad file descriptor)
+file_not_found.lean:14:0-14:5: error: invalid argument (error code: 9, bad file descriptor)

tests/lean/implicitArgumentError.lean

@@ -9,9 +9,10 @@ def foo {n : Nat} := 2*n
 
 /--
 error: don't know how to synthesize implicit argument 'n'
-  @foo ?m.64
+  @foo ?_
 context:
 ⊢ Nat
 -/
 #guard_msgs in
+set_option pp.mvars false in
 #eval foo

tests/lean/inlineIssue.lean.expected.out

@@ -1,2 +0,0 @@
-
-

tests/lean/interactive/incrementalCommand.lean.expected.out

@@ -10,7 +10,7 @@ w
    "severity": 3,
    "range":
    {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}},
-   "message": "\"import\"\n",
+   "message": "\"import\"",
    "fullRange":
    {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}
 {"version": 2,
@@ -20,7 +20,7 @@ w
    "severity": 3,
    "range":
    {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}},
-   "message": "\"import\"\n",
+   "message": "\"import\"",
    "fullRange":
    {"start": {"line": 5, "character": 0}, "end": {"line": 5, "character": 5}}}]}
 {"version": 2,

tests/lean/lcnfTypes.lean.expected.out

@@ -6,8 +6,8 @@ Eq.rec : {α : Sort u_1} → {a : α} → {motive : α → ◾ → Sort u} → m
 GetElem.getElem : {coll : Type u} →
   {idx : Type v} →
     {elem : Type w} → {valid : coll → idx → Prop} → [self : GetElem coll idx elem ◾] → coll → idx → ◾ → elem
-Term.constFold : {ctx : List Ty} → {ty : Ty} → Term ◾ ◾ → Term ◾ ◾
-Term.denote : {ctx : List Ty} → {ty : Ty} → Term ◾ ◾ → HList ◾ ◾ → ◾
+Term.constFold : {ctx : List Ty} → {ty : Ty} → _root_.Term ◾ ◾ → _root_.Term ◾ ◾
+Term.denote : {ctx : List Ty} → {ty : Ty} → _root_.Term ◾ ◾ → HList ◾ ◾ → ◾
 HList.get : {α : Type u_1} → {β : α → Type u_2} → {is : List α} → {i : α} → HList β ◾ → Member ◾ ◾ → β ◾
 Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member ◾ ◾
 Ty.denote : Ty → Type
@@ -15,32 +15,26 @@ MonadControl.liftWith : {m : Type u → Type v} →
   {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → (({β : Type u} → n β → m ◾) → m α) → n α
 MonadControl.restoreM : {m : Type u → Type v} → {n : Type u → Type w} → [self : MonadControl m n] → {α : Type u} → m ◾ → n α
 Decidable.casesOn : {p : Prop} → {motive : Decidable ◾ → Sort u} → Decidable ◾ → (◾ → motive ◾) → (◾ → motive ◾) → motive ◾
-Lean.getConstInfo : {m : Type → Type} →
-  [inst : Monad m] → [inst : Lean.MonadEnv m] → [inst : Lean.MonadError m] → Lean.Name → m Lean.ConstantInfo
+Lean.getConstInfo : {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstantInfo
 Lean.Meta.instMonadMetaM : Monad fun α =>
-  Lean.Meta.Context →
-    ST.Ref PUnit Lean.Meta.State →
-      Lean.Core.Context → ST.Ref PUnit Lean.Core.State → PUnit → EStateM.Result Lean.Exception PUnit α
-Lean.Meta.inferType : Lean.Expr →
-  Lean.Meta.Context →
-    ST.Ref PUnit Lean.Meta.State →
-      Lean.Core.Context → ST.Ref PUnit Lean.Core.State → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr
-Lean.Elab.Term.elabTerm : Lean.Syntax →
-  Option Lean.Expr →
+  Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit α
+Lean.Meta.inferType : Expr →
+  Context → ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr
+Lean.Elab.Term.elabTerm : Syntax →
+  Option Expr →
     Bool →
       Bool →
-        Lean.Elab.Term.Context →
-          ST.Ref PUnit Lean.Elab.Term.State →
-            Lean.Meta.Context →
-              ST.Ref PUnit Lean.Meta.State →
-                Lean.Core.Context → ST.Ref PUnit Lean.Core.State → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr
+        Elab.Term.Context →
+          ST.Ref PUnit Elab.Term.State →
+            Context →
+              ST.Ref PUnit State → Core.Context → ST.Ref PUnit Core.State → PUnit → EStateM.Result Exception PUnit Expr
 Nat.add : Nat → Nat → Nat
 Magma.mul : Magma → ◾ → ◾ → ◾
 weird1 : Bool → ◾
 lamAny₁ : Bool → Monad ◾
 lamAny₂ : Bool → Monad ◾
-Term.constFold : List Ty → Ty → Term lcErased lcErased → Term lcErased lcErased
-Term.denote : List Ty → Ty → Term lcErased lcErased → HList Ty lcErased lcErased → lcErased
+Term.constFold : List Ty → Ty → _root_.Term lcErased lcErased → _root_.Term lcErased lcErased
+Term.denote : List Ty → Ty → _root_.Term lcErased lcErased → HList Ty lcErased lcErased → lcErased
 HList.get : lcErased →
   lcErased → List lcErased → lcErased → HList lcErased lcErased lcErased → Member lcErased lcErased lcErased → lcErased
 Member.head : lcErased → lcErased → List lcErased → Member lcErased lcErased lcErased
@@ -49,18 +43,15 @@ MonadControl.liftWith : lcErased →
   lcErased → MonadControl lcErased lcErased → lcErased → ((lcErased → lcErased → lcErased) → lcErased) → lcErased
 MonadControl.restoreM : lcErased → lcErased → MonadControl lcErased lcErased → lcErased → lcErased → lcErased
 Decidable.casesOn : lcErased → lcErased → Bool → (lcErased → lcErased) → (lcErased → lcErased) → lcErased
-Lean.getConstInfo : lcErased → Monad lcErased → Lean.MonadEnv lcErased → Lean.MonadError lcErased → Lean.Name → lcErased
+Lean.getConstInfo : lcErased → Monad lcErased → MonadEnv lcErased → MonadError lcErased → Name → lcErased
 Lean.Meta.instMonadMetaM : Monad lcErased
-Lean.Meta.inferType : Lean.Expr →
-  Lean.Meta.Context → lcErased → Lean.Core.Context → lcErased → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr
-Lean.Elab.Term.elabTerm : Lean.Syntax →
-  Option Lean.Expr →
+Lean.Meta.inferType : Expr → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr
+Lean.Elab.Term.elabTerm : Syntax →
+  Option Expr →
     Bool →
       Bool →
-        Lean.Elab.Term.Context →
-          lcErased →
-            Lean.Meta.Context →
-              lcErased → Lean.Core.Context → lcErased → PUnit → EStateM.Result Lean.Exception PUnit Lean.Expr
+        Elab.Term.Context →
+          lcErased → Context → lcErased → Core.Context → lcErased → PUnit → EStateM.Result Exception PUnit Expr
 Nat.add : Nat → Nat → Nat
 Fin.add : Nat → Nat → Nat → Nat
 Lean.HashSetBucket.update : lcErased → Array (List lcErased) → USize → List lcErased → lcErased → Array (List lcErased)

tests/lean/metaEvalInstMessage.lean.expected.out

@@ -1,7 +1,2 @@
-metaEvalInstMessage.lean:5:0-5:12: error: expression
-  double
-has type
+metaEvalInstMessage.lean:5:0-5:5: error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
   Nat → Nat
-but instance
-  Lean.MetaEval (Nat → Nat)
-failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

tests/lean/mkProjStx.lean.expected.out

@@ -1,6 +1,3 @@
 A.x (B.toA (C.toB c))
-
 B.y (C.toB c)
-
 C.z c
-

tests/lean/moduleOf.lean.expected.out

@@ -4,4 +4,4 @@
 (some Lean.Data.HashMap)
 none
 none
-moduleOf.lean:16:0-16:9: error: unknown constant 'foo'
+moduleOf.lean:16:0-16:5: error: unknown constant 'foo'

tests/lean/partialIssue.lean.expected.out

@@ -1,2 +1 @@
-
 partialIssue.lean:12:8-12:19: error: (kernel) invalid declaration, safe declaration must not contain partial declaration 'False_intro'

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -6,5 +6,3 @@ has type
   @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type
 but is expected to have type
   @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type
-phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).

tests/lean/promise.lean.expected.out

@@ -1,2 +0,0 @@
-
-

tests/lean/prvCtor.lean.expected.out

@@ -1,8 +1,5 @@
 a : Nat
-
 prvCtor.lean:25:23-25:61: error: invalid {...} notation, constructor for `Lean.Environment` is marked as private
-prvCtor.lean:23:0-25:61: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 prvCtor.lean:27:7-27:8: error: unknown identifier 'a'
 prvCtor.lean:29:25-29:27: error: overloaded, errors 
   failed to synthesize

tests/lean/run/1697.lean

@@ -3,9 +3,6 @@
 error: tactic 'decide' proved that the proposition
   False
 is false
----
-error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 -/
 #guard_msgs in
 #eval show Nat from False.elim (by decide)
@@ -13,8 +10,10 @@ Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 /--
 warning: declaration uses 'sorry'
 ---
-error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
+error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to
+runtime instability and crashes.
+
+To attempt to evaluate anyway despite the risks, use the '#eval!' command.
 -/
 #guard_msgs in
 #eval #[1,2,3][2]'sorry

tests/lean/run/2291.lean

@@ -7,7 +7,107 @@ The following example would cause the pretty printer to panic.
 -/
 
 set_option trace.compiler.simp true in
-/-- info: [0] -/
+/--
+info: [compiler.simp] >> _eval
+let _x_21 := `Nat;
+let _x_22 := [];
+let _x_23 := Lean.Expr.const _x_21 _x_22;
+let _x_24 := `List.nil;
+let _x_25 := Lean.levelZero :: _x_22;
+let _x_26 := Lean.Expr.const _x_24 _x_25;
+let _x_27 := _x_26.app _x_23;
+let _x_28 := `List.cons;
+let _x_29 := Lean.Expr.const _x_28 _x_25;
+let _x_30 := _x_29.app _x_23;
+let _x_31 := [];
+let _x_32 := 0 :: _x_31;
+let _x_33 := Lean.List.toExprAux _x_27 _x_30 _x_32;
+Lean.MessageData.ofExpr _x_33
+[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
+fun nilFn consFn x =>
+  List.casesOn fun head tail =>
+    let _x_1 := Lean.mkNatLit head;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    Lean.mkAppB consFn _x_1 _x_2
+>> _eval
+let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
+let _x_15 := List.nil _neutral;
+let _x_16 := Lean.Expr.const._override _x_14 _x_15;
+let _x_17 := `List.nil;
+let _x_18 := List.cons _neutral Lean.levelZero _x_15;
+let _x_19 := Lean.Expr.const._override _x_17 _x_18;
+let _x_20 := Lean.Expr.app._override _x_19 _x_16;
+let _x_21 := `List.cons;
+let _x_22 := Lean.Expr.const._override _x_21 _x_18;
+let _x_23 := Lean.Expr.app._override _x_22 _x_16;
+let _x_24 := List.cons _neutral 0 _x_15;
+let _x_25 := Lean.List.toExprAux._at._eval._spec_1 _x_20 _x_23 _x_24;
+Lean.MessageData.ofExpr _x_25
+[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
+fun nilFn consFn x =>
+  List.casesOn fun head tail =>
+    let _x_1 := Lean.mkNatLit head;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    Lean.mkAppB consFn _x_1 _x_2
+>> _eval
+let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
+let _x_2 := List.nil _neutral;
+let _x_3 := Lean.Expr.const._override _x_1 _x_2;
+let _x_4 := `List.nil;
+let _x_5 := List.cons _neutral Lean.levelZero _x_2;
+let _x_6 := Lean.Expr.const._override _x_4 _x_5;
+let _x_7 := Lean.Expr.app._override _x_6 _x_3;
+let _x_8 := `List.cons;
+let _x_9 := Lean.Expr.const._override _x_8 _x_5;
+let _x_10 := Lean.Expr.app._override _x_9 _x_3;
+let _x_11 := List.cons _neutral 0 _x_2;
+let _x_12 := Lean.List.toExprAux._at._eval._spec_1 _x_7 _x_10 _x_11;
+Lean.MessageData.ofExpr _x_12
+[compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
+fun nilFn consFn x =>
+  List.casesOn fun head tail =>
+    let _x_1 := Lean.mkNatLit head;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    Lean.mkAppB consFn _x_1 _x_2
+>> _eval._closed_1
+"Nat"
+>> _eval._closed_2
+Lean.Name.str._override Lean.Name.anonymous._impl _eval._closed_1
+>> _eval._closed_3
+let _x_1 := List.nil _neutral;
+Lean.Expr.const._override _eval._closed_2 _x_1
+>> _eval._closed_4
+"List"
+>> _eval._closed_5
+"nil"
+>> _eval._closed_6
+Lean.Name.mkStr2 _eval._closed_4 _eval._closed_5
+>> _eval._closed_7
+let _x_1 := List.nil _neutral;
+List.cons _neutral Lean.levelZero _x_1
+>> _eval._closed_8
+Lean.Expr.const._override _eval._closed_6 _eval._closed_7
+>> _eval._closed_9
+Lean.Expr.app._override _eval._closed_8 _eval._closed_3
+>> _eval._closed_10
+"cons"
+>> _eval._closed_11
+Lean.Name.mkStr2 _eval._closed_4 _eval._closed_10
+>> _eval._closed_12
+Lean.Expr.const._override _eval._closed_11 _eval._closed_7
+>> _eval._closed_13
+Lean.Expr.app._override _eval._closed_12 _eval._closed_3
+>> _eval._closed_14
+let _x_1 := List.nil _neutral;
+List.cons _neutral 0 _x_1
+>> _eval
+let _x_1 :=
+  Lean.List.toExprAux._at._eval._spec_1 _eval._closed_9 _eval._closed_13
+    _eval._closed_14;
+Lean.MessageData.ofExpr _x_1
+---
+info: [0]
+-/
 #guard_msgs in
 #eval [0]
 

tests/lean/run/3713.lean

@@ -5,12 +5,7 @@ def somethingBad : MetaM Nat := do
   IO.println "oh no"
   return 1
 
-/--
-error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
----
-error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
--/
+/-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -/
 #guard_msgs in
 #eval show MetaM Unit from do
   let t := if false then ← somethingBad else 9
@@ -18,12 +13,7 @@ Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 def foo : MetaM Bool :=
   return false
 
-/--
-error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
----
-error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
--/
+/-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -/
 #guard_msgs in
 #eval show MetaM Unit from do
   let t := if (← foo) then ← somethingBad else 9

tests/lean/run/677.lean

@@ -5,7 +5,7 @@ def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
   let json := toJson x
   fromJson? json
 
-/-- info: Lean.Name.mkNum Lean.Name.anonymous 5 -/
+/-- info: Name.anonymous.num 5 -/
 #guard_msgs in
 #eval IO.ofExcept <| encodeDecode (Name.mkNum Name.anonymous 5)
 

tests/lean/run/DefEqAssignBug.lean

@@ -26,10 +26,8 @@ withLocalDeclD `x nat fun x => do
 
 set_option trace.Meta true
 
-/-- info: -/
 #guard_msgs in
 #eval tst1
 
-/-- info: -/
 #guard_msgs in
 #eval tst2

tests/lean/run/ExprLens.lean

@@ -79,7 +79,6 @@ def testTraversal
     if not (← liftM $ isDefEq e e') then
       throwError "\n{e} \nand \n{e'} are different!"
 
-/-- info: -/
 #guard_msgs in
 #eval ((do
   testTraversal traverseLambdaWithPos 1

tests/lean/run/IO_test.lean

@@ -32,7 +32,6 @@ withFile "foo.txt" Mode.read fun h => do
     check_eq "5" [] ys.toList
 pure ()
 
-/-- info: -/
 #guard_msgs in
 #eval test
 
@@ -135,6 +134,5 @@ check_eq "1" [] ys.toList
 let ys ← withFile fn4 Mode.read $ fun h => h.read 1;
 check_eq "2" [] ys.toList
 
-/-- info: -/
 #guard_msgs in
 #eval test4

tests/lean/run/array1.lean

@@ -62,7 +62,8 @@ info: 1
 2
 3
 4
-[12, 14]
+---
+info: [12, 14]
 -/
 #guard_msgs in
 #eval tst

tests/lean/run/catchThe.lean

@@ -21,7 +21,6 @@ def g1 : M Nat :=
     (tryCatchThe String act1 (fun ex => pure 100))
     (fun ex => pure 200)
 
-/-- info: -/
 #guard_msgs in
 #eval testM g1 200
 
@@ -33,7 +32,6 @@ tryCatchThe Exception
   (tryCatchThe String act2 (fun ex => pure 100))
   (fun ex => pure 200)
 
-/-- info: -/
 #guard_msgs in
 #eval testM g2 100
 

tests/lean/run/core.lean

@@ -15,7 +15,8 @@ pure 10;
 /--
 info: ([mdata borrowed:1 Nat]) -> ([mdata borrowed:1 Nat]) -> Nat
 testing...
-10
+---
+info: 10
 -/
 #guard_msgs in
 #eval f
@@ -25,8 +26,10 @@ set_option trace.Elab true
 /--
 info: ([mdata borrowed:1 Nat]) -> ([mdata borrowed:1 Nat]) -> Nat
 testing...
-[Elab] trace message
-10
+---
+info: 10
+---
+info: [Elab] trace message
 -/
 #guard_msgs in
 #eval f

tests/lean/run/csimpAttrFn.lean

@@ -3,14 +3,11 @@ import Lean
 open Lean
 open Lean.Compiler
 
-/-- info: -/
 #guard_msgs in
 #eval (do assert! hasCSimpAttribute (← getEnv) ``List.map_eq_mapTR : MetaM Unit)
 
-/-- info: -/
 #guard_msgs in
 #eval (do assert! hasCSimpAttribute (← getEnv) ``List.append_eq_appendTR : MetaM Unit)
 
-/-- info: -/
 #guard_msgs in
 #eval (do assert! !hasCSimpAttribute (← getEnv) ``List.append : MetaM Unit)

tests/lean/run/doElemAsTermNotation.lean

@@ -6,7 +6,6 @@ def f1 (x : Nat) : IO Unit :=
 #guard_msgs in
 #eval f1 0
 
-/-- info: -/
 #guard_msgs in
 #eval f1 100
 
@@ -28,7 +27,8 @@ def f3 (x : Nat) : IO Nat :=
 /--
 info: 5
 at catch: failed
-0
+---
+info: 0
 -/
 #guard_msgs in
 #eval f3 5

tests/lean/run/doLetElse.lean

@@ -10,7 +10,6 @@ def testFoo (input : Option Nat) (expected : Nat) : IO Unit := do
 #guard_msgs in
 #eval testFoo (some 10) 10
 
-/-- info: -/
 #guard_msgs in
 #eval testFoo none 0
 
@@ -27,14 +26,11 @@ def bar (x : Nat) : IO (Fin (x + 1)) := do
 def testBar (x : Nat) (expected : Fin (x + 1)) : IO Unit := do
   assert! (← bar x) == expected
 
-/-- info: -/
 #guard_msgs in
 #eval testBar 1 0
 
-/-- info: -/
 #guard_msgs in
 #eval testBar 2 1
 
-/-- info: -/
 #guard_msgs in
 #eval testBar 3 0

tests/lean/run/doNotation1.lean

@@ -121,7 +121,8 @@ else
 
 /--
 info: first field is zero
-((), 0, 2)
+---
+info: ((), 0, 2)
 -/
 #guard_msgs in
 #eval tst7.run (0, 2)

tests/lean/run/doNotation2.lean

@@ -22,7 +22,8 @@ aux started
 y: 10, z: 10
 aux started
 y: 10, z: 10
-20
+---
+info: 20
 -/
 #guard_msgs in
 #eval f 10
@@ -36,14 +37,16 @@ return xs.length
 
 /--
 info: >>> xs: [1, 2, 3]
-3
+---
+info: 3
 -/
 #guard_msgs in
 #eval g [1, 2, 3] |>.run' 10
 
 /--
 info: >>> xs: [10]
-1
+---
+info: 1
 -/
 #guard_msgs in
 #eval g [] |>.run' 10
@@ -86,7 +89,8 @@ return sum
 info: >> x: 1
 >> x: 3
 >> x: 5
-16
+---
+info: 16
 -/
 #guard_msgs in
 #eval sumOdd [1, 2, 3, 4, 5, 6, 7, 9, 11, 101] 10
@@ -193,7 +197,8 @@ def f5 (x y : Nat) : Nat × Nat := Id.run <| do
 
 /--
 info: z: 4
-(11, 6)
+---
+info: (11, 6)
 -/
 #guard_msgs in
 #eval f5 5 6

tests/lean/run/doNotation5.lean

@@ -24,14 +24,16 @@ catch ex : Nat =>
 
 /--
 info: nat exception 1010
-(Except.ok (Except.ok 1010), 1000)
+---
+info: (Except.ok (Except.ok 1010), 1000)
 -/
 #guard_msgs in
 #eval (f 10 20).run 1000
 
 /--
 info: string exception balance is zero
-(Except.ok (Except.ok 1000), 20)
+---
+info: (Except.ok (Except.ok 1000), 20)
 -/
 #guard_msgs in
 #eval (f 10 200).run 10

tests/lean/run/doNotation6.lean

@@ -80,7 +80,8 @@ return sum
 info: 1
 2
 3
-6
+---
+info: 6
 -/
 #guard_msgs in
 #eval f4 #[1, 2, 3]
@@ -97,7 +98,8 @@ info: 2
 3
 4
 5
-14
+---
+info: 14
 -/
 #guard_msgs in
 #eval f5 #[1, 2, 3, 4, 5, 6]

tests/lean/run/eval.lean

@@ -0,0 +1,179 @@
+import Lean
+/-!
+# Tests of the `#eval` command
+-/
+
+set_option eval.type true
+
+/-!
+Basic values
+-/
+/-- info: 2 : Nat -/
+#guard_msgs in #eval 2
+/-- info: some 2 : Option Nat -/
+#guard_msgs in #eval some 2
+/-- info: [2, 3, 4] : List Nat -/
+#guard_msgs in #eval [1,2,3].map (· + 1)
+
+/-!
+Deciding a proposition
+-/
+/-- info: true : Bool -/
+#guard_msgs in #eval True
+
+/-!
+Can't evaluate proofs
+-/
+/-- error: cannot evaluate, proofs are not computationally relevant -/
+#guard_msgs in #eval trivial
+
+/-!
+Can't evaluate types
+-/
+/-- error: cannot evaluate, types are not computationally relevant -/
+#guard_msgs in #eval Nat
+
+
+/-!
+Capturing `dbg_trace` output
+-/
+def Nat.choose : Nat → Nat → Nat
+  | _, 0 => dbg_trace "(_, 0)"; 1
+  | 0, _ + 1 => dbg_trace "(0, _ + 1)"; 0
+  | n + 1, k + 1 => dbg_trace "(_ + 1, _ + 1)"; choose n k + choose n (k + 1)
+/--
+info: (_ + 1, _ + 1)
+(_ + 1, _ + 1)
+(_, 0)
+(0, _ + 1)
+(_ + 1, _ + 1)
+(0, _ + 1)
+(0, _ + 1)
+---
+info: 1 : Nat
+-/
+#guard_msgs in #eval Nat.choose 2 2
+
+/-!
+Custom monad
+-/
+
+abbrev MyMonad := ReaderT Nat IO
+/--
+error: unable to synthesize 'MonadEval' instance to adapt
+  MyMonad Nat
+to 'IO' or 'Lean.Elab.Command.CommandElabM'.
+-/
+#guard_msgs in #eval (pure 2 : MyMonad Nat)
+
+-- Note that there is no "this is due to..." diagonostic in this case.
+/--
+error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
+  MyMonad (Nat → Nat)
+-/
+#guard_msgs in #eval (pure id : MyMonad (Nat → _))
+
+instance : MonadEval MyMonad IO where
+  monadEval m := m.run 0
+
+/-- info: 2 : Nat -/
+#guard_msgs in #eval (pure 2 : MyMonad Nat)
+
+-- Note that now we have a MonadEval instance, it doesn't mention MyMonad in the error.
+/--
+error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
+  Nat → Nat
+-/
+#guard_msgs in #eval (pure id : MyMonad (Nat → _))
+
+/-!
+Elaboration error, does not attempt to evaluate.
+-/
+/-- error: unknown identifier 'x' -/
+#guard_msgs in #eval 2 + x
+
+/-!
+Defaulting to the CommandElabM monad
+-/
+/-- info: 2 : Nat -/
+#guard_msgs in #eval do pure 2
+/-- info: true : Bool -/
+#guard_msgs in #eval do return (← Lean.getEnv).contains ``Lean.MessageData
+
+/-!
+Defaulting does not affect postponed elaborators.
+-/
+/-- info: 1 : Nat -/
+#guard_msgs in #eval if True then 1 else 2
+
+/-!
+Testing that dbg_trace and logs carry over from all the major meta monads.
+-/
+/--
+info: hi
+---
+info: dbg
+-/
+#guard_msgs in #eval show Lean.Elab.Term.TermElabM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi"
+/--
+info: hi
+---
+info: dbg
+-/
+#guard_msgs in #eval show Lean.MetaM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi"
+/--
+info: hi
+---
+info: dbg
+-/
+#guard_msgs in #eval show Lean.CoreM Unit from do dbg_trace "dbg"; Lean.logInfo m!"hi"
+
+/-!
+Testing delta deriving
+-/
+def Foo := List Nat
+def Foo.mk (l : List Nat) : Foo := l
+
+/-- info: [1, 2, 3] : Foo -/
+#guard_msgs in #eval Foo.mk [1,2,3]
+
+/-- info: [1, 2, 3] : Foo -/
+#guard_msgs in #eval do return Foo.mk [1,2,3]
+
+/-!
+Testing auto-deriving
+-/
+
+inductive Baz
+  | a | b
+
+/-- info: Baz.a : Baz -/
+#guard_msgs in #eval Baz.a
+
+/-!
+Returning after printing
+-/
+def returns : Lean.CoreM Nat := do
+  IO.println "hi"
+  return 2
+
+/--
+info: hi
+---
+info: 2 : Nat
+-/
+#guard_msgs in #eval returns
+
+/-!
+Throwing an exception after printing
+-/
+def throwsEx : Lean.CoreM Nat := do
+  IO.println "hi"
+  throwError "ex"
+
+/--
+info: hi
+---
+error: ex
+-/
+#guard_msgs in #eval throwsEx

tests/lean/run/expr1.lean

@@ -74,7 +74,6 @@ do let f   := mkConst `f [];
    unless (!t2.hasLooseBVar 1) do throw $ IO.userError "failed-6";
    pure ()
 
-/-- info: -/
 #guard_msgs in
 #eval tst4
 

tests/lean/run/finally.lean

@@ -23,7 +23,8 @@ match r with
 
 /--
 info: finisher executed
-Except.ok 100
+---
+info: Except.ok 100
 -/
 #guard_msgs in
 #eval (tst1.run).run' 0
@@ -39,7 +40,8 @@ tryCatchThe IO.Error
 
 /--
 info: finisher executed
-Except.ok 100
+---
+info: Except.ok 100
 -/
 #guard_msgs in
 #eval (tst2.run).run' 0
@@ -58,7 +60,8 @@ tryCatchThe IO.Error
 /--
 info: inner finisher executed
 outer finisher executed
-Except.ok 101
+---
+info: Except.ok 101
 -/
 #guard_msgs in
 #eval (tst3.run).run' 0
@@ -80,7 +83,8 @@ pure (a + s)
 /--
 info: inner finisher executed
 outer finisher executed
-Except.ok 143
+---
+info: Except.ok 143
 -/
 #guard_msgs in
 #eval (tst4.run).run' 0
@@ -98,7 +102,8 @@ pure a
 
 /--
 info: finalizer received: (some 42)
-Except.ok 42
+---
+info: Except.ok 42
 -/
 #guard_msgs in
 #eval (tst5.run).run' 0

tests/lean/run/float_from_bignum.lean

@@ -9,6 +9,5 @@ def tst1 : IO Unit := do
   check (Nat.toFloat (10^80) > Nat.toFloat (10^40));
   pure ()
 
-/-- info: -/
 #guard_msgs in
 #eval tst1

tests/lean/run/forInPArray.lean

@@ -19,7 +19,8 @@ return sum
 info: x: 2
 x: 4
 x: 10
-16
+---
+info: 16
 -/
 #guard_msgs in
 #eval f1 [1, 2, 3, 4, 5, 10, 20].toPArray' 10

tests/lean/run/getline_crash.lean

@@ -146,18 +146,14 @@ aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
 #guard_msgs in
 #eval tstGetLine ("".pushn 'a' 128)
 
-/-- info: -/
 #guard_msgs in
 #eval tstGetLine2 ("".pushn 'α' 20) ("".pushn 'β' 20)
 
-/-- info: -/
 #guard_msgs in
 #eval tstGetLine2 ("".pushn 'α' 40) ("".pushn 'β' 40)
 
-/-- info: -/
 #guard_msgs in
 #eval tstGetLine2 ("".pushn 'a' 61) ("".pushn 'b' 61)
 
-/-- info: -/
 #guard_msgs in
 #eval tstGetLine2 ("".pushn 'a' 61) ("".pushn 'b' 62)

tests/lean/run/handleLocking.lean

@@ -17,7 +17,6 @@ def test1 : IO Unit := do
   unless (← h2.tryLock) do
     throw <| IO.userError "failed to unlock exclusive lock and then lock"
 
-/-- info: -/
 #guard_msgs in
 #eval test1
 
@@ -29,7 +28,6 @@ def test2 : IO Unit := do
   unless (← h.tryLock) do
     throw <| IO.userError "handle free failed to unlock"
 
-/-- info: -/
 #guard_msgs in
 #eval test2
 
@@ -47,6 +45,5 @@ def test3 : IO Unit := do
   unless (← h2.tryLock) do
     throw <| IO.userError "failed to unlock shared locks and then lock"
 
-/-- info: -/
 #guard_msgs in
 #eval test3

tests/lean/run/kernelInterrupt.lean

@@ -7,7 +7,6 @@ In particular, runtime exceptions such as `interrupted_exception` should properl
  -/
 
 open Lean
-/-- info: -/
 #guard_msgs in
 #eval show CoreM _ from do
   let env ← getEnv

tests/lean/run/match1.lean

@@ -23,7 +23,6 @@ xs.map fun
   | 0 => true
   | _ => false
 
-/-- info: -/
 #guard_msgs in
 #eval checkWithMkMatcherInput ``f.match_1
 

tests/lean/run/meta2.lean

@@ -2,6 +2,8 @@ import Lean.Meta
 open Lean
 open Lean.Meta
 
+set_option pp.mvars false
+
 -- set_option trace.Meta true
 --set_option trace.Meta.isDefEq.step false
 -- set_option trace.Meta.isDefEq.delta false
@@ -181,7 +183,11 @@ do print "----- tst7 -----";
      checkM $ pure $ v == x;
      pure ()
 
-/-- info: [Meta.debug] ----- tst7 ----- -/
+/--
+error: check failed
+---
+info: [Meta.debug] ----- tst7 -----
+-/
 #guard_msgs in
 #eval tst7
 
@@ -591,9 +597,9 @@ withLocalDeclD `x nat $ fun x => do
 
 /--
 info: [Meta.debug] ----- tst30 -----
-[Meta.debug] (?m.2 x).succ
-[Meta.debug] ?m.4.succ
-[Meta.debug] fun x => ?m.4
+[Meta.debug] (?_ x).succ
+[Meta.debug] ?_.succ
+[Meta.debug] fun x => ?_
 -/
 #guard_msgs in
 #eval tst30
@@ -670,7 +676,7 @@ withLocalDeclD `α type $ fun α => do
 
 /--
 info: [Meta.debug] ----- tst34 -----
-[Meta.debug] fun α => ?m.3 α → ?m.3 α
+[Meta.debug] fun α => ?_ α → ?_ α
 -/
 #guard_msgs in
 #eval tst34
@@ -694,7 +700,7 @@ withLocalDeclD `α type $ fun α => do
 
 /--
 info: [Meta.debug] ----- tst35 -----
-[Meta.debug] fun α => ?m.4 α → ?m.4 α
+[Meta.debug] fun α => ?_ α → ?_ α
 [Meta.debug] fun α => α → α
 -/
 #guard_msgs in
@@ -730,7 +736,7 @@ withLocalDeclD `v nat $ fun v => do
 
 /--
 info: [Meta.debug] ----- tst37 -----
-[Meta.debug] ?m.1 v (?m.2 v)
+[Meta.debug] ?_ v (?_ v)
 [Meta.debug] StateM Nat Nat
 -/
 #guard_msgs in

tests/lean/run/meta5.lean

@@ -19,19 +19,20 @@ withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
     trace[Meta.debug] m!"?{mvarId.name} : {mvarDecl.type}"
 }
 
+set_option pp.mvars false
 set_option trace.Meta.debug true
 
 /--
-info: [Meta.debug] ?m.3
+info: [Meta.debug] ?_
 [Meta.debug] x.add y
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.4 : Nat →
+[Meta.debug] ?_uniq.3014 : Nat
+[Meta.debug] ?_uniq.3015 : Nat →
       Nat →
         let x := 0;
         Nat
-[Meta.debug] ?_uniq.3 : Nat
 -/
 #guard_msgs in
 #eval tst1

tests/lean/run/meta7.lean

@@ -259,7 +259,6 @@ def tst10 : MetaM Unit := do
   assert! (← getConstInfoInduct `Foo).isNested
   assert! !(← getConstInfoInduct `Prod).isNested
 
-/-- info: -/
 #guard_msgs in
 #eval tst10
 

tests/lean/run/monadControl.lean

@@ -20,7 +20,8 @@ pure a
 info: started
 hello
 ended
-((Except.error "ERROR", "world"), 1011)
+---
+info: ((Except.error "ERROR", "world"), 1011)
 -/
 #guard_msgs in
 #eval (((tst.run true).run "world").run 1000).run 11
@@ -44,7 +45,8 @@ pure a
 info: started
 hello
 ended
-((Except.ok (1015, true), "world"), 1016)
+---
+info: ((Except.ok (1015, true), "world"), 1016)
 -/
 #guard_msgs in
 #eval (((tst2.run true).run "world").run 1000).run 10

tests/lean/run/nicerNestedDos.lean

@@ -7,7 +7,8 @@ def f (x : Nat) : IO Nat := do
 
 /--
 info: hello
-3
+---
+info: 3
 -/
 #guard_msgs in
 #eval f 2
@@ -16,7 +17,8 @@ info: hello
 info: hello
 x: 10
 done
-11
+---
+info: 11
 -/
 #guard_msgs in
 #eval f 10

tests/lean/run/ptrAddr.lean

@@ -14,7 +14,8 @@ def y := x
 
 /--
 info: >> (1, 2) == (1, 2)
-true
+---
+info: true
 -/
 #guard_msgs in
 #eval withPtrEq x (mk 1) (fun _ => dbgTrace (">> " ++ toString x ++ " == " ++ toString y) $ fun _ => x == y) TrustMe -- should print message

tests/lean/run/readerThe.lean

@@ -14,7 +14,8 @@ pure s
 /--
 info: hello
 true
-10
+---
+info: 10
 -/
 #guard_msgs in
 #eval (f "hello").run' 10 true
@@ -26,7 +27,8 @@ withReader (fun s => s ++ " world") a
 /--
 info: hello world
 false
-10
+---
+info: 10
 -/
 #guard_msgs in
 #eval (g "hello").run' 10 true

tests/lean/run/returnOptIssue.lean

@@ -4,6 +4,5 @@ if x > 10 then
   return
 throw $ IO.userError "x ≤ 10"
 
-/-- info: -/
 #guard_msgs in
 #eval f 11

tests/lean/run/stateRef.lean

@@ -8,14 +8,16 @@ f 5 |>.run' 20
 
 /--
 info: hello
-15
+---
+info: 15
 -/
 #guard_msgs in
 #eval (f 5).run' 20
 
 /--
 info: hello
-95
+---
+info: 95
 -/
 #guard_msgs in
 #eval (do set 100; f 5 : StateRefT Nat IO Nat).run' 0
@@ -27,7 +29,8 @@ get
 
 /--
 info: context 10
-30
+---
+info: 30
 -/
 #guard_msgs in
 #eval (f2.run 10).run' 20
@@ -43,7 +46,8 @@ getThe Nat
 
 /--
 info: test, 10
-11
+---
+info: 11
 -/
 #guard_msgs in
 #eval (f3.run' "test").run' 10
@@ -74,7 +78,8 @@ pure (a0 + a1 + a2)
 info: state0 10
 state1 20
 state1 30
-60
+---
+info: 60
 -/
 #guard_msgs in
 #eval f4.run' ⟨10⟩ |>.run' ⟨20⟩ |>.run' ⟨30⟩

tests/lean/run/task_test.lean

@@ -23,7 +23,8 @@ pure 0
 
 /--
 info: 12 11
-0
+---
+info: 0
 -/
 #guard_msgs in
 #eval tst 10

tests/lean/run/task_test2.lean

@@ -15,7 +15,8 @@ pure 0
 
 /--
 info: >> [100, 100, 100, 100, 100, 100, 100, 100, 100, 100]
-0
+---
+info: 0
 -/
 #guard_msgs in
 #eval tst 10

tests/lean/run/termElab.lean

@@ -29,6 +29,5 @@ let e ← elabTermAndSynthesize stx none;
 trace[Elab.debug] m!">>> {e}";
 throwErrorIfErrors
 
-/-- info: -/
 #guard_msgs in
 #eval tst2

tests/lean/run/trace.lean

@@ -59,7 +59,8 @@ info: [module] message
                world
   [bughunt] at test2
 ERROR
-[module] message
+---
+info: [module] message
   [module] hello
                world
   [bughunt] at test2
@@ -76,11 +77,13 @@ info: [module] message
 [module] hello
              world
 [bughunt] at end of tst3
-[module] message
+---
+info: [module] message
   [module] hello
                world
   [bughunt] at test2
-  [module] hello world
+  [module] hello
+               world
 [module] hello
              world
 [bughunt] at end of tst3

tests/lean/run_meta1.lean.expected.out

@@ -1 +1 @@
-run_meta1.lean:1:0-1:19: error: to use this command, include `import Lean.Elab.Command`
+run_meta1.lean:1:0-1:19: error: to use this command, include `import Lean.Meta.Basic`

tests/lean/scientific.lean.expected.out

@@ -15,8 +15,6 @@ scientific.lean:15:7-15:12: error: unexpected token; expected command
 scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
 scientific.lean:16:7-16:16: error: unexpected token; expected command
 scientific.lean:19:6-19:7: error: unknown identifier 'e'
-scientific.lean:19:0-19:9: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 scientific.lean:20:9: error: missing exponent digits in scientific literal
 scientific.lean:21:9: error: missing exponent digits in scientific literal
 scientific.lean:22:9: error: missing exponent digits in scientific literal
@@ -25,9 +23,5 @@ scientific.lean:24:9: error: missing exponent digits in scientific literal
 scientific.lean:25:9: error: missing exponent digits in scientific literal
 scientific.lean:26:6-26:8: error: invalid dotted identifier notation, unknown identifier `Nat.E` from expected type
   Nat
-scientific.lean:26:0-26:11: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 scientific.lean:27:7-27:9: error: unknown identifier 'E3'
-scientific.lean:27:0-27:9: error: cannot evaluate expression that depends on the `sorry` axiom.
-Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
 scientific.lean:28:7: error: missing exponent digits in scientific literal

tests/lean/updateExprIssue.lean.expected.out

@@ -1,5 +1,4 @@
 
-
 [init]
 def sefFn (x_1 : obj) (x_2 : obj) : obj :=
   case x_1 : obj of