Backslash for unicode breaks down often in recent version of lean4

[Qiu233]

Sometimes the backslash symbol \ become plain text rather with an underline indicating it's pending further input. To fix it I must either:

• restart vscode
• reopen the current file
• restart file (only works for my macbook, but not for wsl)

I have been experiencing this problem very often since updating to 4.9.0, on both macos and windows with wsl. The cause isn't clear. I tried different vscode extension versions published months ago but the problem still remains, so the language server is more likely to have caused this.

[mhuisi]

The language server is not involved here - the underlines and the Unicode mechanism are entirely client sided.

Some questions:

• Are you using a setup where Lean is not running directly on your computer? For example, using Gitpod and SSH is known to cause some issues in the abbreviation provider due to limitations in VS Code.
• Does the issue occur both with v0.0.170 and v0.0.124 of the VS Code extension?
• Are you using any other VS Code extensions that might interfere with input? For example, the Vim VS Code extension is known to cause some issues when used together with the Unicode input mechanism.
• When this happens, are there any errors in the "Lean: Editor" output panel or the developer console? You can open the former using the "Troubleshooting: Show Output" command and the latter using the "Developer: Toggle Developer Tools" command (the output is in the "Console" tab)

[Qiu233]

• no, I was using it from wsl and macos, from months ago, and this problem only occurs recently
• as I just tried now, yes, this problem still happens after switching to v0.0.124, also note that I didn't restart vscode after switching the extension version
• I guess no, my macos vscode has only environment for lean4
• YES there are errors in the developer tools, and they seem to have a common pattern. Here's the most recent ones:

console.ts:137 [Extension Host] rejected promise not handled within 1 second: TypeError: Cannot read properties of undefined (reading 'dispose')
C @ console.ts:137
console.ts:137 [Extension Host] stack trace: TypeError: Cannot read properties of undefined (reading 'dispose')
at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973)
at Generator.next ()
at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285)
at processTicksAndRejections (node:internal/process/task_queues:95:5)
C @ console.ts:137
mainThreadExtensionService.ts:81 [leanprover.lean4]Cannot read properties of undefined (reading 'dispose')
$onExtensionRuntimeError @ mainThreadExtensionService.ts:81
mainThreadExtensionService.ts:82 TypeError: Cannot read properties of undefined (reading 'dispose')
at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973)
at Generator.next ()
at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285)
at processTicksAndRejections (node:internal/process/task_queues:95:5)
$onExtensionRuntimeError @ mainThreadExtensionService.ts:82
console.ts:137 [Extension Host] rejected promise not handled within 1 second: TypeError: Cannot read properties of undefined (reading 'dispose')
C @ console.ts:137
console.ts:137 [Extension Host] stack trace: TypeError: Cannot read properties of undefined (reading 'dispose')
at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973)
at Generator.next ()
at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285)
at processTicksAndRejections (node:internal/process/task_queues:95:5)
C @ console.ts:137
mainThreadExtensionService.ts:81 [leanprover.lean4]Cannot read properties of undefined (reading 'dispose')
$onExtensionRuntimeError @ mainThreadExtensionService.ts:81
mainThreadExtensionService.ts:82 TypeError: Cannot read properties of undefined (reading 'dispose')
at t.AbbreviationRewriterFeature. (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:159973)
at Generator.next ()
at s (/home/qiu/.vscode-server/extensions/leanprover.lean4-0.0.170/dist/extension.js:1:158285)
at processTicksAndRejections (node:internal/process/task_queues:95:5)

[mhuisi]

also note that I didn't restart vscode after switching the extension version

You should! Or at least click the "Restart Extensions" button that shows up in the extension entry after the update. Otherwise it will still use the previous version.

Could you also double-check that the issue indeed does not occur with Lean v4.8.0 on v0.0.170 of the extension?

[mhuisi]

(By the way, the error you saw above is likely unrelated but will be fixed by #492. Thanks for the report.)

[mhuisi]

Are you still encountering this issue?

[Qiu233]

It's almost solved now. But sometimes unicode fails, leave it as is and the bottom panel of vscode shows up with errors. Redoing it will fix.

There's another cursor issue which I am not sure related to this issue or not.
For example, when typing \times I usually got × but with cursor on the left of it.
This happens more often when typing faster, especially working in codespace remotely.

[mhuisi]

But sometimes unicode fails, leave it as is and the bottom panel of vscode shows up with errors.

What is the error you are seeing and what is your current vscode-lean4 version?

FWIW, the fact that replacing the abbreviation sometimes fails is unfortunately something we can't fix (VS Code doesn't support transactions for updating editor state, so if the editor state has changed since the abbreviation mechanism was called, VS Code simply rejects our edits to the document).

There's another cursor issue which I am not sure related to this issue or not.

For this issue, it would also be good to know what your vscode-lean4 version is. We fixed this issue a while ago unless you are also using the Vim extension, in which case text edits issued by the Vim extension and vscode-lean4 can interfere.