`elan toolchain list` refuses to list any toolchains

[eric-wieser]

See this shell session:

$ elan toolchain list
leanprover/lean4:v4.13.0-rc3
leanprover/lean4:v4.8.0-rc2
$ elan toolchain link oh--no--anyway ~/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/
$ elan toolchain list
error: invalid toolchain name: 'oh/no/anyway'

Some motivation for this weird elan toolchain link command; I need a way to smuggle arbitrary paths into toolchain names, and was previously encoding path/to/my/toolchain as path--to--my--toolchain, since / characters are not legal.

This all works correctly when actually running lean and lake, but elan toolchain list fails.

[eric-wieser]

@Kha, do you have any opinions here? It's annoying to be able to use toolchains but not list them (for debugging)

[Kha]

Oof. I'd accept a pull request but this is really quite out there...

[Kha]

Would this be covered by "allow lean-toolchain to directly point to a toolchain path"?

[eric-wieser]

My actual setup is:

• I have one global toolchain at the/global/toolchain
• I link this toolchain under various names as elan link "some--encoded---name" the/global/toolchain
• The script at the/global/toolchain/lean inspects a combination of the path it was invoked through (in this case some--encoded---name, which is encoded from some/encoded:name), and the working directory, and performs some internal logic with this data to:
  • locate the actual lean to invoke.
  • set some extra environment variables

The smallest change that would work for me is to make the regex that matches foo/bar:version a little sloppy so that it also matches foo/bar/baz:version.

A slightly more principled change would be to allow elan link to use arbitrary toolchain names, and distinguish between local toolchains (with freeform naming) and github ones (With the current naming)

[eric-wieser]

If #159 is too much, I could work around this by using an even more stupid encoding like sending foo-bar/baz:version to foo-2D-bar-2F-baz-3A-version instead of foo-bar--baz---version, but I'd prefer not to!

[eric-wieser]

@Kha, any more thoughts on this?