musl-based elan

Stream: general

[Bhavik Mehta]

I just tried to open a PR in codespaces, and the lean extension trying to install elan gave this error:

codespaces-8ed4d0:/workspaces/mathlib4$ bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:stable || (echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")' && exit
elan: musl-based systems are unsupported at the moment

I don't think I have anything other than default codespace settings, so I don't really understand why this no longer works

[Henrik Böving]

Does your codespace happen to be an alpine container?

[Bhavik Mehta]

I don't know what that means, I just pressed the codespaces button and I know it's called ominous potato

[Henrik Böving]

What does cat /etc/os-release give you?

[Bhavik Mehta]

NAME="Alpine Linux"
ID=alpine
VERSION_ID=3.21.3
PRETTY_NAME="Alpine Linux v3.21"
HOME_URL="https://alpinelinux.org/"
BUG_REPORT_URL="https://gitlab.alpinelinux.org/alpine/aports/-/issues"

[Bhavik Mehta]

So seemingly it is an alpine container!

[Henrik Böving]

Congrats, you are in an alpine container :P

[Henrik Böving]

Yeah, you can't run Lean in an alpine container unfortunately

[Bhavik Mehta]

Since I did this from mathlib, I presume that means there's a config file in mathlib we should change to disallow alpine containers?

[Bhavik Mehta]

Or instead, do I need to change something in my codespaces profile (if such a thing exists)?

[Henrik Böving]

I'm a bit confused, the config file https://github.com/leanprover-community/mathlib4/blob/master/.devcontainer/Dockerfile in mathlib branches off from from ubuntu jammy, if that Dockerfile was actually used while you setup the codespace (I've never used codspaces) you should not be in an alpine container

[Henrik Böving]

Or maybe .devcontainer is not related to codespaces? I have no clue how this works really

[Bhavik Mehta]

Here's the start of the creation log

=================================================================================
2025-08-01 20:06:58.392Z: Configuration starting...
2025-08-01 20:06:58.401Z: Cloning...

=================================================================================
2025-08-01 20:07:06.770Z: Creating container...
2025-08-01 20:07:06.806Z: $ devcontainer up --id-label Type=codespaces --workspace-folder /var/lib/docker/codespacemount/workspace/mathlib4 --mount type=bind,source=/.codespaces/agent/mount/cache,target=/vscode --user-data-folder /var/lib/docker/codespacemount/.persistedshare --container-data-folder .vscode-remote/data/Machine --container-system-data-folder /var/vscode-remote --log-level trace --log-format json --update-remote-user-uid-default never --mount-workspace-git-root false --omit-config-remote-env-from-metadata --skip-non-blocking-commands --skip-post-create --config "/var/lib/docker/codespacemount/workspace/mathlib4/.devcontainer/devcontainer.json" --override-config /root/.codespaces/shared/merged_devcontainer.json --default-user-env-probe loginInteractiveShell --container-session-data-folder /workspaces/.codespaces/.persistedshare/devcontainers-cli/cache --secrets-file /root/.codespaces/shared/user-secrets-envs.json
2025-08-01 20:07:06.939Z: @devcontainers/cli 0.80.0. Node.js v18.20.6. linux 6.8.0-1030-azure x64.
2025-08-01 20:07:07.888Z: $4}}] ghcr.io/leanprover-community/mathlib4/gitpod -c echo Container started
2025-08-01 20:07:07.902Z: Unable to find image 'ghcr.io/leanprover-community/mathlib4/gitpod:latest' locally
2025-08-01 20:07:08.538Z: latest: Pulling from leanprover-community/mathlib4/gitpod
2025-08-01 20:07:08.540Z:
[1A[2K
2025-08-01 20:07:08.540Z: 66587c81b81a: Pulling fs layer

[Bhavik Mehta]

Ah, it looks like it was changed 3 months ago to use https://github.com/leanprover-community/mathlib4/blob/master/.devcontainer/devcontainer.json and a prebuilt docker image, rather than that specific Dockerfile

[Bryan Gin-ge Chen]

cc: @Jon Eugster

[Bhavik Mehta]

I just tried again to open a codespaces using the button on mathlib4 readme, and it seems to work fine this time... So perhaps it's either different on PRs, or picks the container type randomly?

[Yaël Dillies]

Uhoh, this is partly my doing. If I update the dockerfiles to use jammy, then everything should be back in order, right?

[Bhavik Mehta]

In your defense this is maybe the 10th time I've used codespaces and the first time it's failed, so it's not entirely clear that it is your fault!

[Yaël Dillies]

This bug is really curious then :thinking:

[Bhavik Mehta]

I just hit this again, twice in a row. In each case, it took about 15 minutes to set up the codespace, and after all that I got the error message as above...