## 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

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

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: May 11 2021 at 00:31 UTC