elan on alpine

Stream: lean4

[Patrick Massot]

Working on CI setup for Lean blueprints I noticed a small issue. Many docker images are based on the minimalist Alpine Linux distribution. But elan refuses to install there. It simply says nope to musl. In particular it is hard to find a docker image containing a full texlive and where installing Lean would be easy. This is really low priority, but I thought I’d mention it in case this is a historical accident that would now be easy to “fix”. @Sebastian Ullrich

[Sebastian Ullrich]

Last time someone tried to build Lean 4 on musl, it didn't work I believe. And even if it worked, we would still have to spend resources on actually providing releases for it.

[Patrick Massot]

Ok, it is very probably not worth the trouble then.