elan
elan copied to clipboard
uninstall a toolchain leaves a mess when a file is locked.
- Lock the lean.exe by running it in VS Code
- run
elan toolchain uninstall leanprover/lean4:nightly
to try and remove that version
Actual: it fails to remove the locked file but leaves things in a bad state where the directory is still there by there's no easy way to clean it up except manually going in and removing the folder. Here's the log of what I'm talking about.
(ell) D:\git\leanprover\lean4-samples\GuessMyNumber>elan toolchain uninstall leanprover/lean4:nightly info: uninstalling toolchain 'leanprover/lean4:nightly' error: could not remove 'update hash' file: 'C:\Users\clovett.REDMOND.elan\update-hashes\leanprover--lean4---nightly' info: caused by: The system cannot find the file specified. (os error 2)
(ell) D:\git\leanprover\lean4-samples\GuessMyNumber>dir c:\Users\clovett.REDMOND.elan\update-hashes\
Volume in drive C is Windows
Volume Serial Number is 7CCB-580B
Directory of c:\Users\clovett.REDMOND\.elan\update-hashes
06/28/2022 09:56 AM <DIR> .
06/28/2022 09:56 AM <DIR> ..
06/22/2022 01:31 PM 75 leanprover--lean4---nightly-2022-06-19
06/22/2022 01:22 PM 75 leanprover--lean4---nightly-2022-06-21
06/22/2022 01:36 PM 75 leanprover--lean4---nightly-2022-06-22
06/22/2022 07:36 PM 58 leanprover--lean4---stable
4 File(s) 283 bytes
2 Dir(s) 64,132,751,360 bytes free
(ell) D:\git\leanprover\lean4-samples\GuessMyNumber>dir c:\Users\clovett.REDMOND.elan\toolchains
Volume in drive C is Windows
Volume Serial Number is 7CCB-580B
Directory of c:\Users\clovett.REDMOND\.elan\toolchains
06/22/2022 07:36 PM <DIR> .
06/22/2022 07:36 PM <DIR> ..
06/28/2022 09:56 AM <DIR> leanprover--lean4---nightly
06/22/2022 01:31 PM <DIR> leanprover--lean4---nightly-2022-06-19
06/22/2022 01:22 PM <DIR> leanprover--lean4---nightly-2022-06-21
06/22/2022 01:36 PM <DIR> leanprover--lean4---nightly-2022-06-22
06/22/2022 07:36 PM <DIR> leanprover--lean4---stable
0 File(s) 0 bytes
7 Dir(s) 64,132,685,824 bytes free
rd /s /q c:\Users\clovett.REDMOND.elan\toolchains\leanprover--lean4---nightly
Now I can re-install that version.