elan

Stream: lean4

[Sebastian Ullrich]

https://github.com/leanprover/elan/pull/98 moves elan documentation and defaults to Lean 4. Existing Lean 3 projects should continue to work as is.

[Scott Morrison]

One thought about the documentation:

The fact that you can create custom releases of Lean 4 simply by pushing a tag to your own fork, and then specifying e.g. semorrison/lean4:release-20230620-max either in lean-toolchain or with elan toolchain, seems to be a secret only "documented" in zulip. Might we want to add a sentence or two here? This is really useful to know if when you need to test changes against mathlib (and want CI assistance, so mere elan override with a local Lean 4 is insufficient).

I could add said sentences to the PR if that's helpful.

(I'll pre-emptively agree this advice should be in the manual as well!)

[Scott Morrison]

Relatedly, if we can work out how to deprecate the lean formula for Homebrew, we would want to do that, right? It is only a trap.

[Scott Morrison]

(Indeed, we might even try to arrange for elan-init on homebrew to be renamed or aliased to lean.)

[Scott Morrison]

https://github.com/Homebrew/homebrew-core/pull/135186

[Sebastian Ullrich]

Mario Carneiro said:

the use of an explicit date in the readme is definitely suboptimal, that will very obviously get out of date

https://github.com/leanprover/elan/pull/99 implements a new kind of toolchain reference that allows us to use the correct Lean version even before downloading mathlib4, avoiding any redundant downloads and outdated readmes

[Mario Carneiro]

Amazing :tada: :rainbow:

[Mario Carneiro]

Does something like leanprover-community/mathlib4@master:lean-toolchain work?

[Sebastian Ullrich]

Not yet... is it necessary? :)

[Mario Carneiro]

does it just use the default branch?

[Sebastian Ullrich]

It does: https://github.com/leanprover/elan/pull/99/files#diff-c23944b7c4d02d84948dcdc3c50fe1fa45767be70e1a898dacd5b9982299cffbR49

[Sebastian Ullrich]

Note that we can now use the same mechanism to ensure that nightly always points to the most recent nightly, not whatever version was recent when elan was first installed/the toolchain was updated explicitly. This will mean that if you use the nightly default default AND work on a Lean file outside a project with pinned lean-toolchain, elan will frequently redownload Lean, but I believe that is the best compromise we can accomplish

[Notification Bot]

7 messages were moved here from #lean4 > installing lean 4, keeping lean 3 by Sebastian Ullrich.