Go-to-def

[joneugster]

Would be nice to have go-to-def open the correct page of the docs: https://leanprover-community.github.io/mathlib4_docs/

[joneugster]

2b799f7 implements a go-to-def functionality.

• It just opens the corresponding doc-gen page, but is missing #My.Lean.Declaration in the URL.
• There is a console error associated with it: Ctrl+Hover over any definition to see it.
• Have to click "Cancel" 4-5 times :(

[tautastic]

@joneugster I still have the Have to click "Cancel" 4-5 times :( bug on macOS but not on Linux. Also the console error when doing Ctrl+Hover over any definition is also present in lean4monaco demo project, so this seems not related to the go-to-def functionality.

[joneugster]

It is related (not in the custom gotodef, but in monaco's gotodef), but youre right, ctrl-hiver should be fixed in lean4monaco. (sometimes the issues between lean4monaco and lean4web arent perfectly separated)

[tautastic]

Also doing right-click then Go To References shows many References that seem valid but trying to view any of them that are not part of the current file throws a similar error. Could we allow lean4monaco access to the .lake/packages directory. Or maybe the first question is: do we want to? If not then maybe we should try to remove the cases where these kinds of errors occur. Also same issue for right-click then peek > peek definition and peek > peek type definition

[tautastic]

@joneugster A quick temporary fix would be to open the source code instead of the docs, since we have the line number we can link directly to what was clicked on. See the code changes here: tautastic@5ce8886

[joneugster]

I think when I implemented this I decided that opening the correct doc page without line numer is nicer than opening the source. But that's probably just personal taste. Ofc getting the relevant info to open the right doc would be ideal

[tautastic]

Is the desired behavior to improve the current solution or to get the "go-to" and "peek" stuff to work just like in vscode? I mean the mathlib files are on the server we could just open them in a new editor tab.

[joneugster]

That could be a nice feature, I suppose 👍

[joneugster]

The go-to-def feature seems now to be broken, I'm disabling the test for now