elan update on Windows gives error

Stream: lean4

[Avi Craimer]

Hi,

I wanted to update my installation of Lean from 4.0 to 4.1.

On windows I opened an admin terminal and ran elan update

 leanprover/lean4:nightly update failed - Lean (version 4.0.0-nightly-2022-06-09, commit d0499ebf4d92, Release)
error: could not remove 'elan-bin' file: 'C:\Users\myUserName\.elan\bin\elan.exe'
info: caused by: Access is denied. (os error 5)

Is there another way to update the Lean version on Windows?

[Scott Morrison]

I think someone just had this problem and closing VSCode first solved the problem. Could you try that?

[Scott Morrison]

but --- you don't actually need to do anything to elan to move from 4.0 to 4.1

[Scott Morrison]

you just edit the lean-toolchain file in your project

[Avi Craimer]

Ok, so I exited VSCode and ran the elan update and it worked. It updated it to the nightly build 4.3.

I don't know yet about using project files. I've just been editing the code in individual .lean files.