From 7c0216595ef2ff7659793c8719478c9062924e53 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Sep 2020 12:44:25 -0700
Subject: [PATCH] fix: remove duplicate error messages due to `variable`(s)

In Lean4, we re-elaborate `variable`(s) for each command, but we don't
want the error messages due to `variable` to appear in the log
multiple times.
---
 src/Lean/Elab/Command.lean                   | 13 ++++++++++---
 src/Lean/Elab/Term.lean                      |  3 +++
 tests/lean/doSeqRightIssue.lean.expected.out |  1 -
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 30a620d02b..9d0199389c 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -220,17 +220,24 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
 ctx ← read;
 s   ← get;
 let scope := s.scopes.head!;
-let x : MetaM _      := (observing x).run (mkTermContext ctx s declName?) { messages := s.messages, nextMacroScope := s.nextMacroScope };
+-- We execute `x` with an empty message log. Thus, `x` cannot modify/view messages produced by previous commands.
+-- This is useful for implementing `runTermElabM` where we use `Term.resetMessageLog`
+let messages         := s.messages;
+let x : MetaM _      := (observing x).run (mkTermContext ctx s declName?) { messages := {}, nextMacroScope := s.nextMacroScope };
 let x : CoreM _      := x.run mkMetaContext {};
 let x : EIO _ _      := x.run (mkCoreContext ctx s) { env := s.env, ngen := s.ngen };
 (((ea, termS), _), coreS) ← liftEIO x;
-modify fun s => { s with env := coreS.env, messages := termS.messages, ngen := coreS.ngen };
+modify fun s => { s with env := coreS.env, messages := messages ++ termS.messages, ngen := coreS.ngen };
 match ea with
 | Except.ok a     => pure a
 | Except.error ex => throw ex
 
 @[inline] def runTermElabM {α} (declName? : Option Name) (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
-s ← get; liftTermElabM declName? (Term.elabBinders (getVarDecls s) elabFn)
+s ← get;
+liftTermElabM declName?
+  -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
+  -- So, we use `Term.resetMessageLog`.
+  (Term.elabBinders (getVarDecls s) (fun xs => do Term.resetMessageLog; elabFn xs))
 
 @[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
 catch x
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 3d1e282a1a..2f86a05329 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -169,6 +169,9 @@ set s.core; set s.meta; set s.elab
 abbrev TermElabResult := EStateM.Result Exception SavedState Expr
 instance TermElabResult.inhabited : Inhabited TermElabResult := ⟨EStateM.Result.ok (arbitrary _) (arbitrary _)⟩
 
+def resetMessageLog : TermElabM Unit := do
+modify fun s => { s with messages := {} }
+
 /--
   Execute `x`, save resulting expression and new state.
   If `x` fails, then it also stores exception and new state.
diff --git a/tests/lean/doSeqRightIssue.lean.expected.out b/tests/lean/doSeqRightIssue.lean.expected.out
index e9bd29f8bc..ec2ffaa064 100644
--- a/tests/lean/doSeqRightIssue.lean.expected.out
+++ b/tests/lean/doSeqRightIssue.lean.expected.out
@@ -1,2 +1 @@
 doSeqRightIssue.lean:5:24: error: unknown universe level v
-doSeqRightIssue.lean:5:24: error: unknown universe level v