elan installation 404

Stream: general

[Shing Tak Lam]

It seems like right a few PRs in staging are failing their builds, since there is a 404 when installing elan

Examples:

• https://github.com/leanprover-community/mathlib/runs/2369859882
• https://github.com/leanprover-community/mathlib/runs/2369854866

Run set -o pipefail
  set -o pipefail
  curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
  ~/.elan/bin/lean --version
  echo "$HOME/.elan/bin" >> $GITHUB_PATH
  shell: /usr/bin/bash -e {0}
info: downloading installer
curl: (22) The requested URL returned error: 404
elan: command failed: curl -sSfL https://github.com/Kha/elan/releases/download/latest/elan-x86_64-unknown-linux-gnu.tar.gz -o /tmp/tmp.LotzRWUxTN/elan-init.tar.gz
Error: Process completed with exit code 1.

[Bryan Gin-ge Chen]

This is probably related to the fact that elan moved to the leanprover organization. I haven't figured out what the fix should be yet though.

cc: @Sebastian Ullrich

[Bryan Gin-ge Chen]

FWIW, elan self update from an older version didn't work for me on macOS:

$ elan self update
info: checking for self-updates
info: downloading self-update
error: failed to set permissions for '/Users/chb/.elan/bin/elan-init'
info: caused by: No such file or directory (os error 2)

However, reinstalling with curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh did work.

[Bryan Gin-ge Chen]

#7324 should hopefully fix things in mathlib. I'll go through the other repos and see what else needs updating.

[Sebastian Ullrich]

This should have only been an intermittent issue, all URLs seem to be forwarded properly now

[Yaël Dillies]

We seem to have that problem again. 5 of my builds recently failed because of that.

[Sebastian Ullrich]

This time we didn't change anything on our side

[Bryan Gin-ge Chen]

@Yaël Dillies can you link to some of the build logs?

[Yaël Dillies]

Here: https://github.com/leanprover-community/mathlib/runs/4456647696?check_suite_focus=true

[Yaël Dillies]

Sorry, should have probably changed to thread "elan installation 503" :grinning:

[Sebastian Ullrich]

Looks like a GitHub hiccup

[Gabriel Ebner]

It's been going on for a few days, and not just with elan. We've been seeing 503 Egress is over the account limit errors repeatedly.

[Chris Lovett]

Github did go down for about an hour last weekend.

[Gabriel Ebner]

Found the github issue: https://github.com/github/feedback/discussions/8535 Seems to have been resolved two days ago.