search

meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
58 stars 10 forks source link

file path is wrong within workspace with multiple folders #70

Closed iacore closed 2 years ago

iacore commented 2 years ago

I have the following workspace with two folders: image

You can add a new folder to the current workspace like this image

The errors are shown in the "Problems" tab but not in the file editor (no squiggle underlines). image

Note that the file path is /null/..., which is wrong.

iacore commented 2 years ago

I think I found the issue, but I can't make the extension work at all after the change. https://github.com/locriacyber/idris-vscode/commit/c0b8541b4014ae3c3c5608610cea1eae845e43e5

meraymond2 commented 2 years ago

Hi, thanks for the issue, I'll look into it as soon as I have time.

Are you using Idris 1 or 2?

iacore commented 2 years ago

Hi, thanks for the issue, I'll look into it as soon as I have time.

Are you using Idris 1 or 2?

Idris 2, as shown in the images above.

meraymond2 commented 2 years ago

I've had a look, I didn't reproduce the /null/ path bug, but I think I know what the problem is. The extension is just a translation layer between the Idris IDE process and VS, and currently it only ever launches a single Idris process. That IDE process needs to be launched in the app directory for the IDE commands to work, so to work with a multi-root workspace it would need to launch multiple processes, one per workspace-folder.

That the logic to get the directory path is assuming a single workspace-folder is definitely a mistake, at the very least it should display an error to the user that it can't currently handle multi-root workspaces. Your change would make it work, but only for the first folder.

For now, I'll document that it doesn't support multi-root workspaces, because the current behaviour is confusing and annoying. Longer term, I think launching multiple client processes could work, but I'm not sure how complicated it would be, so it might take a while.