go to definition failing for some people

Stream: general

[Kevin Buzzard]

I am teaching right now. For two students, clicking on "go to definition" (the little injective hook-arrow) in the infoview simply doesn't work. I have no idea how to debug. They're live streaming their screens. Is this a known issue?

[Mario Carneiro]

I haven't seen this before fwiw

[Bryan Gin-ge Chen]

Is there a #mwe?

[Alex J. Best]

Doesn't work for me at all, on windows, are they also on windows?

[Bryan Gin-ge Chen]

@Alex J. Best if you hit ctrl+shift+p and run "toggle developer tools", do you see any errors in the console when you try to go to definition in the widget infoview?

[Alex J. Best]

Trying it now :smile: as expected it seems to be some funny buisness with backslashes

console.ts:137 [Extension Host] rejected promise not handled within 1 second: Error: cannot open C:%5CUsers%5Calexj%5C.elan%5Ctoolchains%5Cleanprover-community-lean-3.26.0%5Clib%5Clean%5Clibrary%5Cinit%5Ccore.lean. Detail: Unable to resolve resource C:%5CUsers%5Calexj%5C.elan%5Ctoolchains%5Cleanprover-community-lean-3.26.0%5Clib%5Clean%5Clibrary%5Cinit%5Ccore.lean

[Bryan Gin-ge Chen]

Interesting... I wonder why there's a difference from the usual go to definition function.

[Alex J. Best]

Do you know if I need to setup the vscode extension for development to set breakpoints in vscode?

[Eric Wieser]

I think you do, yes - then you launch a new vscode instance from the one you develop the extension in

[Alex J. Best]

Ok on windows it seems the URI scheme when we get to https://github.com/leanprover/vscode-lean/blob/master/src/infoview.ts#L285 is set to "C" instead of "file" (https://docs.microsoft.com/en-us/dotnet/api/system.uri.scheme?view=net-5.0) it seems something is parsing "C:/..." as a uri scheme instead of a drive

[Bryan Gin-ge Chen]

And that function, revealEditorPosition seems to be called from here, being passed Uri.parse(message.loc.file_name).

[Bryan Gin-ge Chen]

So is Lean returning file_names differently for the usual go to definition command and the go to definition button in the widget?

[Alex J. Best]

I think it should use Uri.file instead of Uri.parse

[Alex J. Best]

Building with that change it works for me (as does the usual go to definition via F12)

[Bryan Gin-ge Chen]

Oh yeah, it looks like Uri.file is used almost everywhere else in the extension. There are a few instances of Uri.parse in src/docview.ts: are there issues there on Windows as well?

[Alex J. Best]

https://github.com/leanprover/vscode-lean/pull/258

[Alex J. Best]

I'll look now

[Alex J. Best]

I also think upstream https://github.com/microsoft/vscode-uri/pull/12 might fix this too, but I have no idea how to tell when / if that will make it to a vscode release (or if it has already)

[Eric Wieser]

I think I was looking at making a change in the other direction at one point, Uri.file doesn't work on unsaved buffers as far as I remember

[Bryan Gin-ge Chen]

@Kevin Buzzard I guess it may be too late now for your course, but Gabriel just released vscode-lean 0.16.24 which includes this fix.

[Alex J. Best]

Bryan Gin-ge Chen said:

Oh yeah, it looks like Uri.file is used almost everywhere else in the extension. There are a few instances of Uri.parse in src/docview.ts: are there issues there on Windows as well?

what is doc view used for ? Is it that nice thing where you can view a tutorial in vscode as a separate editor pane, if so can someone point me to where I can set that up (I've looked to no avail!)

[Alex J. Best]

Ah, got it, its built in to the extension lol!

[Bryan Gin-ge Chen]

Yep, I think if you hit ctrl+shift+p and search for "Lean: open documentation view" it should open a panel with some links you can try.

[Alex J. Best]

Yeah they seem to work fine as-is.

[Alex J. Best]

Eric Wieser said:

I think I was looking at making a change in the other direction at one point, Uri.file doesn't work on unsaved buffers as far as I remember

Do you mean completely new buffers, or just any buffers with unsaved changes in?

[Eric Wieser]

Completely new buffers

[Eric Wieser]

In particular, try this does not work in those buffers

[Eric Wieser]

And nor do \-inputs until you leave the new buffer and reenter it, although that's unlikely to be related to URIs