Zulip Chat Archive

Stream: general

Topic: Elan temporarily broken

Gabriel Ebner (Oct 19 2021 at 12:52):

Just a heads-up: I've added an aarch64 build to the latest lean release. Apparently elan downloads that even if an x86_64 build is available. Therefore you can't install 3.33.0 using elan at the moment. Sebastian has already fixed this on master.

@Sebastian Ullrich Can you make a new release please? Or should we change the naming scheme to lean-3.33.0-aarch64-linux.tar.gz so that we don't break old elan versions?

Gabriel Ebner (Oct 19 2021 at 12:53):

Pulled the aarch64 build for now.

Sebastian Ullrich (Oct 19 2021 at 12:55):

Ok, I've cancelled the release

Gabriel Ebner (Oct 19 2021 at 12:55):

https://github.com/leanprover/elan/pull/51

Gabriel Ebner (Oct 19 2021 at 13:03):

And apparently I've broken elan again... Do you want to fix it or should I submit another one liner?

Sebastian Ullrich (Oct 19 2021 at 13:09):

I fixed it, I think

Sebastian Ullrich (Oct 19 2021 at 13:15):

Wait... I think the fix made it worse. Now not even linux.tar.gz is unique.

Gabriel Ebner (Oct 19 2021 at 13:19):

Ah, I see. The old idea was to check if the release tarball contains linux, now we're checking for linux.tar.gz.

Gabriel Ebner (Oct 19 2021 at 13:20):

So there is no way to add new architectures without breaking old elan versions or calling it penguin-aarch64....

Sebastian Ullrich (Oct 19 2021 at 13:29):

Yeah, there is no good solution here

Gabriel Ebner (Oct 19 2021 at 13:32):

Yes, I can only see these two solutions:

  1. Break old elan installations in a cryptic and hard-to-recover way.
  2. Use lin-aarch64 and mac-aarch64 for the new architecture names.

Sebastian Ullrich (Oct 19 2021 at 13:40):

Any weird name that makes them be listed after the existing downloads would also work

Sebastian Ullrich (Oct 19 2021 at 13:41):

linux_aarch64 might work

Gabriel Ebner (Oct 19 2021 at 13:42):

That will still match against linux, wouldn't it?

Gabriel Ebner (Oct 19 2021 at 13:42):

Ah, you mean github sorts the filenames and elan picks the first match? Hmmm.

Gabriel Ebner (Oct 19 2021 at 13:44):

Indeed, that works!

Johan Commelin (Oct 19 2021 at 14:17):

I predict that 37 weeks from now, github changes their LOCALE, and hence the way these files are sorted.

Sebastian Ullrich (Oct 19 2021 at 14:22):

Hey, our HTML parsing code has otherwise been working for over three years

Gabriel Ebner (Oct 19 2021 at 14:22):

37 weeks from now everybody will have hopefully upgraded their elan though.

Johan Commelin (Oct 19 2021 at 14:23):

elan tends to be among those things that I only update once every 37 months... it just works silently in the background (-;

Sebastian Ullrich (Oct 19 2021 at 14:23):

I've updated elan and will do a release wehn everything looks good

Johan Commelin (Oct 19 2021 at 14:24):

Anyway, I'm not to worried about this breakage. We just need to remember that if someone pops in with a cryptic and hard-to-recover error, that we point them to this thread.

Gabriel Ebner (Oct 19 2021 at 14:24):

If you're on nixos, there's an elan package.

Johan Commelin (Oct 19 2021 at 14:24):

Unfortunately not all my boxes are on nixos yet.

Gabriel Ebner (Oct 19 2021 at 14:27):

Sebastian Ullrich said:

I've updated elan and will do a release wehn everything looks good

I see, you've decided to rewrite history and remove today. :smile:

Sebastian Ullrich (Oct 19 2021 at 14:30):

waves hand These aren't the commits you're looking for

Sebastian Ullrich (Oct 19 2021 at 14:35):

Ah, I didn't see your PR until now

Gabriel Ebner (Oct 19 2021 at 15:05):

Lean 3 PR is up: https://github.com/leanprover-community/lean/pull/630

Last updated: Dec 20 2023 at 11:08 UTC