From 41b35baea28bd5bb2ea771ee0ed7d7b54a887f6c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 18 Oct 2024 12:17:30 +0200
Subject: [PATCH] fix: duplicate info trees from
 `IO.processCommandsIncrementally` (#5763)

As reported in https://github.com/leanprover-community/repl/pull/57
---
 src/Lean/Elab/Frontend.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index b89ab0e74671..0a248a42a7d4 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext)
 where
   go initialSnap t commands :=
     let snap := t.get
-    let commands := commands.push snap.data.stx
+    let commands := commands.push snap.data
     if let some next := snap.nextCmdSnap? then
       go initialSnap next.task commands
     else
@@ -111,13 +111,15 @@ where
       let messages := toSnapshotTree initialSnap
         |>.getAll.map (·.diagnostics.msgLog)
         |>.foldl (· ++ ·) {}
-      let trees := toSnapshotTree initialSnap
-        |>.getAll.map (·.infoTree?) |>.filterMap id |>.toPArray'
+      -- In contrast to messages, we should collect info trees only from the top-level command
+      -- snapshots as they subsume any info trees reported incrementally by their children.
+      let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray'
       return {
         commandState := { snap.data.finishedSnap.get.cmdState with messages, infoState.trees := trees }
         parserState := snap.data.parserState
         cmdPos := snap.data.parserState.pos
-        inputCtx, initialSnap, commands
+        commands := commands.map (·.stx)
+        inputCtx, initialSnap
       }
 
 def IO.processCommands (inputCtx : Parser.InputContext) (parserState : Parser.ModuleParserState)