musl binaries

Stream: lean4

[Stefano Volpe]

Lean4 only releases glibc binaries. No musl binaries. @Sebastian Ullrich suggested opening a new (low priority) issue. Anybody else on a musl distribution?

[Stefano Volpe]

Relevant issue: https://github.com/leanprover/lean4/issues/2931

[Bulhwi Cha]

I'm thinking of installing Alpine Linux on an old laptop when I can find time.

[Stefano Volpe]

my daily driver has been alpine for almost one year now. Love it! I was on void linux before

[Sofia Snow]

I also use Alpine. Removing the check for musl from the elan setup script, it successfully installs the glibc version. With gcompat installed, I can run lake and lean just fine. However, lake new fails with

error: could not detect the configuration of the Lake installation

[Sofia Snow]

I'd rather musl builds of course, but gcompat should probably just work here.

[Sofia Snow]

https://wiki.alpinelinux.org/wiki/Running_glibc_programs

[Sofia Snow]

https://git.adelielinux.org/adelie/gcompat

[Sofia Snow]

In the meantime I'm probably going to just use an archlinux user-mode chroot with bubblewrap.

[Stefano Volpe]

So, I am the author of the PR adding the musl check to the elan setup script. Gcompat did not work properly for me back in the days. What I did was compiling lean from source. I consider gcompat to be a hack anyway

[Stefano Volpe]

It makes sense to me to check for a gcompat installation if people are able to properly use it to run lean's glibc binaries (I am not)