From 88a0643592d35d20a279e416e839a1f4184444a1 Mon Sep 17 00:00:00 2001
From: Utensil <utensilcandel@gmail.com>
Date: Thu, 23 May 2024 10:45:33 +0800
Subject: [PATCH] fix: duplicated and misaligned messages and info trees in
 output (#41)

* Reproduce #40

* Deduplicate messages and trees with the initial command state

* Update expected output after the fix

* Update expected output for variables.in, deduplicated

* Simplify
---
 REPL/Frontend.lean            |  5 ++++-
 test/dup_msg.expected.out     | 16 ++++++++++++++++
 test/dup_msg.in               |  5 +++++
 test/dup_sorries.expected.out | 24 ++++++++++++++++++++++++
 test/dup_sorries.in           |  3 +++
 test/variables.expected.out   |  5 -----
 6 files changed, 52 insertions(+), 6 deletions(-)
 create mode 100644 test/dup_msg.expected.out
 create mode 100644 test/dup_msg.in
 create mode 100644 test/dup_sorries.expected.out
 create mode 100644 test/dup_sorries.in

diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
index a70b07e..1ae5166 100644
--- a/REPL/Frontend.lean
+++ b/REPL/Frontend.lean
@@ -20,7 +20,10 @@ def processCommandsWithInfoTrees
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  pure (s, s.messages.msgs.toList, s.infoState.trees.toList)
+  let msgs := s.messages.msgs.toList.drop commandState.messages.msgs.size
+  let trees := s.infoState.trees.toList.drop commandState.infoState.trees.size
+
+  pure (s, msgs, trees)
 
 /--
 Process some text input, with or without an existing command state.
diff --git a/test/dup_msg.expected.out b/test/dup_msg.expected.out
new file mode 100644
index 0000000..9dab2fb
--- /dev/null
+++ b/test/dup_msg.expected.out
@@ -0,0 +1,16 @@
+{"env": 0}
+
+{"messages":
+ [{"severity": "info",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 6},
+   "data": "f : Nat"}],
+ "env": 1}
+
+{"messages":
+ [{"severity": "error",
+   "pos": {"line": 1, "column": 7},
+   "endPos": {"line": 1, "column": 8},
+   "data": "unknown identifier 'g'"}],
+ "env": 2}
+
diff --git a/test/dup_msg.in b/test/dup_msg.in
new file mode 100644
index 0000000..4d53f17
--- /dev/null
+++ b/test/dup_msg.in
@@ -0,0 +1,5 @@
+{"cmd": "def f := 2"}
+
+{"cmd": "#check f", "env": 0}
+
+{"cmd": "#check g", "env": 1}
diff --git a/test/dup_sorries.expected.out b/test/dup_sorries.expected.out
new file mode 100644
index 0000000..d01dd9b
--- /dev/null
+++ b/test/dup_sorries.expected.out
@@ -0,0 +1,24 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 24},
+   "goal": "⊢ 1 = 1",
+   "endPos": {"line": 1, "column": 29}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 12},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"sorries":
+ [{"proofState": 1,
+   "pos": {"line": 1, "column": 24},
+   "goal": "⊢ 2 = 2",
+   "endPos": {"line": 1, "column": 29}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 12},
+   "data": "declaration uses 'sorry'"}],
+ "env": 1}
+
diff --git a/test/dup_sorries.in b/test/dup_sorries.in
new file mode 100644
index 0000000..78c8e1d
--- /dev/null
+++ b/test/dup_sorries.in
@@ -0,0 +1,3 @@
+{"cmd": "theorem thm1 : 1 = 1 := sorry"}
+
+{"cmd": "theorem thm2 : 2 = 2 := sorry", "env": 0}
diff --git a/test/variables.expected.out b/test/variables.expected.out
index d6e4bdd..cd060cb 100644
--- a/test/variables.expected.out
+++ b/test/variables.expected.out
@@ -16,11 +16,6 @@
    "endPos": {"line": 3, "column": 7}}],
  "messages":
  [{"severity": "warning",
-   "pos": {"line": 1, "column": 12},
-   "endPos": {"line": 1, "column": 13},
-   "data":
-   "unused variable `y`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"},
-  {"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 15},
    "data": "declaration uses 'sorry'"}],