Trouble installing Lean4 on Ubuntu

Stream: lean4

[Hanting Zhang]

For some reason I'm having some trouble installing Lean4 on a new Ubuntu machine (22.04).

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
info: downloading installer
info: default toolchain set to 'stable'
info: uninstalling toolchain '/home/paperspace/.elan/toolchains/stable' using obsolete format
$ elan toolchain install leanprover/lean4:stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.15.0
info: downloading component 'lean'
error: binary package was not provided for 'linux'

I don't know why it says it can't find the binary package for linux. I tried downloading the tarball directly, but then elan yells at me more. I'm kinda lost on what to do next. How can I fix this? Thanks!

[Ruben Van de Velde]

Works here

[Sebastian Ullrich]

@Hanting Zhang What does which elan, elan --version say?

[Hanting Zhang]

Huh, I ran sudo apt upgrade and now everything works again. Not sure why, but sorry for the noise!

[Sebastian Ullrich]

Do you somehow have multiple versions of elan installed? You should still fix that

[Hanting Zhang]

No, I don't think so? It looks fine:

$ elan --version
elan 4.0.0 (bb75b50d2 2025-01-30)
$ which elan
/home/hantingz/.elan/bin/elan

[Julian Berman]

How about type -a elan?

[Hanting Zhang]

Oh, hmm

$ type -a elan
elan is /home/hanting/.elan/bin/elan
elan is /usr/bin/elan
elan is /bin/elan

I suppose I should delete the 2nd and 3rd ones?

[Sebastian Ullrich]

Yes I think that's a bit too much elan

[Kevin Buzzard]

Did you install lean via some kind of package, out of interest? At least a while ago the community were trying to eliminate lean packages in Linux repositories for exactly this sort of reason (you get stuck with old versions of software which sometimes aren't supported any more for example)

[Hanting Zhang]

Yes, I think I tried sudo apt install elan at some point... that might have caused issues, although I don't see how. As long as the path defaults to the first elan the 2nd and 3rd shouldn't matter. Maybe updating fixed the paths or something?

[Mauricio Collares]

I wonder what caused it to be installed to /bin! I know some weird distros symlink /bin to /usr/bin, but I thought Debian wasn't one of them.

Edit: Apparently I was wrong, https://wiki.debian.org/UsrMerge was completed a while ago.

[Mauricio Collares]

Hanting Zhang said:

Yes, I think I tried sudo apt install elan at some point... that might have caused issues, although I don't see how. As long as the path defaults to the first elan the 2nd and 3rd shouldn't matter. Maybe updating fixed the paths or something?

You probably didn't restart your shell/terminal after installing elan via curl, and therefore /home/hanting/.elan/ wasn't yet in PATH.

[Sebastian Ullrich]

Which the installation will tell you unless you pass -y to it as you did for some reason