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