Zulip Chat Archive

Stream: general

Topic: elan is broken?


Scott Morrison (Mar 20 2019 at 09:38):

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 (Mar 20 2019 at 09:39):

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

Sebastian Ullrich (Mar 20 2019 at 09:51):

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

Keeley Hoek (Mar 20 2019 at 09:58):

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

Keeley Hoek (Mar 20 2019 at 09:59):

(Who needs a JSON parser anyway ;) )

Sebastian Ullrich (Mar 20 2019 at 10:02):

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

Scott Morrison (Mar 20 2019 at 10:02):

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

Scott Morrison (Mar 20 2019 at 10:02):

ah...

Keeley Hoek (Mar 20 2019 at 10:03):

:-(

Keeley Hoek (Mar 20 2019 at 10:04):

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

Sebastian Ullrich (Mar 20 2019 at 10:04):

I'm parsing the Location: header now

Sebastian Ullrich (Mar 20 2019 at 10:05):

That's the plan at least

Keeley Hoek (Mar 20 2019 at 10:06):

Like HTTP header? From where?

Keeley Hoek (Mar 20 2019 at 10:07):

But cool, sounds more legit

Sebastian Ullrich (Mar 20 2019 at 11:37):

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 (Mar 20 2019 at 11:56):

@Sebastian Ullrich Is that a message for everyone?

Sebastian Ullrich (Mar 20 2019 at 12:01):

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

Johan Commelin (Mar 20 2019 at 12:02):

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

Johan Commelin (Mar 20 2019 at 12:02):

Using @everyone

Sebastian Ullrich (Mar 20 2019 at 12:06):

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 (Mar 20 2019 at 12:06):

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

Johan Commelin (Mar 20 2019 at 12:07):

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

Sebastian Ullrich (Mar 20 2019 at 12:14):

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 (Mar 20 2019 at 14:14):

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 (Mar 20 2019 at 14:15):

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 (Mar 20 2019 at 14:16):

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

Kevin Buzzard (Mar 20 2019 at 14:16):

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

Kevin Buzzard (Mar 20 2019 at 14:16):

and then try updating from the same window etc?

Bryan Gin-ge Chen (Mar 20 2019 at 14:17):

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 (Mar 20 2019 at 14:18):

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 (Mar 20 2019 at 14:19):

I'm on macOS.

Kevin Buzzard (Mar 20 2019 at 14:19):

$ 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 (Mar 20 2019 at 14:19):

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

Kevin Buzzard (Mar 20 2019 at 14:19):

$ 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 (Mar 20 2019 at 14:52):

I only tested the stable toolchain :cry:

Patrick Massot (Mar 20 2019 at 18:01):

But currently nightly = stable, right?

Bryan Gin-ge Chen (Mar 20 2019 at 18:29):

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 (Mar 21 2019 at 12:22):

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


Last updated: Dec 20 2023 at 11:08 UTC