search

leanprover / elan

The Lean version manager
Apache License 2.0
310 stars 35 forks source link

`stable installed - (error reading lean version)` #114

Closed foxyseta closed 10 months ago

foxyseta commented 11 months ago 
$ elan self update  # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.2.0
info: downloading component 'lean'
179.7 MiB / 179.7 MiB (100 %)   1.6 MiB/s ETA:   0 sKk^[[
info: installing component 'lean'
info: default toolchain set to 'leanprover/lean4:stable'

leanprover/lean4:stable installed - (error reading lean version)
$ lean
error: command failed: 'lean'
info: caused by: No such file or directory (os error 2)
$ which lean
/home/foxy/.elan/bin/lean

I am unable to install any Lean toolchain on Alpine Linux.

foxyseta commented 11 months ago

I forgot to mention: the executables can be found on my disk, and are executable. So maybe it's because I am on a musl distribution?

Kha commented 11 months ago

Indeed, we only have releases for glibc: https://lean-lang.org/lean4/doc/setup.html#supported-platforms

foxyseta commented 11 months ago

Oh wow. I even went through that doc page twice before and failed to notice that. My apologies! I believe elan should raise an error then?

OT: is there any issue tracking musl support? Is that planned?

Kha commented 11 months ago

Yes, this would have to be detected in https://github.com/leanprover/elan/blob/master/elan-init.sh.

I don't think musl support was requested before and it would not be high priority but opening an issue at leanprover/lean4 doesn't hurt.

foxyseta commented 11 months ago

Yes, this would have to be detected in https://github.com/leanprover/elan/blob/master/elan-init.sh.

Shall I open a PR? One could look for GLIBC in the first line of the output of ldd --version to check this. Should this happen as soon as we realize we are on a Linux system?

I don't think musl support was requested before and it would not be high priority but opening an issue at leanprover/lean4 doesn't hurt.

Opened https://github.com/leanprover/lean4/issues/2931.

Kha commented 10 months ago

Yes, PRs welcome. But could you first check what upstream rustup does and copy that if applicable?

foxyseta commented 10 months ago

Opened relevant PR. As requested, It is based on the upstream rustup code.