From ee699518fa6855cc179f6cc040de8c9a7bf3b84c Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 20 Aug 2025 10:49:09 -0700
Subject: [PATCH] fix: have `#eval` save the info context (#10008)

This PR fixes a bug in `#eval` where clicking on the evaluated
expression could show errors in the Infoview. This was caused by `#eval`
not saving the temporary environment that is used when elaborating the
expression.
---
 src/Lean/Elab/BuiltinEvalCommand.lean         | 19 ++++++++++---------
 tests/lean/interactive/hover.lean             |  7 +++++++
 .../lean/interactive/hover.lean.expected.out  |  6 ++++++
 3 files changed, 23 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index 7b872f3e1e..fccc983b29 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/src/Lean/Elab/BuiltinEvalCommand.lean
@@ -217,15 +217,16 @@ unsafe def elabEvalCoreUnsafe (bang : Bool) (tk term : Syntax) (expectedType? :
       -- 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
+        withSaveInfoContext do -- save the environment post-elaboration (for matchers, let rec, etc.)
+          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 =>
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index f4bc790070..393b13c0a0 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -299,3 +299,10 @@ open List renaming zip → zip'
                  --^ textDocument/hover
 
 end Foo
+
+/-!
+`#eval` needs to save info context for this hover to give the inferred type,
+since it needs the environment with the generated `_eval.match_1` matcher.
+-/
+#eval (default : Nat) matches .succ ..
+                      --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 27158cd6ee..dd62516d2f 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -650,3 +650,9 @@
  {"value":
   "```lean\nList.zip.{u, v} {α : Type u} {β : Type v} : List α → List β → List (α × β)\n```\n***\nCombines two lists into a list of pairs in which the first and second components are the\ncorresponding elements of each list. The resulting list is the length of the shorter of the input\nlists.\n\n`O(min |xs| |ys|)`.\n\nExamples:\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2, 3] = [(\"Mon\", 1), (\"Tue\", 2), (\"Wed\", 3)]`\n* `[\"Mon\", \"Tue\", \"Wed\"].zip [1, 2] = [(\"Mon\", 1), (\"Tue\", 2)]`\n* `[x₁, x₂, x₃].zip [y₁, y₂, y₃, y₄] = [(x₁, y₁), (x₂, y₂), (x₃, y₃)]`\n\n***\n*import Init.Data.List.Basic*",
   "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 306, "character": 24}}
+{"range":
+ {"start": {"line": 306, "character": 6},
+  "end": {"line": 306, "character": 38}},
+ "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}