search

leanprover / elan

The Lean version manager
Apache License 2.0
292 stars 34 forks source link

Deleting from `~/.elan/toolchains` but leaving matching `~/.elan/update-hashes` leaves elan in broken state. #107

Closed semorrison closed 2 months ago

semorrison commented 11 months ago 
% elan toolchain install leanprover/lean4:v4.0.0
% rm -rf ~/.elan/toolchains/leanprover--lean4---v4.0.0
% lake +leanprover/lean4:v4.0.0 env                   
error: toolchain 'leanprover/lean4:v4.0.0' is not installed
% elan toolchain install leanprover/lean4:v4.0.0

  leanprover/lean4:v4.0.0 unchanged - (toolchain not installed)
% lake +leanprover/lean4:v4.0.0 env                     
error: toolchain 'leanprover/lean4:v4.0.0' is not installed

We had this happen on Hoskinson overnight!

It would be great if elan could detect this condition (toolchain apparently present in update-hashes, but missing in toolchain) and cope, either by cleaning up or explaining how to clean up.

To be fair, this is users abusing elan, but it's an easy failure mode for someone wanting to delete big files.

Kha commented 11 months ago

update-hashes will be gone with #106