Finding all versions of lean on a system

Stream: Is there code for X?

[Jafar Tanoukhi]

Is there a way to find all versions of lean downloaded on my machine via the command prompt
lean --version
returns only one version (probably the latest)

[Markus Himmel]

You can use elan toolchain list or elan show.

[Jafar Tanoukhi]

so elan show worked nicely and gave me the following :

installed toolchains
--------------------

stable (default)
leanprover/lean4:stable
leanprover/lean4:v4.9.0-rc1

active toolchain
----------------

stable (default)
Lean (version 4.7.0, x86_64-w64-windows-gnu, commit 6fce8f7d5cd1, Release)

on my other system I receive this output :

installed toolchains
--------------------

stable (default)
leanprover/lean4:stable

active toolchain
----------------

stable (default)
Lean (version 4.10.0, x86_64-unknown-linux-gnu, commit c375e19f6b65, Release)

I have a couple questions though:
what exactly is lean4:stable, in the first one I thought it was lean 4.7 but here lean 4.10 also appears to be lean4:stable?

Is there a way where i get all the versions in this format Lean (version 4.7.0, x86_64-w64-windows-gnu, commit 6fce8f7d5cd1, Release) under each other ?

How do i switch my active tool chain to another version of lean ?

Context: I'm building a system that's supposed to interact with the LSP and I want it to detect the versions of lean in the user's system and 'pick' the one that's supported if there's any

[Markus Himmel]

stable is a "channel", it points to a certain version. You can run elan update stable to update the stable channel to the latest stable release (at the moment this is 4.11.0)

[Jafar Tanoukhi]

(deleted)

[Markus Himmel]

Jafar Tanoukhi said:

Is there a way where i get all the versions in this format Lean (version 4.7.0, x86_64-w64-windows-gnu, commit 6fce8f7d5cd1, Release) under each other ?

I don't really understand why you want this, but something like elan toolchain list | sed 's/ (default)//g' | xargs -I '{}' elan run '{}' lean --version should do it.

[Markus Himmel]

Jafar Tanoukhi said:

How do i switch my active tool chain to another version of lean ?

Basically all Lean users use Lean from a project directory which contains a lean-toolchain file which contains the Lean version that should be used when working on this project. See Mathlib's lean-toolchain file for example. If you want to change the default toolchain, which is used when you invoke lean somewhere outside of a Lean project, then you can do something like elan default 4.10.0.

[Jafar Tanoukhi]

@Markus Himmel said :

I don't really understand why you want this, but something like elan toolchain list | sed 's/ (default)//g' | xargs -I '{}' elan run '{}' lean --version should do it.

I will not act like i know what I'm doing lol, but basically what my system "wants to do" is the following :

1. run the command to get all lean versions of the system
2. parse the result and get all version numbers
3. find a version number compatible with the system
4. work normally if a compatible version was found or show a warning if it was not

now with something like lean4:stable, the parsing would be a little annoying i believe (maybe also not possible?) because I'm not sure how to go from stable -> 4.11.0 (or whatever the stable channel is currently on the user's system is)

so I think this works perfectly for me, thanks alot!

[Jafar Tanoukhi]

Markus Himmel said:

Basically all Lean users use Lean from a project directory which contains a lean-toolchain file which contains the Lean version that should be used when working on this project. See Mathlib's lean-toolchain file for example. If you want to change the default toolchain, which is used when you invoke lean somewhere outside of a Lean project, then you can do something like elan default 4.10.0.

Yes, makes sense too, i also found this other command :
elan override set <version or channel goes here>