repl messages

Stream: lean4

[Utensil Song]

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

% 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.

Filed as leanprover-community/repl#40 . @Kim Morrison Sorry for cross-posting and the ping, is this output expected, and is there a way I can extract only the messages for the last output?

[Kim Morrison]

No, this is definitely a bug!

[Utensil Song]

Yeah, maybe running repl in batch mode during dataset extraction would not discover it, but I'm doing this interactively.

[Utensil Song]

I may be able to create a PR for this with some pointers if you are busy.

[Utensil Song]

I'm looking into this more deeply. I was trying to see if I can do the same filtering as proof states, it turns out they are also not filtered.

To see this clearly,

image.png

[Utensil Song]

How repl works is to treat the previous inputs as a commandState, process the current input into a parserState, then feed them into IO.processCommands which passed on to Frontend.processCommands to process them as a whole, and all messages, all sorries etc. are returned.

From Lean/Server/README.md:

Once a relevant Snapshot snap has been located, snap.infoTree.smallestInfo? and other functions from Lean.Server.InfoUtils can be used to further locate information about a document position.

Maybe I could give this a try.

[Kim Morrison]

I'm sure this is going to a single-line bug somewhere. Sorry I haven't had a chance to look at it. It is something about how we filter the logs to remove earlier stuff.

[Utensil Song]

Indeed, in processCommandsWithInfoTrees when retrieving the messages and the trees from the returned state, we have the opportunity to deduplicate it with the initial command state.

[Kim Morrison]

I think this already happens later in the code: it's a bug, with the code that exists to do this already not working, rather than an oversight (I think! Certainly for log messages the code tries to remove old messages.)

[Utensil Song]

I fixed it in processCommandsWithInfoTrees and tests show the fix works, will submit a PR for reference after I tidy it up.

Code after that only has a chance to do so in runCommand, it's the last place where the code has access to the initial command state, but all those code (just <20 lines) didn't try to do it. Even later would be repl and main which contain much less code and clearly serves other purposes.

Probably there was once some code that did this, but there seem to be no such non-working code left in the codebase.

[Kim Morrison]

Okay, thanks! I will try make time to review it.

[Utensil Song]

leanprover-community/repl#41 , PRed with 2 new tests, 1 updated test. Will polish the code later. :swim:

[Utensil Song]

I have simplified the code, it's now only ~3 lines, and ready for review.