From c6f8c741bd22ea300fcbece2d67a397b7842831c Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 9 Oct 2024 13:38:30 -0700
Subject: [PATCH 1/2] feat: support `let rec` in `#eval`

Makes `#eval` use the `elabMutualDef` machinery to process all the `let rec`s that might appear in the expression. This now works:
```lean
  let rec fact (n : Nat) : Nat :=
    match n with
    | 0 => 1
    | n' + 1 => n * fact n'
  fact 5
```

Closes #2374
---
 src/Lean/Elab/BuiltinEvalCommand.lean | 23 +++++++----------------
 tests/lean/run/eval.lean              | 16 ++++++++++++++++
 tests/lean/run/meta5.lean             |  4 ++--
 3 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index f5cb0179ba35..3e4620016b73 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/src/Lean/Elab/BuiltinEvalCommand.lean
@@ -4,11 +4,9 @@ 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
+import Lean.Elab.MutualDef
 
 /-!
 # Implementation of `#eval` command
@@ -81,19 +79,12 @@ where
     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
+  -- Use the `elabMutualDef` machinery to be able to support `let rec`.
+  -- Hack: since we are using the `TermElabM` version, we can insert the `value` as a metavariable via `exprToSyntax`.
+  let defView := mkDefViewOfDef { isUnsafe := true }
+    (← `(Parser.Command.definition|
+          def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
+  Term.elabMutualDef #[] { header := "" } #[defView]
   unless allowSorry do
     let axioms ← collectAxioms declName
     if axioms.contains ``sorryAx then
diff --git a/tests/lean/run/eval.lean b/tests/lean/run/eval.lean
index f098698cb6c5..3be84565e5ee 100644
--- a/tests/lean/run/eval.lean
+++ b/tests/lean/run/eval.lean
@@ -177,3 +177,19 @@ info: hi
 error: ex
 -/
 #guard_msgs in #eval throwsEx
+
+/-!
+Let rec support (issue #2374)
+-/
+/-- info: 37 : Nat -/
+#guard_msgs in #eval
+  let rec bar : Nat := 1
+  37
+
+/-- info: 120 : Nat -/
+#guard_msgs in #eval
+  let rec fact (n : Nat) : Nat :=
+    match n with
+    | 0 => 1
+    | n' + 1 => n * fact n'
+  fact 5
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
index f9f7dc391b94..66b48449d004 100644
--- a/tests/lean/run/meta5.lean
+++ b/tests/lean/run/meta5.lean
@@ -28,11 +28,11 @@ info: [Meta.debug] ?_
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.3014 : Nat
-[Meta.debug] ?_uniq.3015 : Nat →
+[Meta.debug] ?_uniq.3019 : Nat →
       Nat →
         let x := 0;
         Nat
+[Meta.debug] ?_uniq.3018 : Nat
 -/
 #guard_msgs in
 #eval tst1

From 517f1d2ac4910d97e81e6c425c02258c3dbaba1c Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 10 Oct 2024 22:49:40 -0700
Subject: [PATCH 2/2] mention experiment

---
 src/Lean/Elab/BuiltinEvalCommand.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index 3e4620016b73..3a11ed0fd81f 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/src/Lean/Elab/BuiltinEvalCommand.lean
@@ -81,6 +81,9 @@ where
 private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Unit := do
   -- Use the `elabMutualDef` machinery to be able to support `let rec`.
   -- Hack: since we are using the `TermElabM` version, we can insert the `value` as a metavariable via `exprToSyntax`.
+  -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
+  -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
+  -- such as "failed to infer definition type" can surface.
   let defView := mkDefViewOfDef { isUnsafe := true }
     (← `(Parser.Command.definition|
           def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))