elan default install broken by removal of 'stable' toolchain

Stream: general

[Jannis Limperg]

When I run the elan install script and select the default installation, I get the following output:

info: downloading installer

Welcome to Lean!

This will download and install Elan, a tool for managing different Lean
versions used in packages you create or download. It will also install a
default version of Lean and its package manager, leanpkg, for editing files not
belonging to any package.

It will add the leanpkg, lean, and elan commands to Elan's bin directory,
located at:

  /home/jannis/.elan/bin

This path will then be added to your PATH environment variable by modifying the
profile file located at:

  /home/jannis/.profile

You can uninstall at any time with elan self uninstall and these changes will
be reverted.

Current installation options:

     default toolchain: stable
  modify PATH variable: yes

1) Proceed with installation (default)
2) Customize installation
3) Cancel installation


info: syncing channel updates for 'stable'
info: latest update on stable, lean version drop
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: None })
error: could not download nonexistent lean version `stable`
info: caused by: could not download file from 'https://github.com/leanprover-community/lean/releases/tag/drop' to '/home/jannis/.elan/tmp/wjh41qwqk8hh4pps_file'
info: caused by: http request returned an unsuccessful status code: 404

I guess the stable toolchain isn't a thing any more? If this is intentional, elan should be updated to avoid this error.

[Johan Commelin]

@Sebastian Ullrich :up:

[Bryan Gin-ge Chen]

I don't think we did anything to remove the stable toolchain recently. My wild guess is that elan might not be dealing with the recent custom "dropDLO" release properly.

[Sebastian Ullrich]

Yeah, that's definitely not a release name elan excepts...

[Jannis Limperg]

Aha! That'll be the culprit.

[Jannis Limperg]

Would it help if this release were demoted to a mere tag?

[Bryan Gin-ge Chen]

I think we can delete this release; if @Yury G. Kudryashov needs it again he can re-create it (temporarily).

[Bryan Gin-ge Chen]

@Jannis Limperg see if elan works now?

[Gabriel Ebner]

@Yury G. Kudryashov You can also push to a tag on your own fork.

[Jannis Limperg]

Yes, elan default install works again. Thanks a lot!

[Yury G. Kudryashov]

Sorry, I didn't mean to break elan.

[Yury G. Kudryashov]

What should I do? Push some tag to my fork? What names elan will accept?

[Yury G. Kudryashov]

My goal is to use this version of lean in the CI for https://github.com/leanprover-community/mathlib/tree/drop-DLO

[Jannis Limperg]

Do you need the CI? Perhaps you could build the dropDLO Lean tag locally and use it to build mathlib.

[Yury G. Kudryashov]

I was going to ask for help from other people, and this would be much easier if it worked withelan.

[Bryan Gin-ge Chen]

@Yury G. Kudryashov I think you can push a dropDLO tag to your fork (with GitHub actions enabled) and then change this line to urkud/lean:dropDLO.

[Bryan Gin-ge Chen]

Not 100% sure though, I haven't tried this myself before.

[Yury G. Kudryashov]

I'll try it.