Closed Kha closed 1 year ago
@semorrison I think it's roughly documented at the right place:
$ elan toolchain help
elan-toolchain
Modify or query the installed toolchains
USAGE:
elan toolchain <SUBCOMMAND>
FLAGS:
-h, --help Prints help information
SUBCOMMANDS:
list List installed toolchains
install Install or update a given toolchain
uninstall Uninstall a toolchain
link Create a custom toolchain by symlinking to a directory
help Prints this message or the help of the given subcommand(s)
DISCUSSION:
Many `elan` commands deal with *toolchains*, a single
installation of the Lean theorem prover. `elan` supports multiple
types of toolchains. The most basic track the official release
channel: 'nightly'; but `elan` can also install toolchains from
the official archives and from local builds.
Standard release channel toolchain names have the following form:
[<origin>:]<channel>[-<date>]
<channel> = nightly|<version>
<date> = YYYY-MM-DD
'channel' is either a named release channel or an explicit version
number, such as '4.0.0-m5'. Channel names can be optionally appended
with an archive date, as in 'nightly-2018-04-10', in which case
the toolchain is downloaded from the archive for that date.
'origin' can be used to refer to custom forks of Lean on Github;
the default is 'leanprover/lean'. For nightly versions, '-nightly'
is appended to the value of 'origin'.
elan can also manage symlinked local toolchain builds, which are
often used to for developing Lean itself. For more information see
`elan toolchain help link`.
That doesn't tell you how to create such a release, but that doesn't really belong to elan's documentation
I've added information about generating releases from tags at https://github.com/leanprover/lean4/pull/2302.
Let's merge this, and I'll update the community webpage docs!
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 inlean-toolchain
or withelan 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 mereelan override
with a local Lean 4 is insufficient).