elan icon indicating copy to clipboard operation
elan copied to clipboard

uninstall a toolchain leaves a mess when a file is locked.

Open lovettchris opened this issue 2 years ago • 0 comments

  1. Lock the lean.exe by running it in VS Code
  2. 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.

lovettchris avatar Jun 28 '22 17:06 lovettchris