Stream: Miscellaneous

Topic: ✔ Docker image with Alectryon


view this post on Zulip Ana de Almeida Borges (May 31 2022 at 00:31):

As far as I can tell there is no docker image with Alectryon yet (right?). I'm trying to create one, but something is going wrong. When I build it locally it seems to work fine (alectryon --version prints the expected version), but when I use it in CI, it complains that the alectryon command can't be found. I have no clue how to debug this, does anyone with more experience have some suggestions? The Dockerfile:

FROM mathcomp/mathcomp:1.13.0-coq-8.15

RUN sudo apt-get update && sudo apt-get install -y python3-pip

RUN python3 -m pip install alectryon

RUN opam update && opam pin add coq-mathcomp-finmap 1.5.1 --yes

view this post on Zulip Paolo Giarrusso (May 31 2022 at 01:05):

Is alectryon in the PATH?

When I build it locally it seems to work fine (alectryon --version prints the expected version)

Locally, but with or without the image? Running the same commands in the same image is meant to give the same results — OTOH, installing Alectryon outside the image might need different instructions.

view this post on Zulip Paolo Giarrusso (May 31 2022 at 01:06):

In particular, you can run docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 locally. Or rather, anybody can, so I'm taking a look

view this post on Zulip Paolo Giarrusso (May 31 2022 at 01:12):

Okay, Unix strikes again: the nested environment gets different PATH values depending on how exactly it is started, so I guess Gitlab's using a different command:

$ docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13
coq@7e1254587dca:~$ which alectryon
/home/coq/.local/bin/alectryon
coq@7e1254587dca:~$ echo $PATH
/home/coq/.opam/4.07.1+flambda/bin:/home/coq/.local/bin:/home/coq/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games
$ docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 /bin/bash
WARNING: The requested image's platform (linux/amd64) does not match the detected host platform (linux/arm64/v8) and no specific platform was requested
coq@332afb7f5ee9:~$ echo $PATH
/home/coq/.opam/4.07.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
coq@332afb7f5ee9:~$ which alectryon
coq@332afb7f5ee9:~$
$ docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 /bin/bash -l
coq@699df2139528:~$ which alectryon
/home/coq/.local/bin/alectryon

view this post on Zulip Paolo Giarrusso (May 31 2022 at 01:16):

If this is the problem you're hitting, the quickfix is to add ~/.local/bin to the PATH anyway, either in the CI script, or in the container by appending to the Dockerfile this:

ENV PATH "/home/coq/.local/bin:$PATH"

(Strictly speaking, this is not perfect but I doubt it's a concrete problem: This might duplicate the PATH entry sometimes).

view this post on Zulip Paolo Giarrusso (May 31 2022 at 01:18):

I haven't summarized why .local/bin is there only sometimes — to say a bit more, that setting is normally added to the PATH by ~/.profile, which is only loaded by bash when it is started as a login shell (e.g. via /bin/bash -l), but not as a normal shell (e.g. via /bin/bash).

view this post on Zulip Paolo Giarrusso (May 31 2022 at 01:19):

I'll stop this wall of text now :sweat_smile: , please let me know any follow-up

view this post on Zulip Théo Zimmermann (May 31 2022 at 07:05):

FWIW, the idea was that by including SerAPI in the Docker-Coq images, it would make it easy to use with Alectryon, since Alectryon is quick to install with pip.

view this post on Zulip Ana de Almeida Borges (May 31 2022 at 09:32):

@Paolo Giarrusso that was exactly the issue, thanks very much!

view this post on Zulip Ana de Almeida Borges (May 31 2022 at 09:35):

Théo Zimmermann said:

FWIW, the idea was that by including SerAPI in the Docker-Coq images, it would make it easy to use with Alectryon, since Alectryon is quick to install with pip.

You're right, but I didn't immediately realize SerAPI was part of the image I was using, and then I already had everything set up, so I thought I might as well go ahead with only alectryon and finmap. It feels wasteful to install dependencies in CI, even if it takes negligible resources :sweat_smile:

view this post on Zulip Notification Bot (May 31 2022 at 09:37):

Ana de Almeida Borges has marked this topic as resolved.


Last updated: Jun 01 2023 at 12:01 UTC