Zulip Chat Archive

Stream: lean4

Topic: Go to import

Yaël Dillies (Jul 16 2023 at 17:17):

Is it expected that one can no longer right-click on an import to go to the file?

Yury G. Kudryashov (Jul 16 2023 at 17:17):

Works for me in Emacs ;)

Yury G. Kudryashov (Jul 16 2023 at 17:18):

(though many fancy new features don't work)

Mario Carneiro (Jul 16 2023 at 17:21):

That works for me

Yaël Dillies (Jul 16 2023 at 17:21):

Let me revise my statement: it works sometimes

Mario Carneiro (Jul 16 2023 at 17:21):

when?

Yaël Dillies (Jul 16 2023 at 17:22):

I can't tell yet. But when it doesn't work, it doesn't work on any file. I just reloaded my gitpod window, so I suspect there's something wrong with the extension that got reset during reload.

Mario Carneiro (Jul 16 2023 at 17:22):

it should hopefully be easy to guess that the answer to "is it expected that go-to-def on imports only works some of the time" is "no"

Mario Carneiro (Jul 16 2023 at 17:24):

although I shouldn't be too facetious since the answer to "is it expected that go-to-def on builtin syntax only works some of the time" is "yes"

Yaël Dillies (Jul 16 2023 at 17:24):

Debugging further... but I cannot reproduce

Kevin Buzzard (Jul 16 2023 at 19:56):

Is ctrl-click any more reliable?

Last updated: Dec 20 2023 at 11:08 UTC