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
leanprover-community · May 23, 2024 · 88a0643 · 88a0643
1 parent 6d5b2c3
commit 88a0643
Show file tree

Hide file tree

Showing 6 changed files with 52 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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'"}],
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		{"cmd": "theorem thm1 : 1 = 1 := sorry"}

		{"cmd": "theorem thm2 : 2 = 2 := sorry", "env": 0}