Goto definition bug on Windows to do with case folding file names.

[lovettchris]

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Goto definition sometimes case folds the file name to lower case, and when this happens the infoview information stops flowing. I suspect this bug is caused by the case folding in lean_io_realpath:

        // Hack for making sure disk is lower case
        // TODO(Leo): more robust solution
        if (strlen(buffer) >= 2 && buffer[1] == ':') {
            buffer[0] = tolower(buffer[0]);
        }

but there is more case folding in the LSP in the calls to (* realPath).normalize which I think also create problems if that case folded name is ever returned the the LSP in response to a "textDocument/definition" request instead of the original un-case folded name.

PS: One could argue this may also be a VS Code framework bug in that they should not care about any casefolding on Windows and things should "just work" even if we do case folding.

Steps to Reproduce

1. on Windows create a folder named "c:\Temp" with an upper case T.
2. in that folder run git clone git@github.com:leanprover/vscode-lean4.git
3. cd vscode-lean4\vscode-lean4\test\test-fixtures\simple
4. code .
5. Open Main.lean and the InfoView should print "4.0.0-nightly-2022-02-17" for the Lean.versionString.
6. Place the cursor in the middle of getLeanVersion and press F12 (goto definition)
7. It will open "version.lean" and not "Version.lean" and as a result the infoView does not update no matter what you do in this file.

Expected behavior: [What you expect to happen] The file should be named Version.lean and the infoview should work.

Actual behavior: [What actually happens] infoView does not update no matter what you do in this file

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[Vtec234]

Is it even a bug to open the lower-cased version, given that NTFS is case-insensitive and so this is the same file? Perhaps we should distinguish since people do assign semantics to casing, but it sounds like the real bug is in the infoview which should treat version.lean and Version.lean as equivalent on Windows. Okay, sorry, you are right. The LSP spec and hence the infoview use RFC3986 URIs which are case-sensitive in the path component, regardless of OS. So while normalising in realpath sounds correct, we should make sure to preserve cases when sending LSP URIs in the server.

[Kha]

Could you attach the LSP log?

I suspect this bug is caused by the case folding in lean_io_realpath:

Hmm, how could that possible affect Version?

but there is more case folding in the LSP in the calls to (* realPath).normalize

I didn't immediately see a use that should affect file names, only search paths (i.e. directories)

[gebner]

:+1: for the LSP logs. It would also be interesting to see what this prints on windows:

#eval IO.FS.realPath "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\Version.lean"
#eval IO.FS.realPath "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\version.lean"

[lovettchris]

You are right, realpath is only case folding the drive letter, so I don't think that is the issue here.

#eval IO.FS.realPath "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\Version.lean"
#eval IO.FS.realPath "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\version.lean"

outputs

Main.lean:10:0
FilePath.mk "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\Version.lean"
Main.lean:12:0
FilePath.mk "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\version.lean"

Logs of the goto definition repro attached: logs.zip

[EdAyers]

Hello I also see this when I go to definition on macOS, so it's not just a windows bug.