fix: #eval command was leaking auxiliary declarations into the envi…

…ronment (#3323)

src/Lean/Elab/BuiltinCommand.lean

@@ -656,35 +656,40 @@ unsafe def elabEvalUnsafe : CommandElab
         return e
     -- Evaluate using term using `MetaEval` class.
     let elabMetaEval : CommandElabM Unit := do
-      -- act? is `some act` if elaborated `term` has type `CommandElabM α`
-      let act? ← runTermElabM fun _ => Term.withDeclName declName 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 <| some act
-        else
-          let e ← mkRunMetaEval e
-          let env ← getEnv
-          let opts ← getOptions
-          let act ← try addAndCompile e; evalConst (Environment → Options → IO (String × Except IO.Error Environment)) declName finally setEnv env
-          let (out, res) ← act env opts -- we execute `act` using the environment
-          logInfoAt tk out
-          match res with
-          | Except.error e => throwError e.toString
-          | Except.ok env  => do setEnv env; pure none
-      let some act := act? | return ()
-      act
+      -- Generate an action without executing it. We use `withoutModifyingEnv` to ensure
+      -- we don't polute 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
+            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
+    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)
-      let env ← getEnv
-      let act ← try addAndCompile e; evalConst (IO (String × Except IO.Error Unit)) declName finally setEnv env
+      addAndCompile e
+      let act ← evalConst (IO (String × Except IO.Error Unit)) declName
       let (out, res) ← liftM (m := IO) act
       logInfoAt tk out
       match res with

tests/lean/evalLeak.lean

@@ -0,0 +1,23 @@
+import Lean
+
+#eval match true with | true => false | false => true
+
+open Lean Elab Command Meta
+#eval show CommandElabM Unit from do
+  match ([] : List Nat) with
+  | []  =>
+    liftCoreM <| addDecl <| Declaration.defnDecl {
+      name        := `foo
+      type        := Lean.mkConst ``Bool
+      levelParams := []
+      value       := Lean.mkConst ``true
+      hints       := .opaque
+      safety      := .safe
+    }
+  | _ => return ()
+
+#check foo
+-- The auxiliary declarations created to elaborate the commands above
+-- should not leak into the environment
+#check _eval.match_1 -- Should fail
+#check _eval.match_2 -- Should fail

tests/lean/evalLeak.lean.expected.out

@@ -0,0 +1,4 @@
+false
+foo : Bool
+evalLeak.lean:22:7-22:20: error: unknown identifier '_eval.match_1'
+evalLeak.lean:23:7-23:20: error: unknown identifier '_eval.match_2'