Backslash for unicode breaks down often in recent version of lean4 about vscode-lean4

[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.)