Zulip Chat Archive

Stream: general

Topic: go to definition failing for some people


Kevin Buzzard (Feb 11 2021 at 17:20):

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 (Feb 11 2021 at 17:28):

I haven't seen this before fwiw

Bryan Gin-ge Chen (Feb 11 2021 at 17:31):

Is there a #mwe?

Alex J. Best (Feb 11 2021 at 17:43):

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

Bryan Gin-ge Chen (Feb 11 2021 at 17:56):

@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 (Feb 11 2021 at 17:57):

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 (Feb 11 2021 at 18:02):

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

Alex J. Best (Feb 11 2021 at 18:04):

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

Eric Wieser (Feb 11 2021 at 18:13):

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

Alex J. Best (Feb 11 2021 at 18:44):

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 (Feb 11 2021 at 18:50):

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

Bryan Gin-ge Chen (Feb 11 2021 at 18:51):

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 (Feb 11 2021 at 18:57):

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

Alex J. Best (Feb 11 2021 at 18:59):

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

Bryan Gin-ge Chen (Feb 11 2021 at 19:03):

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 (Feb 11 2021 at 19:07):

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

Alex J. Best (Feb 11 2021 at 19:07):

I'll look now

Alex J. Best (Feb 11 2021 at 19:09):

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 (Feb 11 2021 at 19:18):

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 (Feb 11 2021 at 19:21):

@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 (Feb 11 2021 at 19:23):

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 (Feb 11 2021 at 19:27):

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

Bryan Gin-ge Chen (Feb 11 2021 at 19:27):

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 (Feb 11 2021 at 19:30):

Yeah they seem to work fine as-is.

Alex J. Best (Feb 11 2021 at 19:30):

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 (Feb 11 2021 at 20:55):

Completely new buffers

Eric Wieser (Feb 11 2021 at 20:56):

In particular, try this does not work in those buffers

Eric Wieser (Feb 11 2021 at 20:57):

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


Last updated: Aug 03 2023 at 10:10 UTC