Install via Micrsoft wigent

Stream: new members

[Eric Taucher]

winget - Windows Package Manager Client, is currently (09/16/2021) preview/beta and does not list Lean as a package for installation.

Is anyone looking into this or has in their future todo list?

[Johan Commelin]

@Eric Taucher mathlib and lean3 currently don't have backwards compatibility high on their agenda. As a result, if you want to use different versions of mathlib, you also need different version of lean installed. The elan tool makes this completely transparent.
For that reason, many of us don't want a globally installed version of lean, but rather use elan.

Note that elan was inspired by rustup, afaik. It seems that rust has/had similar "issues".

[Johan Commelin]

Mathlib of today doesn't compile with Lean from last week.

[Johan Commelin]

(And mathlib from last week doesn't compile with Lean from today.)

[Eric Wieser]

Perhaps elan should be supported by Winget?