Fix canonical paths for paths with spaces #3491
Conversation
After testing today's version of Dafny in VSCode, I realized that a path with name triggered an error when attempting to resolve includes. Hence, I added a unit test to catch this regression for next time and fixed the method that trasnforms file paths (which can be gross URI) to actual file locations
| if (filePath.StartsWith("file:\\")) { | ||
| // Recovery mechanisms for the language server | ||
| return filePath.Substring("file:\\".Length); | ||
| var potentialPrefixes = new List<string>() { "file:\\", "file:/", "file:" }; |
There was a problem hiding this comment.
I'm surprised we need custom code to handle file paths. Why can't Uri help us with all our path parsing and canonicalisation needs?
Also, where do all these potential prefixes come from? Can we document that?
There was a problem hiding this comment.
I'm surprised too.
There is some history about that. In the formatter, I had to switch to plain file URIs for token's filenames, because otherwise it would not be consistent with VSCode URIs. It looks like VSCode's URIs are slightly different than LSP URI, for example, a period in a disk name is encoded on one and not the other.
I wish there is a better solution but for now it's urgent we have a fix. I remember having spent a lot of time previously to ensure everything was working acceptably on the CLI and the language server (including unsaved files, and stdin), both on Windows and Linux.
Yesterday was the first time I tested the code for paths with spaces, and that's probably why it wasn't caught before. After this fix is pushed, feel free to experiment with different alternatives.
MikaelMayer
added
kind: bug
This reverts commit 9e16ab3.
Redo #3491. Co-authored-by: Mikaël Mayer <[email protected]>
After testing today's version of Dafny in VSCode, I realized that a path with name triggered an error when attempting to resolve includes. Hence, I added a unit test to catch this regression for next time and fixed the method that transforms file paths (which can be gross URI) to actual file locations
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.