Zulip Chat Archive
Stream: lean4
Topic: Update toolchain
Markus Schmaus (May 28 2024 at 12:11):
On my computer I have an installed toolchain for a lean PR (leanprover/lean4-pr-releases:pr-release-4242
), since I pushed a commit to lean#4242, I wanted to update the toolchain, but the natural elan install
resulted in an unchanged toolchain.
$ elan toolchain install leanprover/lean4-pr-releases:pr-release-4242
leanprover/lean4-pr-releases:pr-release-4242 unchanged - Lean (version 4.9.0, x86_64-unknown-linux-gnu, commit 2c64390d8fba, Release)
I was able to get a new version by uninstalling and reinstalling the toolchain
$ elan toolchain uninstall leanprover/lean4-pr-releases:pr-release-4242
info: uninstalling toolchain 'leanprover/lean4-pr-releases:pr-release-4242'
info: toolchain 'leanprover/lean4-pr-releases:pr-release-4242' uninstalled
$ elan toolchain install leanprover/lean4-pr-releases:pr-release-4242
info: downloading component 'lean'
243.2 MiB / 243.2 MiB (100 %) 20.1 MiB/s ETA: 0 s
info: installing component 'lean'
leanprover/lean4-pr-releases:pr-release-4242 installed - Lean (version 4.9.0, x86_64-unknown-linux-gnu, commit 82187a1aeab5, Release)
Is there a better way to update such a toolchain other then uninstalling and reinstalling?
Kim Morrison (May 28 2024 at 12:20):
No, this is the preferred method.
Kim Morrison (May 28 2024 at 12:20):
It's a hack in the first place that we are overwriting a toolchain: this is outside the intended usage of elan.
Last updated: May 02 2025 at 03:31 UTC