`elan self update` fails with error `could not create link`

leanprover / elan

The Lean version manager

Apache License 2.0

292 stars 34 forks source link

`elan self update` fails with error `could not create link` #95

Open pwintz opened 1 year ago

pwintz commented 1 year ago

When I run elan self update, the following error occurs:

$  elan self update
←[1minfo: ←[0mchecking for self-updates
←[31m←[1merror: ←[0mcould not create link from 'C:\Users\pwintz\.elan\bin\elan.exe' to 'C:\Users\pwintz\.elan\bin\lake.exe'

Any suggestions for how to fix it?

matt8s commented 1 year ago

I am running Lean 4 on Visual Studio Code. I had the same issue with running this from the command line, while VS Code was open. Once I closed VS Code, I tried this again. With VS Code closed, it worked just fine!

Kha commented 1 year ago

It's an extremely annoying limitation of Windows