This error originally manifested in the extension https://github.com/leanprover/vscode-lean after the 1.11.1 update, as capital completions appearing before any others (even though case-insensitive sort was requested). It appears to trace back to commit 112ce25, which will sort 'B' < 'a'.
- VSCode Version: 1.11.1
- OS Version: Windows 10
I'm not sure how to reproduce this in other modes, but this may suffice:
- Create a new file in javascript mode, and type
var ab, aA, aB, aa, a; the text completions appear in the order aA, ab, aB, aa.
This isn't a great test because I don't know if that is the intended order, but the vscode-lean extension, which is using compareIgnoreCase directly, is definitely getting wrong results.
This error originally manifested in the extension https://github.com/leanprover/vscode-lean after the 1.11.1 update, as capital completions appearing before any others (even though case-insensitive sort was requested). It appears to trace back to commit 112ce25, which will sort
'B' < 'a'.I'm not sure how to reproduce this in other modes, but this may suffice:
var ab, aA, aB, aa, a; the text completions appear in the orderaA,ab,aB,aa.This isn't a great test because I don't know if that is the intended order, but the
vscode-leanextension, which is usingcompareIgnoreCasedirectly, is definitely getting wrong results.