Zulip Chat Archive

Stream: general

Topic: binary package was not provided for 'linux'


Gabriel Ebner (Sep 12 2022 at 14:22):

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 (Sep 12 2022 at 14:53):

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 (Sep 12 2022 at 14:59):

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

Gabriel Ebner (Sep 12 2022 at 15:57):

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

John Burnham (Sep 12 2022 at 16:26):

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 (Sep 12 2022 at 16:33):

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 (Sep 12 2022 at 16:34):

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

Sebastian Ullrich (Sep 12 2022 at 16:36):

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

Mauricio Collares (Sep 12 2022 at 17:01):

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 (Sep 12 2022 at 17:02):

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

Mauricio Collares (Sep 12 2022 at 17:05):

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 (Sep 12 2022 at 17:06):

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 (Sep 12 2022 at 17:14):

Uh oh.

Gabriel Ebner (Sep 12 2022 at 17:29):

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

Chris Lovett (Sep 12 2022 at 17:58):

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

Johan Commelin (Sep 13 2022 at 13:16):

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 (Sep 13 2022 at 13:22):

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

Mauricio Collares (Sep 13 2022 at 13:23):

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 (Sep 13 2022 at 13:25):

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 (Sep 13 2022 at 13:29):

That's evil, right?

Johan Commelin (Sep 13 2022 at 13:29):

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

Mauricio Collares (Sep 13 2022 at 13:30):

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 (Sep 13 2022 at 13:31):

But vscode will not know about that elan.

Johan Commelin (Sep 13 2022 at 13:31):

Maybe I should just wait for a day.

Johan Commelin (Sep 13 2022 at 13:31):

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

Gabriel Ebner (Sep 13 2022 at 13:31):

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 (Sep 14 2022 at 09:03):

/me is very confused

Johan Commelin (Sep 14 2022 at 09:03):

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 (Sep 14 2022 at 09:04):

Any idea where that error can come from?

Gabriel Ebner (Sep 14 2022 at 09:35):

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 (Sep 14 2022 at 09:35):

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

Johan Commelin (Sep 14 2022 at 09:36):

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

Gabriel Ebner (Sep 14 2022 at 09:39):

What does ldd (elan which lean) say?

Johan Commelin (Sep 19 2022 at 07:22):

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

Anne Baanen (Sep 19 2022 at 07:23):

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

Johan Commelin (Sep 19 2022 at 07:38):

Aah, makes sense

Johan Commelin (Sep 19 2022 at 07:38):

❯ 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 (Sep 19 2022 at 07:50):

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

Johan Commelin (Sep 19 2022 at 07:51):

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

Johan Commelin (Sep 19 2022 at 07:52):

❯ 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 (Sep 19 2022 at 16:23):

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 (Sep 19 2022 at 16:41):

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 (Sep 19 2022 at 16:43):

(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 (Sep 19 2022 at 17:10):

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

Chris Lovett (Sep 19 2022 at 20:07):

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

Eric Wieser (Sep 19 2022 at 20:12):

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 (Sep 25 2022 at 12:38):

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

Eric Wieser (Sep 25 2022 at 13:36):

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

Bernd Losert (Sep 25 2022 at 13:59):

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 (Sep 25 2022 at 14:09):

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 (Sep 25 2022 at 15:16):

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


Last updated: Dec 20 2023 at 11:08 UTC