search

leanprover-community / repl

A simple REPL for Lean 4, returning information about errors and sorries.
69 stars 16 forks source link

Messages accumulate with wrong positions #40

Closed utensil closed 4 months ago

utensil commented 4 months ago

When given multiple inputs that have messages in outputs, it seems that repl will accumulate these messages for later outputs, particularly, these messages are marked with positions from previous inputs, causing confusing results.

2 minimal example input/output pairs of repl:

% repl
{"cmd": "def f := 2\n#check f", "env": null}

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data": "f : Nat"}],
 "env": 0}

{"cmd": "example : 1 = 2 := sorry", "env": 0}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 19},
   "goal": "⊢ 1 = 2",
   "endPos": {"line": 1, "column": 24}}],
 "messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data": "f : Nat"},
  {"severity": "warning",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 7},
   "data": "declaration uses 'sorry'"}],
 "env": 1}

Note that, the 2nd command contains only 1 line, but there is a message marked with position on line 2 that is from the previous command.

It gets worse for more commands, and they are unlikely to be deduplicated from the user end, except maybe filtering out identical messages for the same line with different input line.

A visual example for more commands can be seen here:

image

where the arrows are pointing from the later output to the earlier output, both are reported in wrong positions for the later output.

utensil commented 4 months ago

I can see the relevant code in Lean.Elab.IO.processInput didn't filter any message, but I could not find how the positions got wrong in repl code base, maybe it has a deeper origin.

utensil commented 4 months ago

More discussions are on Zulip.