elan is broken?

Stream: general

[Scott Morrison]

Trying to fix the elan installation in the VS Code extension, I've discovered that elan itself is currently not working. Lo:

$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
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:

  /Users/scott/.elan/bin

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

  /Users/scott/.profile
  /Users/scott/.bash_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 v3.4.2","user_id":null}}
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/lean/releases/tag/v3.4.2","user_id":null%7D%7D' to '/Users/scott/.elan/tmp/5dut6cfxwij0ymb0_file'
info: caused by: http request returned an unsuccessful status code: 404

Any ideas, @Sebastian Ullrich?

[Scott Morrison]

Could anyone else (on OSX or otherwise) let me know if they are seeing similar behaviour?

[Sebastian Ullrich]

Hmm, parsing Github HTML to retrieve the latest release might not be the most stable solution in retrospect

[Keeley Hoek]

I have a 2-line fix which uses the github api pull requested :)

[Keeley Hoek]

(Who needs a JSON parser anyway ;) )

[Sebastian Ullrich]

That's what I did at first, until we ran into Github API's rate limits

[Scott Morrison]

merge in 3... 2... 1... :-)

[Scott Morrison]

ah...

[Keeley Hoek]

:-(

[Keeley Hoek]

Well, you could always just put an ampersand after the " in the regex lol

[Sebastian Ullrich]

I'm parsing the Location: header now

[Sebastian Ullrich]

That's the plan at least

[Keeley Hoek]

Like HTTP header? From where?

[Keeley Hoek]

But cool, sounds more legit

[Sebastian Ullrich]

Done. Since elan's self-updater is broken as well, please reinstall elan via e.g.

curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh

[Johan Commelin]

@Sebastian Ullrich Is that a message for everyone?

[Sebastian Ullrich]

@Johan Commelin Yes. Should we make it more prominent in a new all-caps topic or something?

[Johan Commelin]

Yes, and maybe this is one of those cases where you could use a global mention

[Johan Commelin]

Using @everyone

[Sebastian Ullrich]

I don't know, sending notifications to 523 people seems kind of rude :) . If they notice something's wrong, I hope they'll find the Zulip topic by themselves.

[Johan Commelin]

It depends on the fraction of people that we think will find this message helpful.

[Johan Commelin]

I don't have a good estimate for the number of elan users out there. But I guess it might be >50%

[Sebastian Ullrich]

At least of the active users. There may be inactive users with e-mail notifications, though I don't think that is the default.

[Bryan Gin-ge Chen]

I'm getting errors from the nightly toolchain after the update. elan update gives me:

info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.4.2
info: syncing channel updates for 'nightly'
error: failed to resolve latest version of 'nightly'
info: checking for self-updates

       stable unchanged - Lean (version 3.4.2, commit cbd2b6686ddb, Release)
  nightly update failed - Lean (version 3.4.2, nightly-2019-01-13, commit 95fa4cfb0a87, Release)

Running elan toolchain install nightly gives me:

info: syncing channel updates for 'nightly'
error: failed to resolve latest version of 'nightly'
info: caused by: failed to parse latest release tag

Granted, this isn't a big deal for me personally since nightly hasn't changed since I last updated it.

[Kevin Buzzard]

Can you confirm that you followed the instructions at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ELAN.20IS.20BROKEN.20(AND.20FIXED) already?

[Bryan Gin-ge Chen]

Yes, that's what I meant by "after the update".

[Kevin Buzzard]

Oh of course. Did you do the "source" bit at the end?

[Kevin Buzzard]

and then try updating from the same window etc?

[Bryan Gin-ge Chen]

I didn't think I had to since I already had elan in my path, but I just did it and I got the same results.

[Kevin Buzzard]

Yes, I guess all it does is changes the path. Then I can't help, sorry; it works for me on Ubuntu. what OS are you using?

[Bryan Gin-ge Chen]

I'm on macOS.

[Kevin Buzzard]

$ elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.4.2
info: checking for self-updates

  stable unchanged - Lean (version 3.4.2, commit cbd2b6686ddb, Release)

buzzard@bob:~/Encfs/Computer_languages/Lean/lean-projects/mathlib-community-master$

[Bryan Gin-ge Chen]

Right, I have no problems with the "stable" toolchain. Could you try elan toolchain install nightly ?

[Kevin Buzzard]

$ elan toolchain install nightly
info: syncing channel updates for 'nightly'
error: failed to resolve latest version of 'nightly'
info: caused by: failed to parse latest release tag
buzzard@bob:~/Encfs/Computer_languages/Lean/lean-projects/mathlib-community-master$

Aah so I can reproduce your error for the nightly install. I've never typed that before though.

[Sebastian Ullrich]

I only tested the stable toolchain :cry:

[Patrick Massot]

But currently nightly = stable, right?

[Bryan Gin-ge Chen]

I believe they differ, but only in the version string. However, it's possible that the underlying issue affects the usage of other versions of Lean in elan as well (have not checked).

[Sebastian Ullrich]

Okay, I went back to the hackish code...