Error when updating Elan

Stream: lean4

[Daniel Donnelly]

Internal error (while activating Lean 4 features): Error: command 'lean4.restartFile' already exists

Error: command 'lean4.restartFile' already exists
    at mw.registerCommand (file:///c:/VSCode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:112:31435)
    at Object.registerCommand (file:///c:/VSCode/resources/app/out/vs/workbench/api/node/extensionHostProcess.js:172:36499)
    at new t.LeanClientProvider (c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:276681)
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:204550
    at Generator.next (<anonymous>)
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:199892
    at new Promise (<anonymous>)
    at s (c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:199637)
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:204508
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:205110
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:316924
    at Generator.next (<anonymous>)
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:316765
    at new Promise (<anonymous>)
    at i (c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:316510)
    at t.displayInternalErrorsIn (c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:316873)
    at c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:204450
    at Generator.next (<anonymous>)
    at s (c:\Users\fruit\.vscode\extensions\leanprover.lean4-0.0.194\dist\extension.js:1:199694)

Can I ignore it?

[Kim Morrison]

Could you explain what you are doing to produce this error (ideally with reproducible instructions, e.g. clone this repo, checkout this commit, run this command)?

[Marc Huisinga]

This error usually occurs when you have two extensions installed that both contribute the same VS Code command, e.g. the Lean 4 extension and one of the broken forks that exist on the VS Code marketplace. Is that the case in your setup?

[Floris van Doorn]

When updating elan to 4.0.0 on Windows I get the output

Floris@Dell-E MINGW64 ~/projects/mathlib ((6befc6324c7...))
$ elan self update
info: downloading self-update
info: elan updated successfully to 4.0.0
error: could not create link from 'C:\Users\Floris\.elan\bin\elan.exe' to 'C:\Users\Floris\.elan\bin\lake.exe'

It seems that despite the error, everything is working correctly for me afterwards (note: both the mentioned files do exist)