Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
lovettchris opened this issue Jun 28, 2022 · 0 comments
Open

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

lovettchris opened this issue Jun 28, 2022 · 0 comments

Comments

@lovettchris
Copy link
Contributor

  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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant