Goto definition won't work on Windows

[ice1000]

As title.

[ice1000]

I said it doesn't work on Windows because I assume it works on @banacorn's machine, and IIRC he's using a Mac.

[ice1000]

I wonder if there's a way to debug this.

[banacorn]

Thanks, I'll check this out on my gaming PC 😉

[ice1000]

Don't forget that we have nightly binary releases :)

[banacorn]

Root cause: file paths are case-insensitive on Windows I get C:\... from the editor and c:\... from Agda 🥲

[ice1000]

Can't wait to see new release

[ice1000]

Well, it still doesn't seem to work. Can you test if it works for you? @banacorn

[davidmrdavid]

Hey folks, I seem to be running into this issue. Any way I can help debug?

[ShreckYe]

I got this again about 1 or 2 months ago, too. And reinstalling everything doesn't seem to fix the problem.

[mxs1285]

This issue is still a thing, my goto-definition doesn't seem to work.

An example is:

 ≤-lemma : (m n : ℕ) → suc m ≤ suc n → m ≤ n
 ≤-lemma m n (≤-suc m n p) = p

When I attempt to goto-definition, F12, on ≤-suc it only recognises ≤ or suc, wherever the cursor is currently over. Even if I just try to jump to suc it cannot find anything. All the same No definition found for {whatever}. This is a really useful feature and my friend on Mac is able to with no issues ! :(

Worth mentioning that ≤-suc is defined in the exact same file, not that it should matter.

[ice1000]

When I attempt to goto-definition, F12, on ≤-suc it only recognises ≤ or suc, wherever the cursor is currently over.

This is because the language server didn't give a response, so vscode defaults to its own silly lexer

[fredrik-bakke]

When I attempt to goto-definition, F12, on ≤-suc it only recognises ≤ or suc, wherever the cursor is currently over.

This is because the language server didn't give a response, so vscode defaults to its own silly lexer

Is it possible that #149 resolves this?