unknown metavariable in infoview

Stream: lean4

[Jovan Gerbscheid]

In this example when the cursor is on α or the mouse hovers over it, it throws an error about an unknown metavariable:

def oops (i : ∀ α, List α) : List β := i β

[Kyle Miller]

Are you seeing this error in the infoview (like in this thread's title)? I can't reproduce that, but I do see "α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)" when hovering over α in the source.

[Henrik Böving]

https://github.com/leanprover/lean4/issues/4078 sounds like a variant of this one

[Henrik Böving]

Kyle Miller said:

Are you seeing this error in the infoview (like in this thread's title)? I can't reproduce that, but I do see "α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)" when hovering over α in the source.

see what I wrote in the issue about the dual error

[Henrik Böving]

@Jovan Gerbscheid could you comment your example on that issue? Its a much cleaner minimization than the one I provided so it will hopefully make it easier to debug things

[Jovan Gerbscheid]

Kyle Miller said:

Are you seeing this error in the infoview (like in this thread's title)? I can't reproduce that, but I do see "α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)" when hovering over α in the source.

Yes, as described in the issue, there is an error in the infoview when the cursor is on the relevant expression, and the error you see when hovering.

[Joachim Breitner]

I idly had a look and may have fixed it, without knowing too much about what I am doing here. I hope I didn't duplicate any work here.

[Kyle Miller]

when the cursor is on the relevant expression

I see, I didn't observe this Infoview error because I put my mouse cursor on the relevant expression, but I didn't move the editor's text cursor there.

[Kyle Miller]

This should now be fixed in lean4#4192