Zulip Chat Archive

Stream: general

Topic: go to definition failing for some people


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 11 2021 at 17:28):

I haven't seen this before fwiw

view this post on Zulip Bryan Gin-ge Chen (Feb 11 2021 at 17:31):

Is there a #mwe?

view this post on Zulip Alex J. Best (Feb 11 2021 at 17:43):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Alex J. Best (Feb 11 2021 at 18:57):

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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Alex J. Best (Feb 11 2021 at 19:07):

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

view this post on Zulip Alex J. Best (Feb 11 2021 at 19:07):

I'll look now

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip Alex J. Best (Feb 11 2021 at 19:27):

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

view this post on Zulip 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.

view this post on Zulip Alex J. Best (Feb 11 2021 at 19:30):

Yeah they seem to work fine as-is.

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Feb 11 2021 at 20:55):

Completely new buffers

view this post on Zulip Eric Wieser (Feb 11 2021 at 20:56):

In particular, try this does not work in those buffers

view this post on Zulip 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: May 11 2021 at 00:31 UTC