Error with v4.10.0

Stream: lean4

[Etienne Marion]

Hi! I just pulled master on my computer, but when I do lake exe cache get or lake clean or lake build, I get: error: toolchain 'leanprover/lean4:v4.10.0' does not have the binary /Users/etienne/.elan/toolchains/leanprover--lean4---v4.10.0/bin/lake. Can someone help please?

[Sebastian Ullrich]

Could you try elan toolchain uninstall v4.10.0 and try again?

[Etienne Marion]

Thanks for your answer. It didn't work, I got info: no toolchain installed for 'v4.10.0'.

[Sebastian Ullrich]

Is your elan very old?

[Etienne Marion]

Hmmm, that's very possible

[Sebastian Ullrich]

elan self update updates it

[Etienne Marion]

That didn't work

[Sebastian Ullrich]

Then you need to rerun the elan installer from the website

[Etienne Marion]

Ok I'll do that, thanks

[Etienne Marion]

When I do elan --help, it prints elan 3.1.1 (71ddc6633 2024-02-22), which seems to be the latest release?

[Sebastian Ullrich]

My bad, try elan uninstall leanprover/lean4:v4.10.0

[Etienne Marion]

That worked, thank you very much!