Zulip Chat Archive

Stream: general

Topic: Broken "Go To Definition"?

Adam Topaz (May 20 2022 at 14:12):

I'm having issues with "Go To Definition" in VSCode. Is anyone else running into similar issues? Here's an example:
animation.gif

Eric Rodriguez (May 20 2022 at 14:18):

I sometimes get it, also when goto definition goes to exact and such

Gabriel Ebner (May 20 2022 at 14:23):

Regression from https://github.com/leanprover/vscode-lean/pull/301 A fix is coming to your vscode any minute.

Eric Wieser (May 20 2022 at 14:31):

Whoops, sorry!

Eric Wieser (May 20 2022 at 14:32):

(fix was https://github.com/leanprover/vscode-lean/commit/6d025025ee6b2f1ebc7306e4a64af57e77a13410)

Adam Topaz (May 20 2022 at 14:45):

Thanks @Gabriel Ebner ! I can confirm that the issue is now resolved on my end!

Last updated: Dec 20 2023 at 11:08 UTC