leanprover/lean4:v4.6.tmp

Stream: lean4

[Utensil Song]

I was installing Lean via lake build in an unstable network environment, somehow the process is aborted, then the installation could not resume:

% lake build
error: toolchain 'leanprover/lean4:v4.6.0-rc1' is not installed
% elan toolchain list
leanprover/lean4:nightly
leanprover/lean4:stable
leanprover/lean4:v4.6.tmp
leanprover/lean4:v4.7.0
leanprover/lean4:v4.8.0-rc1 (default)
leanprover/lean4:v4.8.0-rc
% elan toolchain uninstall leanprover/lean4:v4.6.tmp
info: uninstalling toolchain 'leanprover/lean4:v4.6.tmp'
error: could not remove 'update hash' file: '/Users/utensil/.elan/update-hashes/leanprover--lean4---v4.6.tmp'

I could fix this by manually removing some directories but this stuck could happen to others, so I report it here. Either installation should be able to resume in this situation, or uninstallation should work.

Gently tagging @Mac Malone as I'm not sure if it's a lake issue or an elan one.

[Utensil Song]

What's under /Users/utensil/.elan/update-hashes/ is leanprover--lean4---v4.6.0-rc1, after removing it and the 4.6.tmp toolchain directory, the installation can resume again.