binary package was not provided for 'linux'

Stream: general

[Gabriel Ebner]

I've just had a few CI runs fail due to this elan error:

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
$ source ~/.elan/env
$ lean +leanprover/lean4:nightly-2022-09-12
info: downloading component 'lean'
error: binary package was not provided for 'linux'

Has anybody else run into this error as well?

[Jannis Limperg]

A student of mine also had this issue earlier, but with Windows and manual lake build. Both nightly-2022-09-11 and nightly-2022-09-07 (I think).

[Gabriel Ebner]

I'm also getting 500 errors on github itself, so maybe this is just a general outage.

[Gabriel Ebner]

Mmmh, this is strange. I'm still getting the errors, but Lean 3 releases seem to be completely unaffected.

[John Burnham]

I've run into the same issue for recent nightly:

λ elan update
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2022-09-12
info: downloading component 'lean'
error: binary package was not provided for 'linux'
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.0.0-m5
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2020-01-15
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.4.2

  leanprover/lean4:nightly update failed - Lean (version 4.0.0-nightly-2022-09-11, commit 1749210a4b39, Release)
       leanprover/lean4:stable unchanged - Lean (version 4.0.0, commit 7dbfaf9b7519, Release)
       leanprover/lean:nightly unchanged - Lean (version 3.4.2, nightly-2020-01-15, commit 72a965986fa5, Release)
        leanprover/lean:stable unchanged - Lean (version 3.4.2, commit cbd2b6686ddb, Release)

[John Burnham]

I think it's a github outage based on twitter and https://downdetector.com/status/github/ reports, but what's strange is that I can manually download from https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-09-12

[Gabriel Ebner]

cc @Sebastian Ullrich In case you haven't seen it already.

[Sebastian Ullrich]

My hopes are on "outage". Wouldn't be the first time.

[Mauricio Collares]

I don't think this is an outage issue. The GitHub page now seems to load the asset list lazily (grep https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-09-08 's source for https://github.com/leanprover/lean4-nightly/releases/expanded_assets/nightly-2022-09-08 to see what I mean). Perhaps this only happens after a certain number of assets?

[Gabriel Ebner]

Can you check https://github.com/leanprover-community/lean/releases? Is it loaded non-lazily?

[Mauricio Collares]

Yes, if you wget the lean 3 releases page you can see the tarball URLs, but https://github.com/leanprover/lean4-nightly/releases only has a bunch of https://github.com/leanprover/lean4-nightly/releases/expanded_assets-starting links

[Mauricio Collares]

You can even see this in-browser: One asset list is collapsed by default while the other is not.

Edit: Never mind, the interface change is not a good indicator. Old Lean 3 releases have collapsed assets which are not lazy-loaded. But the Lean 4 assets all seem to be lazily loaded.

[Gabriel Ebner]

Uh oh.

[Gabriel Ebner]

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

[Chris Lovett]

Time to create a Lean version of elan using gh CLI ?

• gh release list -R https://github.com/leanprover/lean4-nightly/
• gh release download nightly-2022-09-12 -R https://github.com/leanprover/lean4-nightly/ -p *-linux.tar.zst

[Johan Commelin]

The corresponding PR to nixpkgs was merged 4 hours ago. I just ran nix-channel --update and rebuilt my system. But I'm still stuck with elan 1.4.1. Why is nix letting me down?

[Gabriel Ebner]

https://status.nixos.org/ Last nixos-unstable channel update was a day ago.

[Mauricio Collares]

https://nixpk.gs/pr-tracker.html?pr=191035 is useful too (https://nixpk.gs/pr-tracker.html?pr=191039 if you're on 22.05)

[Gabriel Ebner]

You can use a bit of mutable state in the meantime:

nix-env -f https://github.com/nixos/nixpkgs/archive/master.zip -iA elan

[Johan Commelin]

That's evil, right?

[Johan Commelin]

Can nix tell me about all the mutable state that I've used in the past, so that I can undo it?

[Mauricio Collares]

You can also do nix-shell -I nixpkgs=https://github.com/nixos/nixpkgs/archive/master.zip -p elan to get a temporary shell with the newest elan. No mutable state, but slightly less convenient.

[Johan Commelin]

But vscode will not know about that elan.

[Johan Commelin]

Maybe I should just wait for a day.

[Johan Commelin]

Can't I instruct nix-channel --update to really give me actual unstable?

[Gabriel Ebner]

You can do nix-env -q to see all of the mutable "overrides". And then use nix-env -e elan to get rid of it again.

[Johan Commelin]

/me is very confused

[Johan Commelin]

❯ cd ../mathlib

mathlib on  refactor-wlog
❯ elan show
installed toolchains
--------------------

leanprover-community/lean:3.35.0
leanprover-community/lean:3.42.0
leanprover-community/lean:3.42.1
leanprover-community/lean:3.44.1
leanprover-community/lean:3.45.0
leanprover-community/lean:3.47.0
leanprover-community/lean:3.48.0
leanprover/lean4:nightly-2022-09-11 (default)
leanprover/lean4:nightly-2022-09-12
leanprover/lean4:nightly-2022-09-13

active toolchain
----------------

leanprover-community/lean:3.48.0 (overridden by '/home/jmc/repos/mathlib/leanpkg.toml')
Lean (version 3.48.0, commit 283f6ed8083a, Release)


mathlib on  refactor-wlog
❯ lean --version
Lean (version 3.48.0, commit 283f6ed8083a, Release)

mathlib on  refactor-wlog
❯ cd ../mathlib4

mathlib4 on  master [?]
❯ elan show
installed toolchains
--------------------

leanprover-community/lean:3.35.0
leanprover-community/lean:3.42.0
leanprover-community/lean:3.42.1
leanprover-community/lean:3.44.1
leanprover-community/lean:3.45.0
leanprover-community/lean:3.47.0
leanprover-community/lean:3.48.0
leanprover/lean4:nightly-2022-09-11 (default)
leanprover/lean4:nightly-2022-09-12
leanprover/lean4:nightly-2022-09-13

active toolchain
----------------

leanprover/lean4:nightly-2022-09-11 (overridden by '/home/jmc/repos/mathlib4/lean-toolchain')
(error reading lean version)


mathlib4 on  master [?]
❯ lean --version
error: command failed: 'lean'
info: caused by: No such file or directory (os error 2)

[Johan Commelin]

Any idea where that error can come from?

[Gabriel Ebner]

That's because we use patchelf+makeWrapper to make the lean4 builds work on nixos. As a result, they depend on the stdenv used in elan. So if you run the garbage collector, old downloads will stop working.

[Gabriel Ebner]

Just run elan uninstall leanprover/lean4:nightly-2022-09-11

[Johan Commelin]

But it was only downloaded this morning, and I didn't gc after that

[Gabriel Ebner]

What does ldd (elan which lean) say?

[Johan Commelin]

❯ ldd (elan which lean)
zsh: missing end of string

[Anne Baanen]

I assume it should be ldd $(elan which lean), i.e. antiquotation.

[Johan Commelin]

Aah, makes sense

[Johan Commelin]

❯ ldd $(elan which lean)
        linux-vdso.so.1 (0x00007fff865e6000)
        libleanshared.so => /home/jmc/.elan/toolchains/leanprover--lean4---nightly-2022-09-15/bin/../lib/lean/libleanshared.so (0x00007fb628911000)
        libdl.so.2 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libdl.so.2 (0x00007fb62890c000)
        libpthread.so.0 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libpthread.so.0 (0x00007fb6288ec000)
        libc.so.6 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libc.so.6 (0x00007fb628717000)
        libm.so.6 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/libm.so.6 (0x00007fb6285d6000)
        librt.so.1 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib/librt.so.1 (0x00007fb6285c9000)
        /lib64/ld-linux-x86-64.so.2 => /nix/store/q29bwjibv9gi9n86203s38n0577w09sx-glibc-2.33-117/lib64/ld-linux-x86-64.so.2 (0x00007fb62bb79000)

[Sebastian Ullrich]

That's a different nightly (2022-09-15) from before, do both of them fail to execute?

[Johan Commelin]

I removed the 2022-09-11 version. That one is now also broken :sad:

[Johan Commelin]

❯ elan run leanprover/lean4:nightly-2022-09-11 lean --version
error: command failed: 'lean'
info: caused by: No such file or directory (os error 2)

❯ elan run leanprover/lean4:nightly-2022-09-12 lean --version
Lean (version 4.0.0-nightly-2022-09-12, commit ec2372e8d4ca, Release)

[Junyan Xu]

Gitpod is unusable in recent mathlib(3) PRs due to this problem. What else should be done to fix it now that https://github.com/leanprover/elan/pull/83 has been merged?

[Mauricio Collares]

A Docker image probably needs to be rebuilt, but in the meantime you can run elan self update inside the Gitpod VS Code terminal

[Mauricio Collares]

(and then click on any error message buttons that showed up when you opened Gitpod, such as Run leanpkg configure and Restart lean)

[Eric Wieser]

@Scott Morrison, are you able to rebuild the docker images? I think only you have permission to publish them

[Chris Lovett]

I just tried this gitpod (https://gitpod.io/#https://github.com/leanprover/lean4-samples) and it worked fine:
image.png

[Eric Wieser]

I think it's just the lean3 docker containers that are the issue, as they're hosted elsewhere rather than rebuild by gitpod

[Bernd Losert]

I use gitpod and I'm also having this problem with my lean3 project. It is unusable now.

[Eric Wieser]

See the advice above, elan self update makes it usable again

[Bernd Losert]

I tried that. Didn't work. I had installed lean in my gitpod using brew. I tried the curl script to see if there is any difference. I got further, but now I'm getting hundreds of errors of the form "invalid object declaration" and "excessive memory consumption detected".

[Mauricio Collares]

www.gitpodstatus.com says "In eu68 and us68 clusters, we have diagnosed issues that cause git push and loading of dotfiles to fail. We've ceased the traffic shift to eu68 and us68, please stop running workspaces on those clusters, restart your workspaces, and they'll land on eu67 and us67. We're currently investigating the issue, and will provide an update soon."

[Bernd Losert]

Loading of dotfiles seems to be the problem for me at the moment - it won't load .profile.